Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall B n. (exists ftsp_induction_gap. ftsp_induction_gap + n = B) -> ~(n = 0) -> (forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value) -> (exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result)Constructive proof overview
Generated structural guide
Bounded constructive descent on the natural value proves sufficiency of even valuations at every three-modulo-four prime.
The unchanged tactic script uses 18 declared prerequisites and contains 186 exact native proof lines.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged
Proof neighborhood
Direct dependencies
le_zero Stable theorem; checked-use authorized eq_decidable Stable theorem; checked-use authorized prime_divisor_exists Stable theorem; checked-use authorized TS003B prime_mod_four_good_or_three TS002O prime_two_or_one_mod_four_is_sum_of_two_squares TS003A all_bad_prime_even_valuation_value_eq_transport TS0038 all_bad_prime_even_valuations_strip_represented_prime mul_comm Stable theorem; checked-use authorized proper_factor_lt Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized TS001X two_square_representation_multiplicatively_closed power_valuation_exists Alpha theorem; checked-use authorized TS002Z even_positive_prime_valuation_has_square_divisor prime_nonzero Stable theorem; checked-use authorized TS0039 all_bad_prime_even_valuations_strip_square_factor TS003S prime_square_times_nonzero_strictly_increases TS003M two_square_representation_preserved_by_square_factorDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (9)
prime mod four good or threeprime two or one mod four is sum of two squaresall bad prime even valuation value eq transportall bad prime even valuations strip represented primetwo square representation multiplicatively closedeven positive prime valuation has square divisorall bad prime even valuations strip square factorprime square times nonzero strictly increasestwo square representation preserved by square factor
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro B
02Induction on BL2–6
03Separate the logical casesL7–7
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L7
exfalso
04Use earlier factsL8–11
05Fix variables and assumptionsL12–15
06Use earlier factsL16–17
07Separate the logical casesL18–18
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L18
cases eq_decidable
08Construct an explicit witnessL19–20
09Calculate and transport equalitiesL21–22
10Establish hfactorL23–27
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisor exists.
- L23
have hfactor : exists p. (((~(p = 1) /\ forall frm_prime_left_ftsp_induction_factor_prime frm_prime_right_ftsp_induction_factor_prime. p = frm_prime_left_ftsp_induction_factor_prime * frm_prime_right_ftsp_induction_factor_prime -> frm_prime_left_ftsp_induction_factor_prime = 1 \/ frm_prime_right_ftsp_induction_factor_prime = 1)) /\ exists r. n = p * r) - L24
specialize prime_divisor_exists n - L25
apply prime_divisor_exists - L26
exact hnonzero - L27
exact eq_decidable_right
11Separate the logical casesL28–30
12Establish hprefix_nonzeroL31–37
13Establish hchoiceL38–41
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mod four good or three.
14Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
cases hchoice
15Establish hrepresented_primeL43–47
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime two or one mod four is sum of two squares.
- L43
have hrepresented_prime : (exists ftsc_first_ftsp_induction_good_prime ftsc_second_ftsp_induction_good_prime. (x) = ftsc_first_ftsp_induction_good_prime * ftsc_first_ftsp_induction_good_prime + ftsc_second_ftsp_induction_good_prime * ftsc_second_ftsp_induction_good_prime) - L44
specialize prime_two_or_one_mod_four_is_sum_of_two_squares x - L45
apply prime_two_or_one_mod_four_is_sum_of_two_squares - L46
exact hfactor_witness_left - L47
exact hchoice_left
16Establish horderedL48–51
17Establish hproduct_parityL52–57
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply all bad prime even valuation value eq transport.
- L52
have hproduct_parity : ∀ y. ∀ z. Prime(y) → Mod4Three(y) → BoundedPowerValuation(y,x1 · x,x1 · x,z) → ∃ n. z = n + nDefinitions: PrimeMod4ThreeBoundedPowerValuation - L53
specialize all_bad_prime_even_valuation_value_eq_transport n - L54
specialize all_bad_prime_even_valuation_value_eq_transport (x1 * x) - L55
apply all_bad_prime_even_valuation_value_eq_transport - L56
exact hordered - L57
exact hparity
18Establish hprefix_parityL58–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply all bad prime even valuations strip represented prime.
- L58
have hprefix_parity : ∀ x. ∀ y. Prime(x) → Mod4Three(x) → BoundedPowerValuation(x,x1,x1,y) → ∃ z. y = z + zDefinitions: PrimeMod4ThreeBoundedPowerValuation - L59
specialize all_bad_prime_even_valuations_strip_represented_prime x - L60
specialize all_bad_prime_even_valuations_strip_represented_prime x1 - L61
apply all_bad_prime_even_valuations_strip_represented_prime - L62
exact hfactor_witness_left - L63
exact hrepresented_prime - L64
exact hprefix_nonzero - L65
exact hproduct_parity
19Establish hnotoneL66–66
Establish this local claim before using it. It is not an additional assumption.
- L66
have hnotone : ~(x = 1)
20Separate the logical casesL67–67
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L67
cases hfactor_witness_left
21Use earlier factsL68–68
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L68
exact hfactor_witness_left_left
22Establish hstrictL69–76
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply proper factor lt.
23Establish hsuccessor_boundL77–83
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
24Establish hprefix_boundL84–88
25Establish hprefix_representationL89–98
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L89
have hprefix_representation : (exists ftsc_first_ftsp_induction_good_prefix_result ftsc_second_ftsp_induction_good_prefix_result. (x1) = ftsc_first_ftsp_induction_good_prefix_result * ftsc_first_ftsp_induction_good_prefix_result + ftsc_second_ftsp_induction_good_prefix_result * ftsc_second_ftsp_induction_good_prefix_result) - L90
specialize IH x1 - L91
apply IH - L92
exact hprefix_bound - L93
exact hprefix_nonzero - L94
exact hprefix_parity - L95
rewrite hordered - L96
specialize two_square_representation_multiplicatively_closed x1 - L97
specialize two_square_representation_multiplicatively_closed x - L98
apply two_square_representation_multiplicatively_closed
26Use earlier factsL99–100
27Establish hvaluationL101–102
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation exists.
- L101
have hvaluation : ∃ e. BoundedPowerValuation(x,n,n,e)Definitions: BoundedPowerValuation - L102
apply power_valuation_exists
28Separate the logical casesL103–103
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L103
cases hvaluation
29Establish hevenL104–110
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hparity.
30Separate the logical casesL111–111
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L111
cases heven
31Establish hdividesL112–112
Establish this local claim before using it. It is not an additional assumption.
- L112
have hdivides : exists k. n = x * k
32Construct an explicit witnessL113–113
Supply the displayed value, then prove that it has the required property.
- L113
exists x1
33Use earlier factsL114–114
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L114
exact hfactor_witness_right_witness
34Establish hsquareL115–124
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even positive prime valuation has square divisor.
- L115
have hsquare : exists r. n = (x * x) * r - L116
specialize even_positive_prime_valuation_has_square_divisor x - L117
specialize even_positive_prime_valuation_has_square_divisor n - L118
specialize even_positive_prime_valuation_has_square_divisor x2 - L119
specialize even_positive_prime_valuation_has_square_divisor x3 - L120
apply even_positive_prime_valuation_has_square_divisor - L121
exact hfactor_witness_left - L122
exact hnonzero - L123
exact hvaluation_witness - L124
exact hdivides
35Use earlier factsL125–125
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L125
exact heven_witness
36Separate the logical casesL126–126
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L126
cases hsquare
37Establish hsquare_quotient_nonzeroL127–133
38Establish hprime_nonzeroL134–139
39Establish hsquare_orderedL140–143
40Establish hsquare_parityL144–149
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply all bad prime even valuation value eq transport.
- L144
have hsquare_parity : ∀ y. ∀ z. Prime(y) → Mod4Three(y) → BoundedPowerValuation(y,x4 · (x · x),x4 · (x · x),z) → ∃ n. z = n + nDefinitions: PrimeMod4ThreeBoundedPowerValuation - L145
specialize all_bad_prime_even_valuation_value_eq_transport n - L146
specialize all_bad_prime_even_valuation_value_eq_transport (x4 * (x * x)) - L147
apply all_bad_prime_even_valuation_value_eq_transport - L148
exact hsquare_ordered - L149
exact hparity
41Establish hquotient_parityL150–156
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply all bad prime even valuations strip square factor.
- L150
have hquotient_parity : ∀ x. ∀ y. Prime(x) → Mod4Three(x) → BoundedPowerValuation(x,x4,x4,y) → ∃ z. y = z + zDefinitions: PrimeMod4ThreeBoundedPowerValuation - L151
specialize all_bad_prime_even_valuations_strip_square_factor x - L152
specialize all_bad_prime_even_valuations_strip_square_factor x4 - L153
apply all_bad_prime_even_valuations_strip_square_factor - L154
exact hprime_nonzero - L155
exact hsquare_quotient_nonzero - L156
exact hsquare_parity
42Establish hsquare_strictL157–163
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime square times nonzero strictly increases.
- L157
have hsquare_strict : exists k. k + S x4 = (x * x) * x4 - L158
specialize prime_square_times_nonzero_strictly_increases x - L159
specialize prime_square_times_nonzero_strictly_increases x4 - L160
apply prime_square_times_nonzero_strictly_increases - L161
exact hfactor_witness_left - L162
exact hsquare_quotient_nonzero - L163
rewrite <- hsquare_witness at hsquare_strict
43Establish hsquare_successor_boundL164–170
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
44Establish hsquare_boundL171–175
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.
45Establish hquotient_representationL176–185
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L176
have hquotient_representation : (exists ftsc_first_ftsp_induction_bad_prefix_result ftsc_second_ftsp_induction_bad_prefix_result. (x4) = ftsc_first_ftsp_induction_bad_prefix_result * ftsc_first_ftsp_induction_bad_prefix_result + ftsc_second_ftsp_induction_bad_prefix_result * ftsc_second_ftsp_induction_bad_prefix_result) - L177
specialize IH x4 - L178
apply IH - L179
exact hsquare_bound - L180
exact hsquare_quotient_nonzero - L181
exact hquotient_parity - L182
rewrite hsquare_ordered - L183
specialize two_square_representation_preserved_by_square_factor x4 - L184
specialize two_square_representation_preserved_by_square_factor x - L185
apply two_square_representation_preserved_by_square_factor
46Use earlier factsL186–186
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L186
exact hquotient_representation
Original exact command ledger · 186 lines
- 0001
intro B - 0002
induction B - 0003
intro n - 0004
intro hbound - 0005
intro hnonzero - 0006
intro hparity - 0007
exfalso - 0008
apply hnonzero - 0009
specialize le_zero n - 0010
apply le_zero - 0011
exact hbound - 0012
intro n - 0013
intro hbound - 0014
intro hnonzero - 0015
intro hparity - 0016
specialize eq_decidable n - 0017
specialize eq_decidable 1 - 0018
cases eq_decidable - 0019
exists 1 - 0020
exists 0 - 0021
rewrite eq_decidable_left - 0022
norm_num - 0023
have hfactor : exists p. (((~(p = 1) /\ forall frm_prime_left_ftsp_induction_factor_prime frm_prime_right_ftsp_induction_factor_prime. p = frm_prime_left_ftsp_induction_factor_prime * frm_prime_right_ftsp_induction_factor_prime -> frm_prime_left_ftsp_induction_factor_prime = 1 \/ frm_prime_right_ftsp_induction_factor_prime = 1)) /\ exists r. n = p * r) - 0024
specialize prime_divisor_exists n - 0025
apply prime_divisor_exists - 0026
exact hnonzero - 0027
exact eq_decidable_right - 0028
cases hfactor - 0029
cases hfactor_witness - 0030
cases hfactor_witness_right - 0031
have hprefix_nonzero : ~(x1 = 0) - 0032
intro hzero - 0033
apply hnonzero - 0034
trans x * x1 - 0035
exact hfactor_witness_right_witness - 0036
rewrite hzero - 0037
apply PA5 - 0038
have hchoice : ((x = 2 \/ exists k. x = 4 * k + 1) \/ exists k. x = 4 * k + 3) - 0039
specialize prime_mod_four_good_or_three x - 0040
apply prime_mod_four_good_or_three - 0041
exact hfactor_witness_left - 0042
cases hchoice - 0043
have hrepresented_prime : (exists ftsc_first_ftsp_induction_good_prime ftsc_second_ftsp_induction_good_prime. (x) = ftsc_first_ftsp_induction_good_prime * ftsc_first_ftsp_induction_good_prime + ftsc_second_ftsp_induction_good_prime * ftsc_second_ftsp_induction_good_prime) - 0044
specialize prime_two_or_one_mod_four_is_sum_of_two_squares x - 0045
apply prime_two_or_one_mod_four_is_sum_of_two_squares - 0046
exact hfactor_witness_left - 0047
exact hchoice_left - 0048
have hordered : n = x1 * x - 0049
trans x * x1 - 0050
exact hfactor_witness_right_witness - 0051
apply mul_comm - 0052
have hproduct_parity : (forall ftsp_bad_prime_ftsp_induction_good_product ftsp_bad_exponent_ftsp_induction_good_product. ((~(ftsp_bad_prime_ftsp_induction_good_product = 1) /\ forall frm_prime_left_ftsp_ftsp_induction_good_product_prime frm_prime_right_ftsp_ftsp_induction_good_product_prime. ftsp_bad_prime_ftsp_induction_good_product = frm_prime_left_ftsp_ftsp_induction_good_product_prime * frm_prime_right_ftsp_ftsp_induction_good_product_prime -> frm_prime_left_ftsp_ftsp_induction_good_product_prime = 1 \/ frm_prime_right_ftsp_ftsp_induction_good_product_prime = 1)) -> (exists ftsc_four_three_ftsp_ftsp_induction_good_product_three. (ftsp_bad_prime_ftsp_induction_good_product) = 4 * ftsc_four_three_ftsp_ftsp_induction_good_product_three + 3) -> (((exists bpv_gap_ftsp_ftsp_induction_good_product_valuation_exponent_bound. bpv_gap_ftsp_ftsp_induction_good_product_valuation_exponent_bound + ftsp_bad_exponent_ftsp_induction_good_product = (x1 * x)) /\ (exists bpv_result_ftsp_ftsp_induction_good_product_valuation_selected. ((exists ff_b_ftsp_ftsp_induction_good_product_valuation_selected_power ff_c_ftsp_ftsp_induction_good_product_valuation_selected_power. ((forall ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat. (exists ff_lt_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat_bound. ff_lt_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat_bound + S ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat = ftsp_bad_exponent_ftsp_induction_good_product) -> (((exists ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat_decoded. ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_good_product) = S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_good_product_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat_decoded. ff_b_ftsp_ftsp_induction_good_product_valuation_selected_power = ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_good_product_valuation_selected_power) + (ftsp_bad_prime_ftsp_induction_good_product)))) /\ (exists ff_u_ftsp_ftsp_induction_good_product_valuation_selected_power_product ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_start. ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_start. ff_u_ftsp_ftsp_induction_good_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_terminal. ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_good_product_valuation_selected) = S ((S (ftsp_bad_exponent_ftsp_induction_good_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_terminal. ff_u_ftsp_ftsp_induction_good_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_ftsp_induction_good_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product) + (bpv_result_ftsp_ftsp_induction_good_product_valuation_selected))) /\ forall ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product. (exists ff_lt_ftsp_ftsp_induction_good_product_valuation_selected_power_product_bound. ff_lt_ftsp_ftsp_induction_good_product_valuation_selected_power_product_bound + S ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product = ftsp_bad_exponent_ftsp_induction_good_product) -> exists ff_p_ftsp_ftsp_induction_good_product_valuation_selected_power_product ff_r_ftsp_ftsp_induction_good_product_valuation_selected_power_product ff_s_ftsp_ftsp_induction_good_product_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_factor. ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_factor + S (ff_p_ftsp_ftsp_induction_good_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_good_product_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_factor. ff_b_ftsp_ftsp_induction_good_product_valuation_selected_power = ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_good_product_valuation_selected_power) + (ff_p_ftsp_ftsp_induction_good_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_partial. ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_partial + S (ff_r_ftsp_ftsp_induction_good_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_partial. ff_u_ftsp_ftsp_induction_good_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product) + (ff_r_ftsp_ftsp_induction_good_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_successor. ff_h_ftsp_ftsp_induction_good_product_valuation_selected_power_product_successor + S (ff_s_ftsp_ftsp_induction_good_product_valuation_selected_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_successor. ff_u_ftsp_ftsp_induction_good_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_good_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_selected_power_product) + (ff_s_ftsp_ftsp_induction_good_product_valuation_selected_power_product))) /\ ff_s_ftsp_ftsp_induction_good_product_valuation_selected_power_product = ff_r_ftsp_ftsp_induction_good_product_valuation_selected_power_product * ff_p_ftsp_ftsp_induction_good_product_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_good_product_valuation_selected_divides. (x1 * x) = bpv_result_ftsp_ftsp_induction_good_product_valuation_selected * bpv_factor_ftsp_ftsp_induction_good_product_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_ftsp_induction_good_product_valuation. (exists bpv_gap_ftsp_ftsp_induction_good_product_valuation_candidate_bound. bpv_gap_ftsp_ftsp_induction_good_product_valuation_candidate_bound + bpv_candidate_ftsp_ftsp_induction_good_product_valuation = (x1 * x)) -> (exists bpv_result_ftsp_ftsp_induction_good_product_valuation_candidate. ((exists ff_b_ftsp_ftsp_induction_good_product_valuation_candidate_power ff_c_ftsp_ftsp_induction_good_product_valuation_candidate_power. ((forall ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat. (exists ff_lt_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat_bound. ff_lt_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat_bound + S ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat = bpv_candidate_ftsp_ftsp_induction_good_product_valuation) -> (((exists ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat_decoded. ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_good_product) = S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_good_product_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat_decoded. ff_b_ftsp_ftsp_induction_good_product_valuation_candidate_power = ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_good_product_valuation_candidate_power) + (ftsp_bad_prime_ftsp_induction_good_product)))) /\ (exists ff_u_ftsp_ftsp_induction_good_product_valuation_candidate_power_product ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_start. ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_start. ff_u_ftsp_ftsp_induction_good_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_terminal. ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_good_product_valuation_candidate) = S ((S (bpv_candidate_ftsp_ftsp_induction_good_product_valuation)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_terminal. ff_u_ftsp_ftsp_induction_good_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_ftsp_induction_good_product_valuation)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) + (bpv_result_ftsp_ftsp_induction_good_product_valuation_candidate))) /\ forall ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product. (exists ff_lt_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_bound. ff_lt_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_bound + S ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product = bpv_candidate_ftsp_ftsp_induction_good_product_valuation) -> exists ff_p_ftsp_ftsp_induction_good_product_valuation_candidate_power_product ff_r_ftsp_ftsp_induction_good_product_valuation_candidate_power_product ff_s_ftsp_ftsp_induction_good_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_factor. ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_factor + S (ff_p_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_good_product_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_factor. ff_b_ftsp_ftsp_induction_good_product_valuation_candidate_power = ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_good_product_valuation_candidate_power) + (ff_p_ftsp_ftsp_induction_good_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_partial. ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_partial + S (ff_r_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_partial. ff_u_ftsp_ftsp_induction_good_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) + (ff_r_ftsp_ftsp_induction_good_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_successor. ff_h_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_successor + S (ff_s_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_successor. ff_u_ftsp_ftsp_induction_good_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_product_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_product_valuation_candidate_power_product) + (ff_s_ftsp_ftsp_induction_good_product_valuation_candidate_power_product))) /\ ff_s_ftsp_ftsp_induction_good_product_valuation_candidate_power_product = ff_r_ftsp_ftsp_induction_good_product_valuation_candidate_power_product * ff_p_ftsp_ftsp_induction_good_product_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_good_product_valuation_candidate_divides. (x1 * x) = bpv_result_ftsp_ftsp_induction_good_product_valuation_candidate * bpv_factor_ftsp_ftsp_induction_good_product_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_ftsp_induction_good_product_valuation_maximal. bpv_gap_ftsp_ftsp_induction_good_product_valuation_maximal + bpv_candidate_ftsp_ftsp_induction_good_product_valuation = ftsp_bad_exponent_ftsp_induction_good_product)) -> exists ftsp_bad_half_ftsp_induction_good_product. ftsp_bad_exponent_ftsp_induction_good_product = ftsp_bad_half_ftsp_induction_good_product + ftsp_bad_half_ftsp_induction_good_product) - 0053
specialize all_bad_prime_even_valuation_value_eq_transport n - 0054
specialize all_bad_prime_even_valuation_value_eq_transport (x1 * x) - 0055
apply all_bad_prime_even_valuation_value_eq_transport - 0056
exact hordered - 0057
exact hparity - 0058
have hprefix_parity : (forall ftsp_bad_prime_ftsp_induction_good_prefix ftsp_bad_exponent_ftsp_induction_good_prefix. ((~(ftsp_bad_prime_ftsp_induction_good_prefix = 1) /\ forall frm_prime_left_ftsp_ftsp_induction_good_prefix_prime frm_prime_right_ftsp_ftsp_induction_good_prefix_prime. ftsp_bad_prime_ftsp_induction_good_prefix = frm_prime_left_ftsp_ftsp_induction_good_prefix_prime * frm_prime_right_ftsp_ftsp_induction_good_prefix_prime -> frm_prime_left_ftsp_ftsp_induction_good_prefix_prime = 1 \/ frm_prime_right_ftsp_ftsp_induction_good_prefix_prime = 1)) -> (exists ftsc_four_three_ftsp_ftsp_induction_good_prefix_three. (ftsp_bad_prime_ftsp_induction_good_prefix) = 4 * ftsc_four_three_ftsp_ftsp_induction_good_prefix_three + 3) -> (((exists bpv_gap_ftsp_ftsp_induction_good_prefix_valuation_exponent_bound. bpv_gap_ftsp_ftsp_induction_good_prefix_valuation_exponent_bound + ftsp_bad_exponent_ftsp_induction_good_prefix = (x1)) /\ (exists bpv_result_ftsp_ftsp_induction_good_prefix_valuation_selected. ((exists ff_b_ftsp_ftsp_induction_good_prefix_valuation_selected_power ff_c_ftsp_ftsp_induction_good_prefix_valuation_selected_power. ((forall ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat. (exists ff_lt_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat_bound. ff_lt_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat_bound + S ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat = ftsp_bad_exponent_ftsp_induction_good_prefix) -> (((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat_decoded. ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_good_prefix) = S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat_decoded. ff_b_ftsp_ftsp_induction_good_prefix_valuation_selected_power = ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_selected_power) + (ftsp_bad_prime_ftsp_induction_good_prefix)))) /\ (exists ff_u_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_start. ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_start. ff_u_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_terminal. ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_good_prefix_valuation_selected) = S ((S (ftsp_bad_exponent_ftsp_induction_good_prefix)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_terminal. ff_u_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_ftsp_induction_good_prefix)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) + (bpv_result_ftsp_ftsp_induction_good_prefix_valuation_selected))) /\ forall ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product. (exists ff_lt_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_bound. ff_lt_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_bound + S ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product = ftsp_bad_exponent_ftsp_induction_good_prefix) -> exists ff_p_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product ff_r_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product ff_s_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_factor. ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_factor + S (ff_p_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_factor. ff_b_ftsp_ftsp_induction_good_prefix_valuation_selected_power = ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_selected_power) + (ff_p_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_partial. ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_partial + S (ff_r_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_partial. ff_u_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) + (ff_r_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_successor. ff_h_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_successor + S (ff_s_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_successor. ff_u_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product) + (ff_s_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product))) /\ ff_s_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product = ff_r_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product * ff_p_ftsp_ftsp_induction_good_prefix_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_good_prefix_valuation_selected_divides. (x1) = bpv_result_ftsp_ftsp_induction_good_prefix_valuation_selected * bpv_factor_ftsp_ftsp_induction_good_prefix_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation. (exists bpv_gap_ftsp_ftsp_induction_good_prefix_valuation_candidate_bound. bpv_gap_ftsp_ftsp_induction_good_prefix_valuation_candidate_bound + bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation = (x1)) -> (exists bpv_result_ftsp_ftsp_induction_good_prefix_valuation_candidate. ((exists ff_b_ftsp_ftsp_induction_good_prefix_valuation_candidate_power ff_c_ftsp_ftsp_induction_good_prefix_valuation_candidate_power. ((forall ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat. (exists ff_lt_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat_bound. ff_lt_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat_bound + S ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat = bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation) -> (((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat_decoded. ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_good_prefix) = S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat_decoded. ff_b_ftsp_ftsp_induction_good_prefix_valuation_candidate_power = ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_candidate_power) + (ftsp_bad_prime_ftsp_induction_good_prefix)))) /\ (exists ff_u_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_start. ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_start. ff_u_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_terminal. ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_good_prefix_valuation_candidate) = S ((S (bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_terminal. ff_u_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) + (bpv_result_ftsp_ftsp_induction_good_prefix_valuation_candidate))) /\ forall ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product. (exists ff_lt_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_bound. ff_lt_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_bound + S ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product = bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation) -> exists ff_p_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product ff_r_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product ff_s_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_factor. ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_factor + S (ff_p_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_factor. ff_b_ftsp_ftsp_induction_good_prefix_valuation_candidate_power = ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_good_prefix_valuation_candidate_power) + (ff_p_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_partial. ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_partial + S (ff_r_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_partial. ff_u_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) + (ff_r_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_successor. ff_h_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_successor + S (ff_s_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_successor. ff_u_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product) + (ff_s_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product))) /\ ff_s_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product = ff_r_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product * ff_p_ftsp_ftsp_induction_good_prefix_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_good_prefix_valuation_candidate_divides. (x1) = bpv_result_ftsp_ftsp_induction_good_prefix_valuation_candidate * bpv_factor_ftsp_ftsp_induction_good_prefix_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_ftsp_induction_good_prefix_valuation_maximal. bpv_gap_ftsp_ftsp_induction_good_prefix_valuation_maximal + bpv_candidate_ftsp_ftsp_induction_good_prefix_valuation = ftsp_bad_exponent_ftsp_induction_good_prefix)) -> exists ftsp_bad_half_ftsp_induction_good_prefix. ftsp_bad_exponent_ftsp_induction_good_prefix = ftsp_bad_half_ftsp_induction_good_prefix + ftsp_bad_half_ftsp_induction_good_prefix) - 0059
specialize all_bad_prime_even_valuations_strip_represented_prime x - 0060
specialize all_bad_prime_even_valuations_strip_represented_prime x1 - 0061
apply all_bad_prime_even_valuations_strip_represented_prime - 0062
exact hfactor_witness_left - 0063
exact hrepresented_prime - 0064
exact hprefix_nonzero - 0065
exact hproduct_parity - 0066
have hnotone : ~(x = 1) - 0067
cases hfactor_witness_left - 0068
exact hfactor_witness_left_left - 0069
have hstrict : exists k. k + S x1 = n - 0070
specialize proper_factor_lt n - 0071
specialize proper_factor_lt x1 - 0072
specialize proper_factor_lt x - 0073
apply proper_factor_lt - 0074
exact hnonzero - 0075
exact hordered - 0076
exact hnotone - 0077
have hsuccessor_bound : exists k. k + S x1 = S B - 0078
specialize le_trans (S x1) - 0079
specialize le_trans n - 0080
specialize le_trans (S B) - 0081
apply le_trans - 0082
exact hstrict - 0083
exact hbound - 0084
have hprefix_bound : exists k. k + x1 = B - 0085
specialize le_of_succ_le_succ x1 - 0086
specialize le_of_succ_le_succ B - 0087
apply le_of_succ_le_succ - 0088
exact hsuccessor_bound - 0089
have hprefix_representation : (exists ftsc_first_ftsp_induction_good_prefix_result ftsc_second_ftsp_induction_good_prefix_result. (x1) = ftsc_first_ftsp_induction_good_prefix_result * ftsc_first_ftsp_induction_good_prefix_result + ftsc_second_ftsp_induction_good_prefix_result * ftsc_second_ftsp_induction_good_prefix_result) - 0090
specialize IH x1 - 0091
apply IH - 0092
exact hprefix_bound - 0093
exact hprefix_nonzero - 0094
exact hprefix_parity - 0095
rewrite hordered - 0096
specialize two_square_representation_multiplicatively_closed x1 - 0097
specialize two_square_representation_multiplicatively_closed x - 0098
apply two_square_representation_multiplicatively_closed - 0099
exact hprefix_representation - 0100
exact hrepresented_prime - 0101
have hvaluation : exists e. (((exists bpv_gap_ftsp_induction_bad_valuation_exponent_bound. bpv_gap_ftsp_induction_bad_valuation_exponent_bound + e = n) /\ (exists bpv_result_ftsp_induction_bad_valuation_selected. ((exists ff_b_ftsp_induction_bad_valuation_selected_power ff_c_ftsp_induction_bad_valuation_selected_power. ((forall ff_i_ftsp_induction_bad_valuation_selected_power_repeat. (exists ff_lt_ftsp_induction_bad_valuation_selected_power_repeat_bound. ff_lt_ftsp_induction_bad_valuation_selected_power_repeat_bound + S ff_i_ftsp_induction_bad_valuation_selected_power_repeat = e) -> (((exists ff_h_ftsp_induction_bad_valuation_selected_power_repeat_decoded. ff_h_ftsp_induction_bad_valuation_selected_power_repeat_decoded + S (x) = S ((S (ff_i_ftsp_induction_bad_valuation_selected_power_repeat)) * ff_c_ftsp_induction_bad_valuation_selected_power)) /\ exists ff_q_ftsp_induction_bad_valuation_selected_power_repeat_decoded. ff_b_ftsp_induction_bad_valuation_selected_power = ff_q_ftsp_induction_bad_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_induction_bad_valuation_selected_power_repeat)) * ff_c_ftsp_induction_bad_valuation_selected_power) + (x)))) /\ (exists ff_u_ftsp_induction_bad_valuation_selected_power_product ff_v_ftsp_induction_bad_valuation_selected_power_product. ((((exists ff_h_ftsp_induction_bad_valuation_selected_power_product_start. ff_h_ftsp_induction_bad_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_induction_bad_valuation_selected_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_selected_power_product_start. ff_u_ftsp_induction_bad_valuation_selected_power_product = ff_q_ftsp_induction_bad_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_induction_bad_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_induction_bad_valuation_selected_power_product_terminal. ff_h_ftsp_induction_bad_valuation_selected_power_product_terminal + S (bpv_result_ftsp_induction_bad_valuation_selected) = S ((S (e)) * ff_v_ftsp_induction_bad_valuation_selected_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_selected_power_product_terminal. ff_u_ftsp_induction_bad_valuation_selected_power_product = ff_q_ftsp_induction_bad_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_induction_bad_valuation_selected_power_product) + (bpv_result_ftsp_induction_bad_valuation_selected))) /\ forall ff_i_ftsp_induction_bad_valuation_selected_power_product. (exists ff_lt_ftsp_induction_bad_valuation_selected_power_product_bound. ff_lt_ftsp_induction_bad_valuation_selected_power_product_bound + S ff_i_ftsp_induction_bad_valuation_selected_power_product = e) -> exists ff_p_ftsp_induction_bad_valuation_selected_power_product ff_r_ftsp_induction_bad_valuation_selected_power_product ff_s_ftsp_induction_bad_valuation_selected_power_product. ((((exists ff_h_ftsp_induction_bad_valuation_selected_power_product_factor. ff_h_ftsp_induction_bad_valuation_selected_power_product_factor + S (ff_p_ftsp_induction_bad_valuation_selected_power_product) = S ((S (ff_i_ftsp_induction_bad_valuation_selected_power_product)) * ff_c_ftsp_induction_bad_valuation_selected_power)) /\ exists ff_q_ftsp_induction_bad_valuation_selected_power_product_factor. ff_b_ftsp_induction_bad_valuation_selected_power = ff_q_ftsp_induction_bad_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_induction_bad_valuation_selected_power_product)) * ff_c_ftsp_induction_bad_valuation_selected_power) + (ff_p_ftsp_induction_bad_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_induction_bad_valuation_selected_power_product_partial. ff_h_ftsp_induction_bad_valuation_selected_power_product_partial + S (ff_r_ftsp_induction_bad_valuation_selected_power_product) = S ((S (ff_i_ftsp_induction_bad_valuation_selected_power_product)) * ff_v_ftsp_induction_bad_valuation_selected_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_selected_power_product_partial. ff_u_ftsp_induction_bad_valuation_selected_power_product = ff_q_ftsp_induction_bad_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_induction_bad_valuation_selected_power_product)) * ff_v_ftsp_induction_bad_valuation_selected_power_product) + (ff_r_ftsp_induction_bad_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_induction_bad_valuation_selected_power_product_successor. ff_h_ftsp_induction_bad_valuation_selected_power_product_successor + S (ff_s_ftsp_induction_bad_valuation_selected_power_product) = S ((S (S ff_i_ftsp_induction_bad_valuation_selected_power_product)) * ff_v_ftsp_induction_bad_valuation_selected_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_selected_power_product_successor. ff_u_ftsp_induction_bad_valuation_selected_power_product = ff_q_ftsp_induction_bad_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_induction_bad_valuation_selected_power_product)) * ff_v_ftsp_induction_bad_valuation_selected_power_product) + (ff_s_ftsp_induction_bad_valuation_selected_power_product))) /\ ff_s_ftsp_induction_bad_valuation_selected_power_product = ff_r_ftsp_induction_bad_valuation_selected_power_product * ff_p_ftsp_induction_bad_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_induction_bad_valuation_selected_divides. n = bpv_result_ftsp_induction_bad_valuation_selected * bpv_factor_ftsp_induction_bad_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_induction_bad_valuation. (exists bpv_gap_ftsp_induction_bad_valuation_candidate_bound. bpv_gap_ftsp_induction_bad_valuation_candidate_bound + bpv_candidate_ftsp_induction_bad_valuation = n) -> (exists bpv_result_ftsp_induction_bad_valuation_candidate. ((exists ff_b_ftsp_induction_bad_valuation_candidate_power ff_c_ftsp_induction_bad_valuation_candidate_power. ((forall ff_i_ftsp_induction_bad_valuation_candidate_power_repeat. (exists ff_lt_ftsp_induction_bad_valuation_candidate_power_repeat_bound. ff_lt_ftsp_induction_bad_valuation_candidate_power_repeat_bound + S ff_i_ftsp_induction_bad_valuation_candidate_power_repeat = bpv_candidate_ftsp_induction_bad_valuation) -> (((exists ff_h_ftsp_induction_bad_valuation_candidate_power_repeat_decoded. ff_h_ftsp_induction_bad_valuation_candidate_power_repeat_decoded + S (x) = S ((S (ff_i_ftsp_induction_bad_valuation_candidate_power_repeat)) * ff_c_ftsp_induction_bad_valuation_candidate_power)) /\ exists ff_q_ftsp_induction_bad_valuation_candidate_power_repeat_decoded. ff_b_ftsp_induction_bad_valuation_candidate_power = ff_q_ftsp_induction_bad_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_induction_bad_valuation_candidate_power_repeat)) * ff_c_ftsp_induction_bad_valuation_candidate_power) + (x)))) /\ (exists ff_u_ftsp_induction_bad_valuation_candidate_power_product ff_v_ftsp_induction_bad_valuation_candidate_power_product. ((((exists ff_h_ftsp_induction_bad_valuation_candidate_power_product_start. ff_h_ftsp_induction_bad_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_candidate_power_product_start. ff_u_ftsp_induction_bad_valuation_candidate_power_product = ff_q_ftsp_induction_bad_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_induction_bad_valuation_candidate_power_product_terminal. ff_h_ftsp_induction_bad_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_induction_bad_valuation_candidate) = S ((S (bpv_candidate_ftsp_induction_bad_valuation)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_candidate_power_product_terminal. ff_u_ftsp_induction_bad_valuation_candidate_power_product = ff_q_ftsp_induction_bad_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_induction_bad_valuation)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product) + (bpv_result_ftsp_induction_bad_valuation_candidate))) /\ forall ff_i_ftsp_induction_bad_valuation_candidate_power_product. (exists ff_lt_ftsp_induction_bad_valuation_candidate_power_product_bound. ff_lt_ftsp_induction_bad_valuation_candidate_power_product_bound + S ff_i_ftsp_induction_bad_valuation_candidate_power_product = bpv_candidate_ftsp_induction_bad_valuation) -> exists ff_p_ftsp_induction_bad_valuation_candidate_power_product ff_r_ftsp_induction_bad_valuation_candidate_power_product ff_s_ftsp_induction_bad_valuation_candidate_power_product. ((((exists ff_h_ftsp_induction_bad_valuation_candidate_power_product_factor. ff_h_ftsp_induction_bad_valuation_candidate_power_product_factor + S (ff_p_ftsp_induction_bad_valuation_candidate_power_product) = S ((S (ff_i_ftsp_induction_bad_valuation_candidate_power_product)) * ff_c_ftsp_induction_bad_valuation_candidate_power)) /\ exists ff_q_ftsp_induction_bad_valuation_candidate_power_product_factor. ff_b_ftsp_induction_bad_valuation_candidate_power = ff_q_ftsp_induction_bad_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_induction_bad_valuation_candidate_power_product)) * ff_c_ftsp_induction_bad_valuation_candidate_power) + (ff_p_ftsp_induction_bad_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_induction_bad_valuation_candidate_power_product_partial. ff_h_ftsp_induction_bad_valuation_candidate_power_product_partial + S (ff_r_ftsp_induction_bad_valuation_candidate_power_product) = S ((S (ff_i_ftsp_induction_bad_valuation_candidate_power_product)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_candidate_power_product_partial. ff_u_ftsp_induction_bad_valuation_candidate_power_product = ff_q_ftsp_induction_bad_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_induction_bad_valuation_candidate_power_product)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product) + (ff_r_ftsp_induction_bad_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_induction_bad_valuation_candidate_power_product_successor. ff_h_ftsp_induction_bad_valuation_candidate_power_product_successor + S (ff_s_ftsp_induction_bad_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_induction_bad_valuation_candidate_power_product)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product)) /\ exists ff_q_ftsp_induction_bad_valuation_candidate_power_product_successor. ff_u_ftsp_induction_bad_valuation_candidate_power_product = ff_q_ftsp_induction_bad_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_induction_bad_valuation_candidate_power_product)) * ff_v_ftsp_induction_bad_valuation_candidate_power_product) + (ff_s_ftsp_induction_bad_valuation_candidate_power_product))) /\ ff_s_ftsp_induction_bad_valuation_candidate_power_product = ff_r_ftsp_induction_bad_valuation_candidate_power_product * ff_p_ftsp_induction_bad_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_induction_bad_valuation_candidate_divides. n = bpv_result_ftsp_induction_bad_valuation_candidate * bpv_factor_ftsp_induction_bad_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_induction_bad_valuation_maximal. bpv_gap_ftsp_induction_bad_valuation_maximal + bpv_candidate_ftsp_induction_bad_valuation = e)) - 0102
apply power_valuation_exists - 0103
cases hvaluation - 0104
have heven : exists h. x2 = h + h - 0105
specialize hparity x - 0106
specialize hparity x2 - 0107
apply hparity - 0108
exact hfactor_witness_left - 0109
exact hchoice_right - 0110
exact hvaluation_witness - 0111
cases heven - 0112
have hdivides : exists k. n = x * k - 0113
exists x1 - 0114
exact hfactor_witness_right_witness - 0115
have hsquare : exists r. n = (x * x) * r - 0116
specialize even_positive_prime_valuation_has_square_divisor x - 0117
specialize even_positive_prime_valuation_has_square_divisor n - 0118
specialize even_positive_prime_valuation_has_square_divisor x2 - 0119
specialize even_positive_prime_valuation_has_square_divisor x3 - 0120
apply even_positive_prime_valuation_has_square_divisor - 0121
exact hfactor_witness_left - 0122
exact hnonzero - 0123
exact hvaluation_witness - 0124
exact hdivides - 0125
exact heven_witness - 0126
cases hsquare - 0127
have hsquare_quotient_nonzero : ~(x4 = 0) - 0128
intro hzero - 0129
apply hnonzero - 0130
trans (x * x) * x4 - 0131
exact hsquare_witness - 0132
rewrite hzero - 0133
apply PA5 - 0134
have hprime_nonzero : ~(x = 0) - 0135
specialize prime_nonzero x - 0136
intro hzero - 0137
apply prime_nonzero - 0138
exact hfactor_witness_left - 0139
exact hzero - 0140
have hsquare_ordered : n = x4 * (x * x) - 0141
trans (x * x) * x4 - 0142
exact hsquare_witness - 0143
apply mul_comm - 0144
have hsquare_parity : (forall ftsp_bad_prime_ftsp_induction_bad_product ftsp_bad_exponent_ftsp_induction_bad_product. ((~(ftsp_bad_prime_ftsp_induction_bad_product = 1) /\ forall frm_prime_left_ftsp_ftsp_induction_bad_product_prime frm_prime_right_ftsp_ftsp_induction_bad_product_prime. ftsp_bad_prime_ftsp_induction_bad_product = frm_prime_left_ftsp_ftsp_induction_bad_product_prime * frm_prime_right_ftsp_ftsp_induction_bad_product_prime -> frm_prime_left_ftsp_ftsp_induction_bad_product_prime = 1 \/ frm_prime_right_ftsp_ftsp_induction_bad_product_prime = 1)) -> (exists ftsc_four_three_ftsp_ftsp_induction_bad_product_three. (ftsp_bad_prime_ftsp_induction_bad_product) = 4 * ftsc_four_three_ftsp_ftsp_induction_bad_product_three + 3) -> (((exists bpv_gap_ftsp_ftsp_induction_bad_product_valuation_exponent_bound. bpv_gap_ftsp_ftsp_induction_bad_product_valuation_exponent_bound + ftsp_bad_exponent_ftsp_induction_bad_product = (x4 * (x * x))) /\ (exists bpv_result_ftsp_ftsp_induction_bad_product_valuation_selected. ((exists ff_b_ftsp_ftsp_induction_bad_product_valuation_selected_power ff_c_ftsp_ftsp_induction_bad_product_valuation_selected_power. ((forall ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat. (exists ff_lt_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat_bound. ff_lt_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat_bound + S ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat = ftsp_bad_exponent_ftsp_induction_bad_product) -> (((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat_decoded. ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_bad_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat_decoded. ff_b_ftsp_ftsp_induction_bad_product_valuation_selected_power = ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_selected_power) + (ftsp_bad_prime_ftsp_induction_bad_product)))) /\ (exists ff_u_ftsp_ftsp_induction_bad_product_valuation_selected_power_product ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_start. ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_start. ff_u_ftsp_ftsp_induction_bad_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_terminal. ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_bad_product_valuation_selected) = S ((S (ftsp_bad_exponent_ftsp_induction_bad_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_terminal. ff_u_ftsp_ftsp_induction_bad_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_ftsp_induction_bad_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) + (bpv_result_ftsp_ftsp_induction_bad_product_valuation_selected))) /\ forall ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product. (exists ff_lt_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_bound. ff_lt_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_bound + S ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product = ftsp_bad_exponent_ftsp_induction_bad_product) -> exists ff_p_ftsp_ftsp_induction_bad_product_valuation_selected_power_product ff_r_ftsp_ftsp_induction_bad_product_valuation_selected_power_product ff_s_ftsp_ftsp_induction_bad_product_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_factor. ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_factor + S (ff_p_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_factor. ff_b_ftsp_ftsp_induction_bad_product_valuation_selected_power = ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_selected_power) + (ff_p_ftsp_ftsp_induction_bad_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_partial. ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_partial + S (ff_r_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_partial. ff_u_ftsp_ftsp_induction_bad_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) + (ff_r_ftsp_ftsp_induction_bad_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_successor. ff_h_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_successor + S (ff_s_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_successor. ff_u_ftsp_ftsp_induction_bad_product_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_selected_power_product) + (ff_s_ftsp_ftsp_induction_bad_product_valuation_selected_power_product))) /\ ff_s_ftsp_ftsp_induction_bad_product_valuation_selected_power_product = ff_r_ftsp_ftsp_induction_bad_product_valuation_selected_power_product * ff_p_ftsp_ftsp_induction_bad_product_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_bad_product_valuation_selected_divides. (x4 * (x * x)) = bpv_result_ftsp_ftsp_induction_bad_product_valuation_selected * bpv_factor_ftsp_ftsp_induction_bad_product_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_ftsp_induction_bad_product_valuation. (exists bpv_gap_ftsp_ftsp_induction_bad_product_valuation_candidate_bound. bpv_gap_ftsp_ftsp_induction_bad_product_valuation_candidate_bound + bpv_candidate_ftsp_ftsp_induction_bad_product_valuation = (x4 * (x * x))) -> (exists bpv_result_ftsp_ftsp_induction_bad_product_valuation_candidate. ((exists ff_b_ftsp_ftsp_induction_bad_product_valuation_candidate_power ff_c_ftsp_ftsp_induction_bad_product_valuation_candidate_power. ((forall ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat. (exists ff_lt_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat_bound. ff_lt_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat_bound + S ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat = bpv_candidate_ftsp_ftsp_induction_bad_product_valuation) -> (((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat_decoded. ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_bad_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat_decoded. ff_b_ftsp_ftsp_induction_bad_product_valuation_candidate_power = ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_candidate_power) + (ftsp_bad_prime_ftsp_induction_bad_product)))) /\ (exists ff_u_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_start. ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_start. ff_u_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_terminal. ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_bad_product_valuation_candidate) = S ((S (bpv_candidate_ftsp_ftsp_induction_bad_product_valuation)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_terminal. ff_u_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_ftsp_induction_bad_product_valuation)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) + (bpv_result_ftsp_ftsp_induction_bad_product_valuation_candidate))) /\ forall ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product. (exists ff_lt_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_bound. ff_lt_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_bound + S ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product = bpv_candidate_ftsp_ftsp_induction_bad_product_valuation) -> exists ff_p_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product ff_r_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product ff_s_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_factor. ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_factor + S (ff_p_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_factor. ff_b_ftsp_ftsp_induction_bad_product_valuation_candidate_power = ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_bad_product_valuation_candidate_power) + (ff_p_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_partial. ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_partial + S (ff_r_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_partial. ff_u_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) + (ff_r_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_successor. ff_h_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_successor + S (ff_s_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_successor. ff_u_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product) + (ff_s_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product))) /\ ff_s_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product = ff_r_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product * ff_p_ftsp_ftsp_induction_bad_product_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_bad_product_valuation_candidate_divides. (x4 * (x * x)) = bpv_result_ftsp_ftsp_induction_bad_product_valuation_candidate * bpv_factor_ftsp_ftsp_induction_bad_product_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_ftsp_induction_bad_product_valuation_maximal. bpv_gap_ftsp_ftsp_induction_bad_product_valuation_maximal + bpv_candidate_ftsp_ftsp_induction_bad_product_valuation = ftsp_bad_exponent_ftsp_induction_bad_product)) -> exists ftsp_bad_half_ftsp_induction_bad_product. ftsp_bad_exponent_ftsp_induction_bad_product = ftsp_bad_half_ftsp_induction_bad_product + ftsp_bad_half_ftsp_induction_bad_product) - 0145
specialize all_bad_prime_even_valuation_value_eq_transport n - 0146
specialize all_bad_prime_even_valuation_value_eq_transport (x4 * (x * x)) - 0147
apply all_bad_prime_even_valuation_value_eq_transport - 0148
exact hsquare_ordered - 0149
exact hparity - 0150
have hquotient_parity : (forall ftsp_bad_prime_ftsp_induction_bad_prefix ftsp_bad_exponent_ftsp_induction_bad_prefix. ((~(ftsp_bad_prime_ftsp_induction_bad_prefix = 1) /\ forall frm_prime_left_ftsp_ftsp_induction_bad_prefix_prime frm_prime_right_ftsp_ftsp_induction_bad_prefix_prime. ftsp_bad_prime_ftsp_induction_bad_prefix = frm_prime_left_ftsp_ftsp_induction_bad_prefix_prime * frm_prime_right_ftsp_ftsp_induction_bad_prefix_prime -> frm_prime_left_ftsp_ftsp_induction_bad_prefix_prime = 1 \/ frm_prime_right_ftsp_ftsp_induction_bad_prefix_prime = 1)) -> (exists ftsc_four_three_ftsp_ftsp_induction_bad_prefix_three. (ftsp_bad_prime_ftsp_induction_bad_prefix) = 4 * ftsc_four_three_ftsp_ftsp_induction_bad_prefix_three + 3) -> (((exists bpv_gap_ftsp_ftsp_induction_bad_prefix_valuation_exponent_bound. bpv_gap_ftsp_ftsp_induction_bad_prefix_valuation_exponent_bound + ftsp_bad_exponent_ftsp_induction_bad_prefix = (x4)) /\ (exists bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_selected. ((exists ff_b_ftsp_ftsp_induction_bad_prefix_valuation_selected_power ff_c_ftsp_ftsp_induction_bad_prefix_valuation_selected_power. ((forall ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat. (exists ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat_bound. ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat_bound + S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat = ftsp_bad_exponent_ftsp_induction_bad_prefix) -> (((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat_decoded. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_bad_prefix) = S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat_decoded. ff_b_ftsp_ftsp_induction_bad_prefix_valuation_selected_power = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_selected_power) + (ftsp_bad_prime_ftsp_induction_bad_prefix)))) /\ (exists ff_u_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_start. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_start. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_terminal. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_selected) = S ((S (ftsp_bad_exponent_ftsp_induction_bad_prefix)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_terminal. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_ftsp_induction_bad_prefix)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) + (bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_selected))) /\ forall ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product. (exists ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_bound. ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_bound + S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product = ftsp_bad_exponent_ftsp_induction_bad_prefix) -> exists ff_p_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product ff_r_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product ff_s_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_factor. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_factor + S (ff_p_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_selected_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_factor. ff_b_ftsp_ftsp_induction_bad_prefix_valuation_selected_power = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_selected_power) + (ff_p_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_partial. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_partial + S (ff_r_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_partial. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) + (ff_r_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_successor. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_successor + S (ff_s_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_successor. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product) + (ff_s_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product))) /\ ff_s_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product = ff_r_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product * ff_p_ftsp_ftsp_induction_bad_prefix_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_bad_prefix_valuation_selected_divides. (x4) = bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_selected * bpv_factor_ftsp_ftsp_induction_bad_prefix_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation. (exists bpv_gap_ftsp_ftsp_induction_bad_prefix_valuation_candidate_bound. bpv_gap_ftsp_ftsp_induction_bad_prefix_valuation_candidate_bound + bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation = (x4)) -> (exists bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_candidate. ((exists ff_b_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power ff_c_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power. ((forall ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat. (exists ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat_bound. ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat_bound + S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat = bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation) -> (((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat_decoded. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_ftsp_induction_bad_prefix) = S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat_decoded. ff_b_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_repeat)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power) + (ftsp_bad_prime_ftsp_induction_bad_prefix)))) /\ (exists ff_u_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_start. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_start. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_terminal. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_candidate) = S ((S (bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_terminal. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) + (bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_candidate))) /\ forall ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product. (exists ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_bound. ff_lt_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_bound + S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product = bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation) -> exists ff_p_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product ff_r_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product ff_s_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product. ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_factor. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_factor + S (ff_p_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_factor. ff_b_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) * ff_c_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power) + (ff_p_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_partial. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_partial + S (ff_r_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) = S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_partial. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) + (ff_r_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_successor. ff_h_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_successor + S (ff_s_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) /\ exists ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_successor. ff_u_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product = ff_q_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)) * ff_v_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product) + (ff_s_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product))) /\ ff_s_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product = ff_r_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product * ff_p_ftsp_ftsp_induction_bad_prefix_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_ftsp_induction_bad_prefix_valuation_candidate_divides. (x4) = bpv_result_ftsp_ftsp_induction_bad_prefix_valuation_candidate * bpv_factor_ftsp_ftsp_induction_bad_prefix_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_ftsp_induction_bad_prefix_valuation_maximal. bpv_gap_ftsp_ftsp_induction_bad_prefix_valuation_maximal + bpv_candidate_ftsp_ftsp_induction_bad_prefix_valuation = ftsp_bad_exponent_ftsp_induction_bad_prefix)) -> exists ftsp_bad_half_ftsp_induction_bad_prefix. ftsp_bad_exponent_ftsp_induction_bad_prefix = ftsp_bad_half_ftsp_induction_bad_prefix + ftsp_bad_half_ftsp_induction_bad_prefix) - 0151
specialize all_bad_prime_even_valuations_strip_square_factor x - 0152
specialize all_bad_prime_even_valuations_strip_square_factor x4 - 0153
apply all_bad_prime_even_valuations_strip_square_factor - 0154
exact hprime_nonzero - 0155
exact hsquare_quotient_nonzero - 0156
exact hsquare_parity - 0157
have hsquare_strict : exists k. k + S x4 = (x * x) * x4 - 0158
specialize prime_square_times_nonzero_strictly_increases x - 0159
specialize prime_square_times_nonzero_strictly_increases x4 - 0160
apply prime_square_times_nonzero_strictly_increases - 0161
exact hfactor_witness_left - 0162
exact hsquare_quotient_nonzero - 0163
rewrite <- hsquare_witness at hsquare_strict - 0164
have hsquare_successor_bound : exists k. k + S x4 = S B - 0165
specialize le_trans (S x4) - 0166
specialize le_trans n - 0167
specialize le_trans (S B) - 0168
apply le_trans - 0169
exact hsquare_strict - 0170
exact hbound - 0171
have hsquare_bound : exists k. k + x4 = B - 0172
specialize le_of_succ_le_succ x4 - 0173
specialize le_of_succ_le_succ B - 0174
apply le_of_succ_le_succ - 0175
exact hsquare_successor_bound - 0176
have hquotient_representation : (exists ftsc_first_ftsp_induction_bad_prefix_result ftsc_second_ftsp_induction_bad_prefix_result. (x4) = ftsc_first_ftsp_induction_bad_prefix_result * ftsc_first_ftsp_induction_bad_prefix_result + ftsc_second_ftsp_induction_bad_prefix_result * ftsc_second_ftsp_induction_bad_prefix_result) - 0177
specialize IH x4 - 0178
apply IH - 0179
exact hsquare_bound - 0180
exact hsquare_quotient_nonzero - 0181
exact hquotient_parity - 0182
rewrite hsquare_ordered - 0183
specialize two_square_representation_preserved_by_square_factor x4 - 0184
specialize two_square_representation_preserved_by_square_factor x - 0185
apply two_square_representation_preserved_by_square_factor - 0186
exact hquotient_representation