EL0016

lte_prime_self_valuation_value

Every maximal valuation of a prime at itself is exactly one, derived by actual cofactor cancellation.

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

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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ p. ∀ e. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → BoundedPowerValuation(p,p,p,e) → e = 1

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Dvd(d,n) · 2Pow(a,e,z) · 2BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_divisor_power_valuation_nonzero · checked external prerequisitemultiple_refl · checked external prerequisitenonzero_is_succ · checked external prerequisitepower_valuation_exact_cofactor · checked external prerequisitepow_successor_decompose · checked external prerequisitemul_left_cancel_nonzero · checked external prerequisitemul_one · checked external prerequisitemul_eq_one_components · checked external prerequisiteeq_decidable · checked external prerequisitelte_prime_nondivisor_onepow_positive_exponent_base_divides · checked external prerequisiteadd_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisitemul_comm · checked external prerequisiteadd_assoc · checked external prerequisitenatural_mul_swap_right_tail · checked external prerequisite
Original expanded first-order statement 
forall p e. (~((p) = 1) /\ forall pvs_left_self_prime pvs_right_self_prime. (p) = pvs_left_self_prime * pvs_right_self_prime -> pvs_left_self_prime = 1 \/ pvs_right_self_prime = 1) -> (((exists bpd_gap_pvs_self_source_selected_bound. bpd_gap_pvs_self_source_selected_bound + (e) = (p)) /\ (exists bpvi_result_pvs_self_source_selected. ((exists bpvi_b_pvs_self_source_selected_power bpvi_c_pvs_self_source_selected_power. ((forall bpvi_i_pvs_self_source_selected_power. (exists bpvi_repeat_gap_pvs_self_source_selected_power. bpvi_repeat_gap_pvs_self_source_selected_power + S bpvi_i_pvs_self_source_selected_power = e) -> (((exists bpvi_h_pvs_self_source_selected_power_repeat. bpvi_h_pvs_self_source_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_self_source_selected_power)) * bpvi_c_pvs_self_source_selected_power)) /\ exists bpvi_q_pvs_self_source_selected_power_repeat. bpvi_b_pvs_self_source_selected_power = bpvi_q_pvs_self_source_selected_power_repeat * S ((S (bpvi_i_pvs_self_source_selected_power)) * bpvi_c_pvs_self_source_selected_power) + (p)))) /\ (exists bpvi_u_pvs_self_source_selected_power bpvi_v_pvs_self_source_selected_power. ((((exists bpvi_h_pvs_self_source_selected_power_start. bpvi_h_pvs_self_source_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_self_source_selected_power)) /\ exists bpvi_q_pvs_self_source_selected_power_start. bpvi_u_pvs_self_source_selected_power = bpvi_q_pvs_self_source_selected_power_start * S ((S (0)) * bpvi_v_pvs_self_source_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_self_source_selected_power_terminal. bpvi_h_pvs_self_source_selected_power_terminal + S (bpvi_result_pvs_self_source_selected) = S ((S (e)) * bpvi_v_pvs_self_source_selected_power)) /\ exists bpvi_q_pvs_self_source_selected_power_terminal. bpvi_u_pvs_self_source_selected_power = bpvi_q_pvs_self_source_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_self_source_selected_power) + (bpvi_result_pvs_self_source_selected))) /\ forall bpvi_j_pvs_self_source_selected_power. (exists bpvi_product_gap_pvs_self_source_selected_power. bpvi_product_gap_pvs_self_source_selected_power + S bpvi_j_pvs_self_source_selected_power = e) -> exists bpvi_factor_pvs_self_source_selected_power bpvi_partial_pvs_self_source_selected_power bpvi_successor_pvs_self_source_selected_power. ((((exists bpvi_h_pvs_self_source_selected_power_factor. bpvi_h_pvs_self_source_selected_power_factor + S (bpvi_factor_pvs_self_source_selected_power) = S ((S (bpvi_j_pvs_self_source_selected_power)) * bpvi_c_pvs_self_source_selected_power)) /\ exists bpvi_q_pvs_self_source_selected_power_factor. bpvi_b_pvs_self_source_selected_power = bpvi_q_pvs_self_source_selected_power_factor * S ((S (bpvi_j_pvs_self_source_selected_power)) * bpvi_c_pvs_self_source_selected_power) + (bpvi_factor_pvs_self_source_selected_power))) /\ ((((exists bpvi_h_pvs_self_source_selected_power_partial. bpvi_h_pvs_self_source_selected_power_partial + S (bpvi_partial_pvs_self_source_selected_power) = S ((S (bpvi_j_pvs_self_source_selected_power)) * bpvi_v_pvs_self_source_selected_power)) /\ exists bpvi_q_pvs_self_source_selected_power_partial. bpvi_u_pvs_self_source_selected_power = bpvi_q_pvs_self_source_selected_power_partial * S ((S (bpvi_j_pvs_self_source_selected_power)) * bpvi_v_pvs_self_source_selected_power) + (bpvi_partial_pvs_self_source_selected_power))) /\ ((((exists bpvi_h_pvs_self_source_selected_power_successor. bpvi_h_pvs_self_source_selected_power_successor + S (bpvi_successor_pvs_self_source_selected_power) = S ((S (S bpvi_j_pvs_self_source_selected_power)) * bpvi_v_pvs_self_source_selected_power)) /\ exists bpvi_q_pvs_self_source_selected_power_successor. bpvi_u_pvs_self_source_selected_power = bpvi_q_pvs_self_source_selected_power_successor * S ((S (S bpvi_j_pvs_self_source_selected_power)) * bpvi_v_pvs_self_source_selected_power) + (bpvi_successor_pvs_self_source_selected_power))) /\ bpvi_successor_pvs_self_source_selected_power = bpvi_partial_pvs_self_source_selected_power * bpvi_factor_pvs_self_source_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_self_source_selected. p = bpvi_result_pvs_self_source_selected * bpvi_divisor_factor_pvs_self_source_selected))) /\ forall bpd_candidate_pvs_self_source. (exists bpd_gap_pvs_self_source_candidate_bound. bpd_gap_pvs_self_source_candidate_bound + (bpd_candidate_pvs_self_source) = (p)) -> (exists bpvi_result_pvs_self_source_candidate. ((exists bpvi_b_pvs_self_source_candidate_power bpvi_c_pvs_self_source_candidate_power. ((forall bpvi_i_pvs_self_source_candidate_power. (exists bpvi_repeat_gap_pvs_self_source_candidate_power. bpvi_repeat_gap_pvs_self_source_candidate_power + S bpvi_i_pvs_self_source_candidate_power = bpd_candidate_pvs_self_source) -> (((exists bpvi_h_pvs_self_source_candidate_power_repeat. bpvi_h_pvs_self_source_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_self_source_candidate_power)) * bpvi_c_pvs_self_source_candidate_power)) /\ exists bpvi_q_pvs_self_source_candidate_power_repeat. bpvi_b_pvs_self_source_candidate_power = bpvi_q_pvs_self_source_candidate_power_repeat * S ((S (bpvi_i_pvs_self_source_candidate_power)) * bpvi_c_pvs_self_source_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_self_source_candidate_power bpvi_v_pvs_self_source_candidate_power. ((((exists bpvi_h_pvs_self_source_candidate_power_start. bpvi_h_pvs_self_source_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_self_source_candidate_power)) /\ exists bpvi_q_pvs_self_source_candidate_power_start. bpvi_u_pvs_self_source_candidate_power = bpvi_q_pvs_self_source_candidate_power_start * S ((S (0)) * bpvi_v_pvs_self_source_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_self_source_candidate_power_terminal. bpvi_h_pvs_self_source_candidate_power_terminal + S (bpvi_result_pvs_self_source_candidate) = S ((S (bpd_candidate_pvs_self_source)) * bpvi_v_pvs_self_source_candidate_power)) /\ exists bpvi_q_pvs_self_source_candidate_power_terminal. bpvi_u_pvs_self_source_candidate_power = bpvi_q_pvs_self_source_candidate_power_terminal * S ((S (bpd_candidate_pvs_self_source)) * bpvi_v_pvs_self_source_candidate_power) + (bpvi_result_pvs_self_source_candidate))) /\ forall bpvi_j_pvs_self_source_candidate_power. (exists bpvi_product_gap_pvs_self_source_candidate_power. bpvi_product_gap_pvs_self_source_candidate_power + S bpvi_j_pvs_self_source_candidate_power = bpd_candidate_pvs_self_source) -> exists bpvi_factor_pvs_self_source_candidate_power bpvi_partial_pvs_self_source_candidate_power bpvi_successor_pvs_self_source_candidate_power. ((((exists bpvi_h_pvs_self_source_candidate_power_factor. bpvi_h_pvs_self_source_candidate_power_factor + S (bpvi_factor_pvs_self_source_candidate_power) = S ((S (bpvi_j_pvs_self_source_candidate_power)) * bpvi_c_pvs_self_source_candidate_power)) /\ exists bpvi_q_pvs_self_source_candidate_power_factor. bpvi_b_pvs_self_source_candidate_power = bpvi_q_pvs_self_source_candidate_power_factor * S ((S (bpvi_j_pvs_self_source_candidate_power)) * bpvi_c_pvs_self_source_candidate_power) + (bpvi_factor_pvs_self_source_candidate_power))) /\ ((((exists bpvi_h_pvs_self_source_candidate_power_partial. bpvi_h_pvs_self_source_candidate_power_partial + S (bpvi_partial_pvs_self_source_candidate_power) = S ((S (bpvi_j_pvs_self_source_candidate_power)) * bpvi_v_pvs_self_source_candidate_power)) /\ exists bpvi_q_pvs_self_source_candidate_power_partial. bpvi_u_pvs_self_source_candidate_power = bpvi_q_pvs_self_source_candidate_power_partial * S ((S (bpvi_j_pvs_self_source_candidate_power)) * bpvi_v_pvs_self_source_candidate_power) + (bpvi_partial_pvs_self_source_candidate_power))) /\ ((((exists bpvi_h_pvs_self_source_candidate_power_successor. bpvi_h_pvs_self_source_candidate_power_successor + S (bpvi_successor_pvs_self_source_candidate_power) = S ((S (S bpvi_j_pvs_self_source_candidate_power)) * bpvi_v_pvs_self_source_candidate_power)) /\ exists bpvi_q_pvs_self_source_candidate_power_successor. bpvi_u_pvs_self_source_candidate_power = bpvi_q_pvs_self_source_candidate_power_successor * S ((S (S bpvi_j_pvs_self_source_candidate_power)) * bpvi_v_pvs_self_source_candidate_power) + (bpvi_successor_pvs_self_source_candidate_power))) /\ bpvi_successor_pvs_self_source_candidate_power = bpvi_partial_pvs_self_source_candidate_power * bpvi_factor_pvs_self_source_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_self_source_candidate. p = bpvi_result_pvs_self_source_candidate * bpvi_divisor_factor_pvs_self_source_candidate)) -> (exists bpd_gap_pvs_self_source_maximal. bpd_gap_pvs_self_source_maximal + (bpd_candidate_pvs_self_source) = (e))) -> e = 1

Complete tactic proof in conservative notation

All 113 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

113 script commands · 28 reading checkpoints · 8 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)
lte prime nondivisor one
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro hp
  4. L4
    intro hval
02Establish hpzeroL5–10

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

  1. L5
    have hpzero : ~(p = 0)
  2. L6
    intro hz
  3. L7
    specialize prime_nonzero (p)
  4. L8
    apply prime_nonzero
  5. L9
    exact hp
  6. L10
    exact hz
03Establish heneL11–20

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

  1. L11
    have hene : ~(e = 0)
  2. L12
    intro hezero
  3. L13
    specialize prime_divisor_power_valuation_nonzero (p)
  4. L14
    specialize prime_divisor_power_valuation_nonzero (p)
  5. L15
    specialize prime_divisor_power_valuation_nonzero (e)
  6. L16
    apply prime_divisor_power_valuation_nonzero
  7. L17
    exact hp
  8. L18
    exact hpzero
  9. L19
    exact hval
  10. L20
    specialize multiple_refl (p)
04Use earlier factsL21–22

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

  1. L21
    apply multiple_refl
  2. L22
    exact hezero
05Establish hsuccL23–26

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

  1. L23
    have hsucc : exists k. e = S k
  2. L24
    specialize nonzero_is_succ (e)
  3. L25
    apply nonzero_is_succ
  4. L26
    exact hene
06Separate the logical casesL27–27

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

  1. L27
    cases hsucc
07Establish hcofactorL28–35

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

  1. L28
    have hcofactor : ∃ P. ∃ u. Pow(p,e,P) ∧ (p = P · u ∧ (¬u = 0 ∧ ¬Dvd(p,u)))Definitions: Pow(p,e,P)Dvd(p,u)Original native command in the exact edition
  2. L29
    specialize power_valuation_exact_cofactor (p)
  3. L30
    specialize power_valuation_exact_cofactor (p)
  4. L31
    specialize power_valuation_exact_cofactor (e)
  5. L32
    apply power_valuation_exact_cofactor
  6. L33
    exact hp
  7. L34
    exact hpzero
  8. L35
    exact hval
08Separate the logical casesL36–40

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

  1. L36
    cases hcofactor
  2. L37
    cases hcofactor_witness
  3. L38
    cases hcofactor_witness_witness
  4. L39
    cases hcofactor_witness_witness_right
  5. L40
    cases hcofactor_witness_witness_right_right
09Establish hprevL41–48

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

  1. L41
    have hprev : ∃ r. Pow(p,x,r) ∧ x1 = r · pDefinitions: Pow(p,x,r)Original native command in the exact edition
  2. L42
    specialize pow_successor_decompose (p)
  3. L43
    specialize pow_successor_decompose (x)
  4. L44
    specialize pow_successor_decompose (e)
  5. L45
    specialize pow_successor_decompose (x1)
  6. L46
    apply pow_successor_decompose
  7. L47
    exact hsucc_witness
  8. L48
    exact hcofactor_witness_witness_left
10Separate the logical casesL49–50

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

  1. L49
    cases hprev
  2. L50
    cases hprev_witness
11Establish hproductL51–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.

  1. L51
    have hproduct : 1 = x3 * x2
  2. L52
    specialize mul_left_cancel_nonzero (p)
  3. L53
    specialize mul_left_cancel_nonzero (1)
  4. L54
    specialize mul_left_cancel_nonzero (x3 * x2)
  5. L55
    apply mul_left_cancel_nonzero
  6. L56
    exact hpzero
  7. L57
    trans p
  8. L58
    apply mul_one
  9. L59
    trans x1 * x2
  10. L60
    exact hcofactor_witness_witness_right_left
12Calculate and transport equalitiesL61–65

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

  1. L61
    rewrite hprev_witness_right
  2. L62
    trans (((x3) * (((p) * (x2)))))
  3. L63
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  4. L64
    trans (((p) * (((x2) * (x3)))))
  5. L65
    trans ((p) * (((x3) * (x2))))
13Use earlier factsL66–66

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

  1. L66
    apply natural_mul_swap_right_tail
14Calculate and transport equalitiesL67–69

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

  1. L67
    congr
  2. L68
    refl
  3. L69
    trans ((x2) * (x3))
15Use earlier factsL70–70

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

  1. L70
    apply mul_comm
16Calculate and transport equalitiesL71–80

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

  1. L71
    congr
  2. L72
    refl
  3. L73
    refl
  4. L74
    trans (((p) * (((x2) * (x3)))))
  5. L75
    refl
  6. L76
    trans (((p) * (((x3) * (x2)))))
  7. L77
    symm
  8. L78
    congr
  9. L79
    refl
  10. L80
    trans ((x2) * (x3))
17Use earlier factsL81–81

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

  1. L81
    apply mul_comm
18Calculate and transport equalitiesL82–86

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

  1. L82
    congr
  2. L83
    refl
  3. L84
    refl
  4. L85
    symm
  5. L86
    simp [add_mul, mul_add, mul_assoc, add_assoc]
19Establish hcomponentsL87–92

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq one components.

  1. L87
    have hcomponents : x3 = 1 /\ x2 = 1
  2. L88
    specialize mul_eq_one_components (x3)
  3. L89
    specialize mul_eq_one_components (x2)
  4. L90
    apply mul_eq_one_components
  5. L91
    symm
  6. L92
    exact hproduct
20Separate the logical casesL93–93

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

  1. L93
    cases hcomponents
21Use earlier factsL94–95

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

  1. L94
    specialize eq_decidable x
  2. L95
    specialize eq_decidable 0
22Separate the logical casesL96–96

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

  1. L96
    cases eq_decidable
23Calculate and transport equalitiesL97–97

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

  1. L97
    trans S x
24Use earlier factsL98–98

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

  1. L98
    exact hsucc_witness
25Calculate and transport equalitiesL99–100

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

  1. L99
    rewrite eq_decidable_left
  2. L100
    refl
26Separate the logical casesL101–101

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

  1. L101
    exfalso
27Use earlier factsL102–104

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

  1. L102
    specialize lte_prime_nondivisor_one (p)
  2. L103
    apply lte_prime_nondivisor_one
  3. L104
    exact hp
28Establish hdivL105–113

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

  1. L105
  2. L106
    specialize pow_positive_exponent_base_divides (p)
  3. L107
    specialize pow_positive_exponent_base_divides (x)
  4. L108
    specialize pow_positive_exponent_base_divides (x3)
  5. L109
    apply pow_positive_exponent_base_divides
  6. L110
    exact eq_decidable_right
  7. L111
    exact hprev_witness_left
  8. L112
    rewrite hcomponents_left at hdiv
  9. L113
    exact hdiv

Library-wide reading audit

Original defined command ledger · 113 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro hp
  4. 0004intro hval
  5. 0005have hpzero : ~(p = 0)
  6. 0006intro hz
  7. 0007specialize prime_nonzero (p)
  8. 0008apply prime_nonzero
  9. 0009exact hp
  10. 0010exact hz
  11. 0011have hene : ~(e = 0)
  12. 0012intro hezero
  13. 0013specialize prime_divisor_power_valuation_nonzero (p)
  14. 0014specialize prime_divisor_power_valuation_nonzero (p)
  15. 0015specialize prime_divisor_power_valuation_nonzero (e)
  16. 0016apply prime_divisor_power_valuation_nonzero
  17. 0017exact hp
  18. 0018exact hpzero
  19. 0019exact hval
  20. 0020specialize multiple_refl (p)
  21. 0021apply multiple_refl
  22. 0022exact hezero
  23. 0023have hsucc : exists k. e = S k
  24. 0024specialize nonzero_is_succ (e)
  25. 0025apply nonzero_is_succ
  26. 0026exact hene
  27. 0027cases hsucc
  28. 0028have hcofactor : ∃ P. ∃ u. Pow(p,e,P) ∧ (p = P · u ∧ (¬u = 0 ∧ ¬Dvd(p,u)))
  29. 0029specialize power_valuation_exact_cofactor (p)
  30. 0030specialize power_valuation_exact_cofactor (p)
  31. 0031specialize power_valuation_exact_cofactor (e)
  32. 0032apply power_valuation_exact_cofactor
  33. 0033exact hp
  34. 0034exact hpzero
  35. 0035exact hval
  36. 0036cases hcofactor
  37. 0037cases hcofactor_witness
  38. 0038cases hcofactor_witness_witness
  39. 0039cases hcofactor_witness_witness_right
  40. 0040cases hcofactor_witness_witness_right_right
  41. 0041have hprev : ∃ r. Pow(p,x,r) ∧ x1 = r · p
  42. 0042specialize pow_successor_decompose (p)
  43. 0043specialize pow_successor_decompose (x)
  44. 0044specialize pow_successor_decompose (e)
  45. 0045specialize pow_successor_decompose (x1)
  46. 0046apply pow_successor_decompose
  47. 0047exact hsucc_witness
  48. 0048exact hcofactor_witness_witness_left
  49. 0049cases hprev
  50. 0050cases hprev_witness
  51. 0051have hproduct : 1 = x3 * x2
  52. 0052specialize mul_left_cancel_nonzero (p)
  53. 0053specialize mul_left_cancel_nonzero (1)
  54. 0054specialize mul_left_cancel_nonzero (x3 * x2)
  55. 0055apply mul_left_cancel_nonzero
  56. 0056exact hpzero
  57. 0057trans p
  58. 0058apply mul_one
  59. 0059trans x1 * x2
  60. 0060exact hcofactor_witness_witness_right_left
  61. 0061rewrite hprev_witness_right
  62. 0062trans (((x3) * (((p) * (x2)))))
  63. 0063simp [add_mul, mul_add, mul_assoc, add_assoc]
  64. 0064trans (((p) * (((x2) * (x3)))))
  65. 0065trans ((p) * (((x3) * (x2))))
  66. 0066apply natural_mul_swap_right_tail
  67. 0067congr
  68. 0068refl
  69. 0069trans ((x2) * (x3))
  70. 0070apply mul_comm
  71. 0071congr
  72. 0072refl
  73. 0073refl
  74. 0074trans (((p) * (((x2) * (x3)))))
  75. 0075refl
  76. 0076trans (((p) * (((x3) * (x2)))))
  77. 0077symm
  78. 0078congr
  79. 0079refl
  80. 0080trans ((x2) * (x3))
  81. 0081apply mul_comm
  82. 0082congr
  83. 0083refl
  84. 0084refl
  85. 0085symm
  86. 0086simp [add_mul, mul_add, mul_assoc, add_assoc]
  87. 0087have hcomponents : x3 = 1 /\ x2 = 1
  88. 0088specialize mul_eq_one_components (x3)
  89. 0089specialize mul_eq_one_components (x2)
  90. 0090apply mul_eq_one_components
  91. 0091symm
  92. 0092exact hproduct
  93. 0093cases hcomponents
  94. 0094specialize eq_decidable x
  95. 0095specialize eq_decidable 0
  96. 0096cases eq_decidable
  97. 0097trans S x
  98. 0098exact hsucc_witness
  99. 0099rewrite eq_decidable_left
  100. 0100refl
  101. 0101exfalso
  102. 0102specialize lte_prime_nondivisor_one (p)
  103. 0103apply lte_prime_nondivisor_one
  104. 0104exact hp
  105. 0105have hdiv : Dvd(p,x3)
  106. 0106specialize pow_positive_exponent_base_divides (p)
  107. 0107specialize pow_positive_exponent_base_divides (x)
  108. 0108specialize pow_positive_exponent_base_divides (x3)
  109. 0109apply pow_positive_exponent_base_divides
  110. 0110exact eq_decidable_right
  111. 0111exact hprev_witness_left
  112. 0112rewrite hcomponents_left at hdiv
  113. 0113exact hdiv