TS002Z · theorem body

even_positive_prime_valuation_has_square_divisor

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

A positive even valuation at a prime yields an actual constructive divisor witness for the prime square.

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.

Statement with defined notation

∀ p. ∀ n. ∀ e. ∀ h. Prime(p) → ¬n = 0 → PowerValuation(p,n,e) → Dvd(p,n) → e = h + h → Dvd(p · p,n)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0004 Prime PD0046 PowerValuation

In local proof propositions

PD0002 Lt PD0044 PowerDivides
Exact expanded first-order statement
forall p n e h. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ~(n = 0) -> (((exists bpv_gap_ftsp_source_exponent_bound. bpv_gap_ftsp_source_exponent_bound + e = n) /\ (exists bpv_result_ftsp_source_selected. ((exists ff_b_ftsp_source_selected_power ff_c_ftsp_source_selected_power. ((forall ff_i_ftsp_source_selected_power_repeat. (exists ff_lt_ftsp_source_selected_power_repeat_bound. ff_lt_ftsp_source_selected_power_repeat_bound + S ff_i_ftsp_source_selected_power_repeat = e) -> (((exists ff_h_ftsp_source_selected_power_repeat_decoded. ff_h_ftsp_source_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_source_selected_power_repeat)) * ff_c_ftsp_source_selected_power)) /\ exists ff_q_ftsp_source_selected_power_repeat_decoded. ff_b_ftsp_source_selected_power = ff_q_ftsp_source_selected_power_repeat_decoded * S ((S (ff_i_ftsp_source_selected_power_repeat)) * ff_c_ftsp_source_selected_power) + (p)))) /\ (exists ff_u_ftsp_source_selected_power_product ff_v_ftsp_source_selected_power_product. ((((exists ff_h_ftsp_source_selected_power_product_start. ff_h_ftsp_source_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_start. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_start * S ((S (0)) * ff_v_ftsp_source_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_source_selected_power_product_terminal. ff_h_ftsp_source_selected_power_product_terminal + S (bpv_result_ftsp_source_selected) = S ((S (e)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_terminal. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_source_selected_power_product) + (bpv_result_ftsp_source_selected))) /\ forall ff_i_ftsp_source_selected_power_product. (exists ff_lt_ftsp_source_selected_power_product_bound. ff_lt_ftsp_source_selected_power_product_bound + S ff_i_ftsp_source_selected_power_product = e) -> exists ff_p_ftsp_source_selected_power_product ff_r_ftsp_source_selected_power_product ff_s_ftsp_source_selected_power_product. ((((exists ff_h_ftsp_source_selected_power_product_factor. ff_h_ftsp_source_selected_power_product_factor + S (ff_p_ftsp_source_selected_power_product) = S ((S (ff_i_ftsp_source_selected_power_product)) * ff_c_ftsp_source_selected_power)) /\ exists ff_q_ftsp_source_selected_power_product_factor. ff_b_ftsp_source_selected_power = ff_q_ftsp_source_selected_power_product_factor * S ((S (ff_i_ftsp_source_selected_power_product)) * ff_c_ftsp_source_selected_power) + (ff_p_ftsp_source_selected_power_product))) /\ ((((exists ff_h_ftsp_source_selected_power_product_partial. ff_h_ftsp_source_selected_power_product_partial + S (ff_r_ftsp_source_selected_power_product) = S ((S (ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_partial. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_partial * S ((S (ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product) + (ff_r_ftsp_source_selected_power_product))) /\ ((((exists ff_h_ftsp_source_selected_power_product_successor. ff_h_ftsp_source_selected_power_product_successor + S (ff_s_ftsp_source_selected_power_product) = S ((S (S ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_successor. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_successor * S ((S (S ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product) + (ff_s_ftsp_source_selected_power_product))) /\ ff_s_ftsp_source_selected_power_product = ff_r_ftsp_source_selected_power_product * ff_p_ftsp_source_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_source_selected_divides. n = bpv_result_ftsp_source_selected * bpv_factor_ftsp_source_selected_divides)))) /\ forall bpv_candidate_ftsp_source. (exists bpv_gap_ftsp_source_candidate_bound. bpv_gap_ftsp_source_candidate_bound + bpv_candidate_ftsp_source = n) -> (exists bpv_result_ftsp_source_candidate. ((exists ff_b_ftsp_source_candidate_power ff_c_ftsp_source_candidate_power. ((forall ff_i_ftsp_source_candidate_power_repeat. (exists ff_lt_ftsp_source_candidate_power_repeat_bound. ff_lt_ftsp_source_candidate_power_repeat_bound + S ff_i_ftsp_source_candidate_power_repeat = bpv_candidate_ftsp_source) -> (((exists ff_h_ftsp_source_candidate_power_repeat_decoded. ff_h_ftsp_source_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_source_candidate_power_repeat)) * ff_c_ftsp_source_candidate_power)) /\ exists ff_q_ftsp_source_candidate_power_repeat_decoded. ff_b_ftsp_source_candidate_power = ff_q_ftsp_source_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_source_candidate_power_repeat)) * ff_c_ftsp_source_candidate_power) + (p)))) /\ (exists ff_u_ftsp_source_candidate_power_product ff_v_ftsp_source_candidate_power_product. ((((exists ff_h_ftsp_source_candidate_power_product_start. ff_h_ftsp_source_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_start. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_source_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_source_candidate_power_product_terminal. ff_h_ftsp_source_candidate_power_product_terminal + S (bpv_result_ftsp_source_candidate) = S ((S (bpv_candidate_ftsp_source)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_terminal. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_source)) * ff_v_ftsp_source_candidate_power_product) + (bpv_result_ftsp_source_candidate))) /\ forall ff_i_ftsp_source_candidate_power_product. (exists ff_lt_ftsp_source_candidate_power_product_bound. ff_lt_ftsp_source_candidate_power_product_bound + S ff_i_ftsp_source_candidate_power_product = bpv_candidate_ftsp_source) -> exists ff_p_ftsp_source_candidate_power_product ff_r_ftsp_source_candidate_power_product ff_s_ftsp_source_candidate_power_product. ((((exists ff_h_ftsp_source_candidate_power_product_factor. ff_h_ftsp_source_candidate_power_product_factor + S (ff_p_ftsp_source_candidate_power_product) = S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_c_ftsp_source_candidate_power)) /\ exists ff_q_ftsp_source_candidate_power_product_factor. ff_b_ftsp_source_candidate_power = ff_q_ftsp_source_candidate_power_product_factor * S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_c_ftsp_source_candidate_power) + (ff_p_ftsp_source_candidate_power_product))) /\ ((((exists ff_h_ftsp_source_candidate_power_product_partial. ff_h_ftsp_source_candidate_power_product_partial + S (ff_r_ftsp_source_candidate_power_product) = S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_partial. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_partial * S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product) + (ff_r_ftsp_source_candidate_power_product))) /\ ((((exists ff_h_ftsp_source_candidate_power_product_successor. ff_h_ftsp_source_candidate_power_product_successor + S (ff_s_ftsp_source_candidate_power_product) = S ((S (S ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_successor. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_successor * S ((S (S ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product) + (ff_s_ftsp_source_candidate_power_product))) /\ ff_s_ftsp_source_candidate_power_product = ff_r_ftsp_source_candidate_power_product * ff_p_ftsp_source_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_source_candidate_divides. n = bpv_result_ftsp_source_candidate * bpv_factor_ftsp_source_candidate_divides))) -> (exists bpv_gap_ftsp_source_maximal. bpv_gap_ftsp_source_maximal + bpv_candidate_ftsp_source = e)) -> (exists ftcn_factor_ftsp_value. (n) = (p) * ftcn_factor_ftsp_value) -> e = h + h -> (exists ftcn_factor_ftsp_square. (n) = (p * p) * ftcn_factor_ftsp_square)

Proof neighborhood

Direct theorem prerequisites

prime_divisor_power_valuation_nonzero · Alpha closed TS002Y positive_double_at_least_two power_valuation_power_divides · Alpha closed power_divides_exponent_antitone · Alpha closed pow_two · Stable closed

Direct theorem dependents

TS0032 even_valuation_sorted_terminal_prime_has_equal_predecessor TS003C all_bad_prime_even_two_square_sufficiency_bounded

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

64 script commands · 14 reading checkpoints · 7 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
positive double at least two
01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro e
  4. L4
    intro h
  5. L5
    intro hprime
  6. L6
    intro hnonzero
  7. L7
    intro hvaluation
  8. L8
    intro hdivides
  9. L9
    intro heven
02Establish hexponentL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisor power valuation nonzero.

  1. L10
    have hexponent : ~(e = 0)
  2. L11
    specialize prime_divisor_power_valuation_nonzero p
  3. L12
    specialize prime_divisor_power_valuation_nonzero n
  4. L13
    specialize prime_divisor_power_valuation_nonzero e
  5. L14
    intro hezero
  6. L15
    apply prime_divisor_power_valuation_nonzero
  7. L16
    exact hprime
  8. L17
    exact hnonzero
  9. L18
    exact hvaluation
  10. L19
    exact hdivides
03Use earlier factsL20–20

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    exact hezero
04Establish hhalfL21–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hexponent.

  1. L21
    have hhalf : ~(h = 0)
  2. L22
    intro hhalf_zero
  3. L23
    apply hexponent
  4. L24
    trans h + h
  5. L25
    exact heven
  6. L26
    rewrite hhalf_zero
  7. L27
    rewrite hhalf_zero
  8. L28
    simp
05Establish hlowerL29–30

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hlower : Lt(1,e)Definitions: Lt(1,e)Original native command in the exact edition
  2. L30
    specialize positive_double_at_least_two h
06Establish hdoubledL31–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply positive double at least two.

  1. L31
    have hdoubled : Lt(1,h + h)Definitions: Lt(1,h + h)Original native command in the exact edition
  2. L32
    apply positive_double_at_least_two
  3. L33
    exact hhalf
  4. L34
    rewrite <- heven at hdoubled
  5. L35
    exact hdoubled
07Establish hselectedL36–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation power divides.

  1. L36
    have hselected : PowerDivides(p,e,n)Definitions: PowerDivides(p,e,n)Original native command in the exact edition
  2. L37
    specialize power_valuation_power_divides p
  3. L38
    specialize power_valuation_power_divides n
  4. L39
    specialize power_valuation_power_divides e
  5. L40
    apply power_valuation_power_divides
  6. L41
    exact hvaluation
08Establish hsquareL42–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power divides exponent antitone.

  1. L42
    have hsquare : PowerDivides(p,2,n)Definitions: PowerDivides(p,2,n)Original native command in the exact edition
  2. L43
    specialize power_divides_exponent_antitone p
  3. L44
    specialize power_divides_exponent_antitone 2
  4. L45
    specialize power_divides_exponent_antitone e
  5. L46
    specialize power_divides_exponent_antitone n
  6. L47
    apply power_divides_exponent_antitone
  7. L48
    exact hlower
  8. L49
    exact hselected
09Separate the logical casesL50–52

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L50
    cases hsquare
  2. L51
    cases hsquare_witness
  3. L52
    cases hsquare_witness_right
10Establish hpower_valueL53–59

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two.

  1. L53
    have hpower_value : x = p * p
  2. L54
    specialize pow_two p
  3. L55
    specialize pow_two 2
  4. L56
    specialize pow_two x
  5. L57
    apply pow_two
  6. L58
    refl
  7. L59
    exact hsquare_witness_left
11Construct an explicit witnessL60–60

Supply the displayed value, then prove that it has the required property.

  1. L60
    exists x1
12Calculate and transport equalitiesL61–61

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L61
    trans x * x1
13Use earlier factsL62–62

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L62
    exact hsquare_witness_right_witness
14Calculate and transport equalitiesL63–64

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L63
    rewrite hpower_value
  2. L64
    refl

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro e
  4. 0004intro h
  5. 0005intro hprime
  6. 0006intro hnonzero
  7. 0007intro hvaluation
  8. 0008intro hdivides
  9. 0009intro heven
  10. 0010have hexponent : ~(e = 0)
  11. 0011specialize prime_divisor_power_valuation_nonzero p
  12. 0012specialize prime_divisor_power_valuation_nonzero n
  13. 0013specialize prime_divisor_power_valuation_nonzero e
  14. 0014intro hezero
  15. 0015apply prime_divisor_power_valuation_nonzero
  16. 0016exact hprime
  17. 0017exact hnonzero
  18. 0018exact hvaluation
  19. 0019exact hdivides
  20. 0020exact hezero
  21. 0021have hhalf : ~(h = 0)
  22. 0022intro hhalf_zero
  23. 0023apply hexponent
  24. 0024trans h + h
  25. 0025exact heven
  26. 0026rewrite hhalf_zero
  27. 0027rewrite hhalf_zero
  28. 0028simp
  29. 0029have hlower : Lt(1,e)
    Exact native replay linehave hlower : exists k. k + 2 = e
  30. 0030specialize positive_double_at_least_two h
  31. 0031have hdoubled : Lt(1,h + h)
    Exact native replay linehave hdoubled : exists k. k + 2 = h + h
  32. 0032apply positive_double_at_least_two
  33. 0033exact hhalf
  34. 0034rewrite <- heven at hdoubled
  35. 0035exact hdoubled
  36. 0036have hselected : PowerDivides(p,e,n)
    Exact native replay linehave hselected : exists bpv_result_ftsp_selected. ((exists ff_b_ftsp_selected_power ff_c_ftsp_selected_power. ((forall ff_i_ftsp_selected_power_repeat. (exists ff_lt_ftsp_selected_power_repeat_bound. ff_lt_ftsp_selected_power_repeat_bound + S ff_i_ftsp_selected_power_repeat = e) -> (((exists ff_h_ftsp_selected_power_repeat_decoded. ff_h_ftsp_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_selected_power_repeat)) * ff_c_ftsp_selected_power)) /\ exists ff_q_ftsp_selected_power_repeat_decoded. ff_b_ftsp_selected_power = ff_q_ftsp_selected_power_repeat_decoded * S ((S (ff_i_ftsp_selected_power_repeat)) * ff_c_ftsp_selected_power) + (p)))) /\ (exists ff_u_ftsp_selected_power_product ff_v_ftsp_selected_power_product. ((((exists ff_h_ftsp_selected_power_product_start. ff_h_ftsp_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_selected_power_product)) /\ exists ff_q_ftsp_selected_power_product_start. ff_u_ftsp_selected_power_product = ff_q_ftsp_selected_power_product_start * S ((S (0)) * ff_v_ftsp_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_selected_power_product_terminal. ff_h_ftsp_selected_power_product_terminal + S (bpv_result_ftsp_selected) = S ((S (e)) * ff_v_ftsp_selected_power_product)) /\ exists ff_q_ftsp_selected_power_product_terminal. ff_u_ftsp_selected_power_product = ff_q_ftsp_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_selected_power_product) + (bpv_result_ftsp_selected))) /\ forall ff_i_ftsp_selected_power_product. (exists ff_lt_ftsp_selected_power_product_bound. ff_lt_ftsp_selected_power_product_bound + S ff_i_ftsp_selected_power_product = e) -> exists ff_p_ftsp_selected_power_product ff_r_ftsp_selected_power_product ff_s_ftsp_selected_power_product. ((((exists ff_h_ftsp_selected_power_product_factor. ff_h_ftsp_selected_power_product_factor + S (ff_p_ftsp_selected_power_product) = S ((S (ff_i_ftsp_selected_power_product)) * ff_c_ftsp_selected_power)) /\ exists ff_q_ftsp_selected_power_product_factor. ff_b_ftsp_selected_power = ff_q_ftsp_selected_power_product_factor * S ((S (ff_i_ftsp_selected_power_product)) * ff_c_ftsp_selected_power) + (ff_p_ftsp_selected_power_product))) /\ ((((exists ff_h_ftsp_selected_power_product_partial. ff_h_ftsp_selected_power_product_partial + S (ff_r_ftsp_selected_power_product) = S ((S (ff_i_ftsp_selected_power_product)) * ff_v_ftsp_selected_power_product)) /\ exists ff_q_ftsp_selected_power_product_partial. ff_u_ftsp_selected_power_product = ff_q_ftsp_selected_power_product_partial * S ((S (ff_i_ftsp_selected_power_product)) * ff_v_ftsp_selected_power_product) + (ff_r_ftsp_selected_power_product))) /\ ((((exists ff_h_ftsp_selected_power_product_successor. ff_h_ftsp_selected_power_product_successor + S (ff_s_ftsp_selected_power_product) = S ((S (S ff_i_ftsp_selected_power_product)) * ff_v_ftsp_selected_power_product)) /\ exists ff_q_ftsp_selected_power_product_successor. ff_u_ftsp_selected_power_product = ff_q_ftsp_selected_power_product_successor * S ((S (S ff_i_ftsp_selected_power_product)) * ff_v_ftsp_selected_power_product) + (ff_s_ftsp_selected_power_product))) /\ ff_s_ftsp_selected_power_product = ff_r_ftsp_selected_power_product * ff_p_ftsp_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_selected_divides. n = bpv_result_ftsp_selected * bpv_factor_ftsp_selected_divides))
  37. 0037specialize power_valuation_power_divides p
  38. 0038specialize power_valuation_power_divides n
  39. 0039specialize power_valuation_power_divides e
  40. 0040apply power_valuation_power_divides
  41. 0041exact hvaluation
  42. 0042have hsquare : PowerDivides(p,2,n)
    Exact native replay linehave hsquare : exists bpvi_result_ftsp_second. ((exists bpvi_b_ftsp_second_power bpvi_c_ftsp_second_power. ((forall bpvi_i_ftsp_second_power. (exists bpvi_repeat_gap_ftsp_second_power. bpvi_repeat_gap_ftsp_second_power + S bpvi_i_ftsp_second_power = 2) -> (((exists bpvi_h_ftsp_second_power_repeat. bpvi_h_ftsp_second_power_repeat + S (p) = S ((S (bpvi_i_ftsp_second_power)) * bpvi_c_ftsp_second_power)) /\ exists bpvi_q_ftsp_second_power_repeat. bpvi_b_ftsp_second_power = bpvi_q_ftsp_second_power_repeat * S ((S (bpvi_i_ftsp_second_power)) * bpvi_c_ftsp_second_power) + (p)))) /\ (exists bpvi_u_ftsp_second_power bpvi_v_ftsp_second_power. ((((exists bpvi_h_ftsp_second_power_start. bpvi_h_ftsp_second_power_start + S (1) = S ((S (0)) * bpvi_v_ftsp_second_power)) /\ exists bpvi_q_ftsp_second_power_start. bpvi_u_ftsp_second_power = bpvi_q_ftsp_second_power_start * S ((S (0)) * bpvi_v_ftsp_second_power) + (1))) /\ ((((exists bpvi_h_ftsp_second_power_terminal. bpvi_h_ftsp_second_power_terminal + S (bpvi_result_ftsp_second) = S ((S (2)) * bpvi_v_ftsp_second_power)) /\ exists bpvi_q_ftsp_second_power_terminal. bpvi_u_ftsp_second_power = bpvi_q_ftsp_second_power_terminal * S ((S (2)) * bpvi_v_ftsp_second_power) + (bpvi_result_ftsp_second))) /\ forall bpvi_j_ftsp_second_power. (exists bpvi_product_gap_ftsp_second_power. bpvi_product_gap_ftsp_second_power + S bpvi_j_ftsp_second_power = 2) -> exists bpvi_factor_ftsp_second_power bpvi_partial_ftsp_second_power bpvi_successor_ftsp_second_power. ((((exists bpvi_h_ftsp_second_power_factor. bpvi_h_ftsp_second_power_factor + S (bpvi_factor_ftsp_second_power) = S ((S (bpvi_j_ftsp_second_power)) * bpvi_c_ftsp_second_power)) /\ exists bpvi_q_ftsp_second_power_factor. bpvi_b_ftsp_second_power = bpvi_q_ftsp_second_power_factor * S ((S (bpvi_j_ftsp_second_power)) * bpvi_c_ftsp_second_power) + (bpvi_factor_ftsp_second_power))) /\ ((((exists bpvi_h_ftsp_second_power_partial. bpvi_h_ftsp_second_power_partial + S (bpvi_partial_ftsp_second_power) = S ((S (bpvi_j_ftsp_second_power)) * bpvi_v_ftsp_second_power)) /\ exists bpvi_q_ftsp_second_power_partial. bpvi_u_ftsp_second_power = bpvi_q_ftsp_second_power_partial * S ((S (bpvi_j_ftsp_second_power)) * bpvi_v_ftsp_second_power) + (bpvi_partial_ftsp_second_power))) /\ ((((exists bpvi_h_ftsp_second_power_successor. bpvi_h_ftsp_second_power_successor + S (bpvi_successor_ftsp_second_power) = S ((S (S bpvi_j_ftsp_second_power)) * bpvi_v_ftsp_second_power)) /\ exists bpvi_q_ftsp_second_power_successor. bpvi_u_ftsp_second_power = bpvi_q_ftsp_second_power_successor * S ((S (S bpvi_j_ftsp_second_power)) * bpvi_v_ftsp_second_power) + (bpvi_successor_ftsp_second_power))) /\ bpvi_successor_ftsp_second_power = bpvi_partial_ftsp_second_power * bpvi_factor_ftsp_second_power)))))))) /\ exists bpvi_divisor_factor_ftsp_second. n = bpvi_result_ftsp_second * bpvi_divisor_factor_ftsp_second)
  43. 0043specialize power_divides_exponent_antitone p
  44. 0044specialize power_divides_exponent_antitone 2
  45. 0045specialize power_divides_exponent_antitone e
  46. 0046specialize power_divides_exponent_antitone n
  47. 0047apply power_divides_exponent_antitone
  48. 0048exact hlower
  49. 0049exact hselected
  50. 0050cases hsquare
  51. 0051cases hsquare_witness
  52. 0052cases hsquare_witness_right
  53. 0053have hpower_value : x = p * p
  54. 0054specialize pow_two p
  55. 0055specialize pow_two 2
  56. 0056specialize pow_two x
  57. 0057apply pow_two
  58. 0058refl
  59. 0059exact hsquare_witness_left
  60. 0060exists x1
  61. 0061trans x * x1
  62. 0062exact hsquare_witness_right_witness
  63. 0063rewrite hpower_value
  64. 0064refl