prime_factorization_exists_unique_up_to_permutation

Exact expanded first-order arithmetic statement

forall n. ~(n = 0) -> exists l b c. (((~(n = 0) /\ ((exists ff_u_fsat_complete_source_product ff_v_fsat_complete_source_product. ((((exists ff_h_fsat_complete_source_product_start. ff_h_fsat_complete_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_start. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_start * S ((S (0)) * ff_v_fsat_complete_source_product) + (1))) /\ ((((exists ff_h_fsat_complete_source_product_terminal. ff_h_fsat_complete_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_terminal. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_terminal * S ((S (l)) * ff_v_fsat_complete_source_product) + (n))) /\ forall ff_i_fsat_complete_source_product. (exists ff_lt_fsat_complete_source_product_bound. ff_lt_fsat_complete_source_product_bound + S ff_i_fsat_complete_source_product = l) -> exists ff_p_fsat_complete_source_product ff_r_fsat_complete_source_product ff_s_fsat_complete_source_product. ((((exists ff_h_fsat_complete_source_product_factor. ff_h_fsat_complete_source_product_factor + S (ff_p_fsat_complete_source_product) = S ((S (ff_i_fsat_complete_source_product)) * c)) /\ exists ff_q_fsat_complete_source_product_factor. b = ff_q_fsat_complete_source_product_factor * S ((S (ff_i_fsat_complete_source_product)) * c) + (ff_p_fsat_complete_source_product))) /\ ((((exists ff_h_fsat_complete_source_product_partial. ff_h_fsat_complete_source_product_partial + S (ff_r_fsat_complete_source_product) = S ((S (ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_partial. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_partial * S ((S (ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product) + (ff_r_fsat_complete_source_product))) /\ ((((exists ff_h_fsat_complete_source_product_successor. ff_h_fsat_complete_source_product_successor + S (ff_s_fsat_complete_source_product) = S ((S (S ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_successor. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_successor * S ((S (S ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product) + (ff_s_fsat_complete_source_product))) /\ ff_s_fsat_complete_source_product = ff_r_fsat_complete_source_product * ff_p_fsat_complete_source_product)))))) /\ (forall ftsf_index_fsat_complete_source_primes. (exists ftsf_gap_fsat_complete_source_primes_bound. ftsf_gap_fsat_complete_source_primes_bound + S ftsf_index_fsat_complete_source_primes = (l)) -> exists ftsf_factor_fsat_complete_source_primes. ((((exists ff_h_ftsf_fsat_complete_source_primes_entry. ff_h_ftsf_fsat_complete_source_primes_entry + S (ftsf_factor_fsat_complete_source_primes) = S ((S (ftsf_index_fsat_complete_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_complete_source_primes_entry. b = ff_q_ftsf_fsat_complete_source_primes_entry * S ((S (ftsf_index_fsat_complete_source_primes)) * c) + (ftsf_factor_fsat_complete_source_primes))) /\ ((~(ftsf_factor_fsat_complete_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_complete_source_primes_prime frm_prime_right_ftsf_fsat_complete_source_primes_prime. ftsf_factor_fsat_complete_source_primes = frm_prime_left_ftsf_fsat_complete_source_primes_prime * frm_prime_right_ftsf_fsat_complete_source_primes_prime -> frm_prime_left_ftsf_fsat_complete_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_complete_source_primes_prime = 1))))))) /\ forall m d e. ((~(n = 0) /\ ((exists ff_u_fsat_complete_target_product ff_v_fsat_complete_target_product. ((((exists ff_h_fsat_complete_target_product_start. ff_h_fsat_complete_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_start. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_start * S ((S (0)) * ff_v_fsat_complete_target_product) + (1))) /\ ((((exists ff_h_fsat_complete_target_product_terminal. ff_h_fsat_complete_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_terminal. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_terminal * S ((S (m)) * ff_v_fsat_complete_target_product) + (n))) /\ forall ff_i_fsat_complete_target_product. (exists ff_lt_fsat_complete_target_product_bound. ff_lt_fsat_complete_target_product_bound + S ff_i_fsat_complete_target_product = m) -> exists ff_p_fsat_complete_target_product ff_r_fsat_complete_target_product ff_s_fsat_complete_target_product. ((((exists ff_h_fsat_complete_target_product_factor. ff_h_fsat_complete_target_product_factor + S (ff_p_fsat_complete_target_product) = S ((S (ff_i_fsat_complete_target_product)) * e)) /\ exists ff_q_fsat_complete_target_product_factor. d = ff_q_fsat_complete_target_product_factor * S ((S (ff_i_fsat_complete_target_product)) * e) + (ff_p_fsat_complete_target_product))) /\ ((((exists ff_h_fsat_complete_target_product_partial. ff_h_fsat_complete_target_product_partial + S (ff_r_fsat_complete_target_product) = S ((S (ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_partial. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_partial * S ((S (ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product) + (ff_r_fsat_complete_target_product))) /\ ((((exists ff_h_fsat_complete_target_product_successor. ff_h_fsat_complete_target_product_successor + S (ff_s_fsat_complete_target_product) = S ((S (S ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_successor. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_successor * S ((S (S ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product) + (ff_s_fsat_complete_target_product))) /\ ff_s_fsat_complete_target_product = ff_r_fsat_complete_target_product * ff_p_fsat_complete_target_product)))))) /\ (forall ftsf_index_fsat_complete_target_primes. (exists ftsf_gap_fsat_complete_target_primes_bound. ftsf_gap_fsat_complete_target_primes_bound + S ftsf_index_fsat_complete_target_primes = (m)) -> exists ftsf_factor_fsat_complete_target_primes. ((((exists ff_h_ftsf_fsat_complete_target_primes_entry. ff_h_ftsf_fsat_complete_target_primes_entry + S (ftsf_factor_fsat_complete_target_primes) = S ((S (ftsf_index_fsat_complete_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_complete_target_primes_entry. d = ff_q_ftsf_fsat_complete_target_primes_entry * S ((S (ftsf_index_fsat_complete_target_primes)) * e) + (ftsf_factor_fsat_complete_target_primes))) /\ ((~(ftsf_factor_fsat_complete_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_complete_target_primes_prime frm_prime_right_ftsf_fsat_complete_target_primes_prime. ftsf_factor_fsat_complete_target_primes = frm_prime_left_ftsf_fsat_complete_target_primes_prime * frm_prime_right_ftsf_fsat_complete_target_primes_prime -> frm_prime_left_ftsf_fsat_complete_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_complete_target_primes_prime = 1))))))) -> exists u v. (((l = m) /\ (((((forall pfp_i_complete_permutationpermutationbounded. (exists pfp_gap_complete_permutationpermutationboundedindex. pfp_gap_complete_permutationpermutationboundedindex + S (pfp_i_complete_permutationpermutationbounded) = (l)) -> exists pfp_a_complete_permutationpermutationbounded. (((exists ff_h_pfp_complete_permutationpermutationboundedentry. ff_h_pfp_complete_permutationpermutationboundedentry + S (pfp_a_complete_permutationpermutationbounded) = S ((S (pfp_i_complete_permutationpermutationbounded)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationboundedentry. u = ff_q_pfp_complete_permutationpermutationboundedentry * S ((S (pfp_i_complete_permutationpermutationbounded)) * v) + (pfp_a_complete_permutationpermutationbounded))) /\ (exists pfp_gap_complete_permutationpermutationboundedvalue. pfp_gap_complete_permutationpermutationboundedvalue + S (pfp_a_complete_permutationpermutationbounded) = (l))) /\ (((forall pfp_i_complete_permutationpermutationinjective pfp_j_complete_permutationpermutationinjective pfp_a_complete_permutationpermutationinjective. (exists pfp_gap_complete_permutationpermutationinjectivefirst. pfp_gap_complete_permutationpermutationinjectivefirst + S (pfp_i_complete_permutationpermutationinjective) = (l)) -> (exists pfp_gap_complete_permutationpermutationinjectivesecond. pfp_gap_complete_permutationpermutationinjectivesecond + S (pfp_j_complete_permutationpermutationinjective) = (l)) -> (((exists ff_h_pfp_complete_permutationpermutationinjectiveleft. ff_h_pfp_complete_permutationpermutationinjectiveleft + S (pfp_a_complete_permutationpermutationinjective) = S ((S (pfp_i_complete_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationinjectiveleft. u = ff_q_pfp_complete_permutationpermutationinjectiveleft * S ((S (pfp_i_complete_permutationpermutationinjective)) * v) + (pfp_a_complete_permutationpermutationinjective))) -> (((exists ff_h_pfp_complete_permutationpermutationinjectiveright. ff_h_pfp_complete_permutationpermutationinjectiveright + S (pfp_a_complete_permutationpermutationinjective) = S ((S (pfp_j_complete_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationinjectiveright. u = ff_q_pfp_complete_permutationpermutationinjectiveright * S ((S (pfp_j_complete_permutationpermutationinjective)) * v) + (pfp_a_complete_permutationpermutationinjective))) -> pfp_i_complete_permutationpermutationinjective = pfp_j_complete_permutationpermutationinjective) /\ (forall pfp_a_complete_permutationpermutationsurjective. (exists pfp_gap_complete_permutationpermutationsurjectivevalue. pfp_gap_complete_permutationpermutationsurjectivevalue + S (pfp_a_complete_permutationpermutationsurjective) = (l)) -> exists pfp_i_complete_permutationpermutationsurjective. (exists pfp_gap_complete_permutationpermutationsurjectiveindex. pfp_gap_complete_permutationpermutationsurjectiveindex + S (pfp_i_complete_permutationpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_complete_permutationpermutationsurjectiveentry. ff_h_pfp_complete_permutationpermutationsurjectiveentry + S (pfp_a_complete_permutationpermutationsurjective) = S ((S (pfp_i_complete_permutationpermutationsurjective)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationsurjectiveentry. u = ff_q_pfp_complete_permutationpermutationsurjectiveentry * S ((S (pfp_i_complete_permutationpermutationsurjective)) * v) + (pfp_a_complete_permutationpermutationsurjective)))))))) /\ (forall pfp_i_complete_permutationmatching pfp_j_complete_permutationmatching pfp_a_complete_permutationmatching. (exists pfp_gap_complete_permutationmatchingbound. pfp_gap_complete_permutationmatchingbound + S (pfp_i_complete_permutationmatching) = (l)) -> (((exists ff_h_pfp_complete_permutationmatchingmap. ff_h_pfp_complete_permutationmatchingmap + S (pfp_j_complete_permutationmatching) = S ((S (pfp_i_complete_permutationmatching)) * v)) /\ exists ff_q_pfp_complete_permutationmatchingmap. u = ff_q_pfp_complete_permutationmatchingmap * S ((S (pfp_i_complete_permutationmatching)) * v) + (pfp_j_complete_permutationmatching))) -> (((exists ff_h_pfp_complete_permutationmatchingsource. ff_h_pfp_complete_permutationmatchingsource + S (pfp_a_complete_permutationmatching) = S ((S (pfp_i_complete_permutationmatching)) * c)) /\ exists ff_q_pfp_complete_permutationmatchingsource. b = ff_q_pfp_complete_permutationmatchingsource * S ((S (pfp_i_complete_permutationmatching)) * c) + (pfp_a_complete_permutationmatching))) -> (((exists ff_h_pfp_complete_permutationmatchingtarget. ff_h_pfp_complete_permutationmatchingtarget + S (pfp_a_complete_permutationmatching) = S ((S (pfp_j_complete_permutationmatching)) * e)) /\ exists ff_q_pfp_complete_permutationmatchingtarget. d = ff_q_pfp_complete_permutationmatchingtarget * S ((S (pfp_j_complete_permutationmatching)) * e) + (pfp_a_complete_permutationmatching)))))))))