EL0016

lte_prime_self_valuation_value

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 18 declared prerequisites and contains 113 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_nonzero Stable theorem; checked-use authorized prime_divisor_power_valuation_nonzero Alpha theorem; checked-use authorized multiple_refl Stable theorem; checked-use authorized nonzero_is_succ Stable theorem; checked-use authorized power_valuation_exact_cofactor Alpha theorem; checked-use authorized pow_successor_decompose Stable theorem; checked-use authorized mul_left_cancel_nonzero Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized mul_eq_one_components Stable theorem; checked-use authorized eq_decidable Stable theorem; checked-use authorized EL000C lte_prime_nondivisor_one pow_positive_exponent_base_divides Alpha theorem; checked-use authorized add_mul Stable theorem; checked-use authorized mul_add Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized natural_mul_swap_right_tail Alpha theorem; checked-use authorized

Direct dependents

EL0017 lte_prime_self_valuation

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

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.

Named ingredients (1)
lte prime nondivisor one

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: DvdPow
  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
  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
    have hdiv : exists olte_factor_self_previous_divisor. (x3) = (p) * olte_factor_self_previous_divisor
  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 exact 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 : exists P u. (((exists pa_b_olte_self_cofactor pa_c_olte_self_cofactor. ((forall pa_i_olte_self_cofactor_repeat. (exists pa_lt_olte_self_cofactor_repeat_bound. pa_lt_olte_self_cofactor_repeat_bound + S pa_i_olte_self_cofactor_repeat = e) -> (((exists pa_h_olte_self_cofactor_repeat_decoded. pa_h_olte_self_cofactor_repeat_decoded + S (p) = S ((S (pa_i_olte_self_cofactor_repeat)) * pa_c_olte_self_cofactor)) /\ exists pa_q_olte_self_cofactor_repeat_decoded. pa_b_olte_self_cofactor = pa_q_olte_self_cofactor_repeat_decoded * S ((S (pa_i_olte_self_cofactor_repeat)) * pa_c_olte_self_cofactor) + (p)))) /\ (exists pa_u_olte_self_cofactor_product pa_v_olte_self_cofactor_product. ((((exists pa_h_olte_self_cofactor_product_start. pa_h_olte_self_cofactor_product_start + S (1) = S ((S (0)) * pa_v_olte_self_cofactor_product)) /\ exists pa_q_olte_self_cofactor_product_start. pa_u_olte_self_cofactor_product = pa_q_olte_self_cofactor_product_start * S ((S (0)) * pa_v_olte_self_cofactor_product) + (1))) /\ ((((exists pa_h_olte_self_cofactor_product_terminal. pa_h_olte_self_cofactor_product_terminal + S (P) = S ((S (e)) * pa_v_olte_self_cofactor_product)) /\ exists pa_q_olte_self_cofactor_product_terminal. pa_u_olte_self_cofactor_product = pa_q_olte_self_cofactor_product_terminal * S ((S (e)) * pa_v_olte_self_cofactor_product) + (P))) /\ forall pa_i_olte_self_cofactor_product. (exists pa_lt_olte_self_cofactor_product_bound. pa_lt_olte_self_cofactor_product_bound + S pa_i_olte_self_cofactor_product = e) -> exists pa_p_olte_self_cofactor_product pa_r_olte_self_cofactor_product pa_s_olte_self_cofactor_product. ((((exists pa_h_olte_self_cofactor_product_factor. pa_h_olte_self_cofactor_product_factor + S (pa_p_olte_self_cofactor_product) = S ((S (pa_i_olte_self_cofactor_product)) * pa_c_olte_self_cofactor)) /\ exists pa_q_olte_self_cofactor_product_factor. pa_b_olte_self_cofactor = pa_q_olte_self_cofactor_product_factor * S ((S (pa_i_olte_self_cofactor_product)) * pa_c_olte_self_cofactor) + (pa_p_olte_self_cofactor_product))) /\ ((((exists pa_h_olte_self_cofactor_product_partial. pa_h_olte_self_cofactor_product_partial + S (pa_r_olte_self_cofactor_product) = S ((S (pa_i_olte_self_cofactor_product)) * pa_v_olte_self_cofactor_product)) /\ exists pa_q_olte_self_cofactor_product_partial. pa_u_olte_self_cofactor_product = pa_q_olte_self_cofactor_product_partial * S ((S (pa_i_olte_self_cofactor_product)) * pa_v_olte_self_cofactor_product) + (pa_r_olte_self_cofactor_product))) /\ ((((exists pa_h_olte_self_cofactor_product_successor. pa_h_olte_self_cofactor_product_successor + S (pa_s_olte_self_cofactor_product) = S ((S (S pa_i_olte_self_cofactor_product)) * pa_v_olte_self_cofactor_product)) /\ exists pa_q_olte_self_cofactor_product_successor. pa_u_olte_self_cofactor_product = pa_q_olte_self_cofactor_product_successor * S ((S (S pa_i_olte_self_cofactor_product)) * pa_v_olte_self_cofactor_product) + (pa_s_olte_self_cofactor_product))) /\ pa_s_olte_self_cofactor_product = pa_r_olte_self_cofactor_product * pa_p_olte_self_cofactor_product)))))))) /\ (((p = P * u) /\ (((~(u = 0)) /\ (~(exists olte_factor_self_unit. (u) = (p) * olte_factor_self_unit))))))))
  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 : exists r. (exists pa_b_olte_self_previous pa_c_olte_self_previous. ((forall pa_i_olte_self_previous_repeat. (exists pa_lt_olte_self_previous_repeat_bound. pa_lt_olte_self_previous_repeat_bound + S pa_i_olte_self_previous_repeat = x) -> (((exists pa_h_olte_self_previous_repeat_decoded. pa_h_olte_self_previous_repeat_decoded + S (p) = S ((S (pa_i_olte_self_previous_repeat)) * pa_c_olte_self_previous)) /\ exists pa_q_olte_self_previous_repeat_decoded. pa_b_olte_self_previous = pa_q_olte_self_previous_repeat_decoded * S ((S (pa_i_olte_self_previous_repeat)) * pa_c_olte_self_previous) + (p)))) /\ (exists pa_u_olte_self_previous_product pa_v_olte_self_previous_product. ((((exists pa_h_olte_self_previous_product_start. pa_h_olte_self_previous_product_start + S (1) = S ((S (0)) * pa_v_olte_self_previous_product)) /\ exists pa_q_olte_self_previous_product_start. pa_u_olte_self_previous_product = pa_q_olte_self_previous_product_start * S ((S (0)) * pa_v_olte_self_previous_product) + (1))) /\ ((((exists pa_h_olte_self_previous_product_terminal. pa_h_olte_self_previous_product_terminal + S (r) = S ((S (x)) * pa_v_olte_self_previous_product)) /\ exists pa_q_olte_self_previous_product_terminal. pa_u_olte_self_previous_product = pa_q_olte_self_previous_product_terminal * S ((S (x)) * pa_v_olte_self_previous_product) + (r))) /\ forall pa_i_olte_self_previous_product. (exists pa_lt_olte_self_previous_product_bound. pa_lt_olte_self_previous_product_bound + S pa_i_olte_self_previous_product = x) -> exists pa_p_olte_self_previous_product pa_r_olte_self_previous_product pa_s_olte_self_previous_product. ((((exists pa_h_olte_self_previous_product_factor. pa_h_olte_self_previous_product_factor + S (pa_p_olte_self_previous_product) = S ((S (pa_i_olte_self_previous_product)) * pa_c_olte_self_previous)) /\ exists pa_q_olte_self_previous_product_factor. pa_b_olte_self_previous = pa_q_olte_self_previous_product_factor * S ((S (pa_i_olte_self_previous_product)) * pa_c_olte_self_previous) + (pa_p_olte_self_previous_product))) /\ ((((exists pa_h_olte_self_previous_product_partial. pa_h_olte_self_previous_product_partial + S (pa_r_olte_self_previous_product) = S ((S (pa_i_olte_self_previous_product)) * pa_v_olte_self_previous_product)) /\ exists pa_q_olte_self_previous_product_partial. pa_u_olte_self_previous_product = pa_q_olte_self_previous_product_partial * S ((S (pa_i_olte_self_previous_product)) * pa_v_olte_self_previous_product) + (pa_r_olte_self_previous_product))) /\ ((((exists pa_h_olte_self_previous_product_successor. pa_h_olte_self_previous_product_successor + S (pa_s_olte_self_previous_product) = S ((S (S pa_i_olte_self_previous_product)) * pa_v_olte_self_previous_product)) /\ exists pa_q_olte_self_previous_product_successor. pa_u_olte_self_previous_product = pa_q_olte_self_previous_product_successor * S ((S (S pa_i_olte_self_previous_product)) * pa_v_olte_self_previous_product) + (pa_s_olte_self_previous_product))) /\ pa_s_olte_self_previous_product = pa_r_olte_self_previous_product * pa_p_olte_self_previous_product)))))))) /\ 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 : exists olte_factor_self_previous_divisor. (x3) = (p) * olte_factor_self_previous_divisor
  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