BT00RL · Bertrand theorem

prime_power_valuation_one_zero

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

At a prime base, the bounded valuation of one has exponent zero.

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. ∀ one. ∀ e. one = 1 → Prime(p) → PowerValuation(p,one,e) → e = 0

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0046 PowerValuation

2 occurrences

In local proof propositions

PD0020 Pow PD0044 PowerDivides

2 occurrences

Exact expanded native-PA statement
forall p one e. one = 1 -> ((~(p = 1) /\ forall frm_prime_left_bfv_prime frm_prime_right_bfv_prime. p = frm_prime_left_bfv_prime * frm_prime_right_bfv_prime -> frm_prime_left_bfv_prime = 1 \/ frm_prime_right_bfv_prime = 1)) -> (((exists bpv_gap_bfv_one_exponent_bound. bpv_gap_bfv_one_exponent_bound + e = one) /\ (exists bpv_result_bfv_one_selected. ((exists ff_b_bfv_one_selected_power ff_c_bfv_one_selected_power. ((forall ff_i_bfv_one_selected_power_repeat. (exists ff_lt_bfv_one_selected_power_repeat_bound. ff_lt_bfv_one_selected_power_repeat_bound + S ff_i_bfv_one_selected_power_repeat = e) -> (((exists ff_h_bfv_one_selected_power_repeat_decoded. ff_h_bfv_one_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_repeat_decoded. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_repeat_decoded * S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power) + (p)))) /\ (exists ff_u_bfv_one_selected_power_product ff_v_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_start. ff_h_bfv_one_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_start. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_start * S ((S (0)) * ff_v_bfv_one_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_one_selected_power_product_terminal. ff_h_bfv_one_selected_power_product_terminal + S (bpv_result_bfv_one_selected) = S ((S (e)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_terminal. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_one_selected_power_product) + (bpv_result_bfv_one_selected))) /\ forall ff_i_bfv_one_selected_power_product. (exists ff_lt_bfv_one_selected_power_product_bound. ff_lt_bfv_one_selected_power_product_bound + S ff_i_bfv_one_selected_power_product = e) -> exists ff_p_bfv_one_selected_power_product ff_r_bfv_one_selected_power_product ff_s_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_factor. ff_h_bfv_one_selected_power_product_factor + S (ff_p_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_product_factor. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_product_factor * S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power) + (ff_p_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_partial. ff_h_bfv_one_selected_power_product_partial + S (ff_r_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_partial. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_partial * S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_r_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_successor. ff_h_bfv_one_selected_power_product_successor + S (ff_s_bfv_one_selected_power_product) = S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_successor. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_successor * S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_s_bfv_one_selected_power_product))) /\ ff_s_bfv_one_selected_power_product = ff_r_bfv_one_selected_power_product * ff_p_bfv_one_selected_power_product)))))))) /\ (exists bpv_factor_bfv_one_selected_divides. one = bpv_result_bfv_one_selected * bpv_factor_bfv_one_selected_divides)))) /\ forall bpv_candidate_bfv_one. (exists bpv_gap_bfv_one_candidate_bound. bpv_gap_bfv_one_candidate_bound + bpv_candidate_bfv_one = one) -> (exists bpv_result_bfv_one_candidate. ((exists ff_b_bfv_one_candidate_power ff_c_bfv_one_candidate_power. ((forall ff_i_bfv_one_candidate_power_repeat. (exists ff_lt_bfv_one_candidate_power_repeat_bound. ff_lt_bfv_one_candidate_power_repeat_bound + S ff_i_bfv_one_candidate_power_repeat = bpv_candidate_bfv_one) -> (((exists ff_h_bfv_one_candidate_power_repeat_decoded. ff_h_bfv_one_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_candidate_power_repeat)) * ff_c_bfv_one_candidate_power)) /\ exists ff_q_bfv_one_candidate_power_repeat_decoded. ff_b_bfv_one_candidate_power = ff_q_bfv_one_candidate_power_repeat_decoded * S ((S (ff_i_bfv_one_candidate_power_repeat)) * ff_c_bfv_one_candidate_power) + (p)))) /\ (exists ff_u_bfv_one_candidate_power_product ff_v_bfv_one_candidate_power_product. ((((exists ff_h_bfv_one_candidate_power_product_start. ff_h_bfv_one_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_start. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_start * S ((S (0)) * ff_v_bfv_one_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_one_candidate_power_product_terminal. ff_h_bfv_one_candidate_power_product_terminal + S (bpv_result_bfv_one_candidate) = S ((S (bpv_candidate_bfv_one)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_terminal. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_one)) * ff_v_bfv_one_candidate_power_product) + (bpv_result_bfv_one_candidate))) /\ forall ff_i_bfv_one_candidate_power_product. (exists ff_lt_bfv_one_candidate_power_product_bound. ff_lt_bfv_one_candidate_power_product_bound + S ff_i_bfv_one_candidate_power_product = bpv_candidate_bfv_one) -> exists ff_p_bfv_one_candidate_power_product ff_r_bfv_one_candidate_power_product ff_s_bfv_one_candidate_power_product. ((((exists ff_h_bfv_one_candidate_power_product_factor. ff_h_bfv_one_candidate_power_product_factor + S (ff_p_bfv_one_candidate_power_product) = S ((S (ff_i_bfv_one_candidate_power_product)) * ff_c_bfv_one_candidate_power)) /\ exists ff_q_bfv_one_candidate_power_product_factor. ff_b_bfv_one_candidate_power = ff_q_bfv_one_candidate_power_product_factor * S ((S (ff_i_bfv_one_candidate_power_product)) * ff_c_bfv_one_candidate_power) + (ff_p_bfv_one_candidate_power_product))) /\ ((((exists ff_h_bfv_one_candidate_power_product_partial. ff_h_bfv_one_candidate_power_product_partial + S (ff_r_bfv_one_candidate_power_product) = S ((S (ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_partial. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_partial * S ((S (ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product) + (ff_r_bfv_one_candidate_power_product))) /\ ((((exists ff_h_bfv_one_candidate_power_product_successor. ff_h_bfv_one_candidate_power_product_successor + S (ff_s_bfv_one_candidate_power_product) = S ((S (S ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_successor. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_successor * S ((S (S ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product) + (ff_s_bfv_one_candidate_power_product))) /\ ff_s_bfv_one_candidate_power_product = ff_r_bfv_one_candidate_power_product * ff_p_bfv_one_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_one_candidate_divides. one = bpv_result_bfv_one_candidate * bpv_factor_bfv_one_candidate_divides))) -> (exists bpv_gap_bfv_one_maximal. bpv_gap_bfv_one_maximal + bpv_candidate_bfv_one = e)) -> e = 0

Proof neighborhood

Direct theorem prerequisites

BT00Q9 power_valuation_power_divides BT000Q zero_or_succ BT0083 pow_successor_decompose BT0020 mul_eq_one_components

Direct theorem dependents

BT00RO prime_factorial_valuation_zero

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

56 script commands · 20 reading checkpoints · 6 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 (4)
power valuation power divideszero or succpow successor decomposemul eq one components
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro one
  3. L3
    intro e
  4. L4
    intro hone
  5. L5
    intro hp
  6. L6
    intro hvaluation
02Separate the logical casesL7–7

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

  1. L7
    cases hp
03Establish hselectedL8–13

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

  1. L8
    have hselected : PowerDivides(p,e,one)Definitions: PowerDivides(p,e,one)Original native command in the exact edition
  2. L9
    specialize power_valuation_power_divides p
  3. L10
    specialize power_valuation_power_divides one
  4. L11
    specialize power_valuation_power_divides e
  5. L12
    apply power_valuation_power_divides
  6. L13
    exact hvaluation
04Separate the logical casesL14–16

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

  1. L14
    cases hselected
  2. L15
    cases hselected_witness
  3. L16
    cases hselected_witness_right
05Use earlier factsL17–17

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

  1. L17
    specialize zero_or_succ e
06Separate the logical casesL18–18

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

  1. L18
    cases zero_or_succ
07Use earlier factsL19–19

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

  1. L19
    exact zero_or_succ_left
08Separate the logical casesL20–20

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

  1. L20
    cases zero_or_succ_right
09Establish hstepL21–28

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

  1. L21
    have hstep : ∃ R. Pow(p,x2,R) ∧ x = R · pDefinitions: Pow(p,x2,R)Original native command in the exact edition
  2. L22
    specialize pow_successor_decompose p
  3. L23
    specialize pow_successor_decompose x2
  4. L24
    specialize pow_successor_decompose e
  5. L25
    specialize pow_successor_decompose x
  6. L26
    apply pow_successor_decompose
  7. L27
    exact zero_or_succ_right_witness
  8. L28
    exact hselected_witness_left
10Separate the logical casesL29–30

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

  1. L29
    cases hstep
  2. L30
    cases hstep_witness
11Establish hresult_oneL31–33

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

  1. L31
    have hresult_one : x = 1
  2. L32
    specialize mul_eq_one_components x
  3. L33
    specialize mul_eq_one_components x1
12Establish hresult_partsL34–40

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

  1. L34
    have hresult_parts : x = 1 /\ x1 = 1
  2. L35
    apply mul_eq_one_components
  3. L36
    symm
  4. L37
    trans one
  5. L38
    symm
  6. L39
    exact hone
  7. L40
    exact hselected_witness_right_witness
13Separate the logical casesL41–41

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

  1. L41
    cases hresult_parts
14Use earlier factsL42–42

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

  1. L42
    exact hresult_parts_left
15Establish hprime_oneL43–45

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

  1. L43
    have hprime_one : p = 1
  2. L44
    specialize mul_eq_one_components x3
  3. L45
    specialize mul_eq_one_components p
16Establish hstep_partsL46–51

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

  1. L46
    have hstep_parts : x3 = 1 /\ p = 1
  2. L47
    apply mul_eq_one_components
  3. L48
    trans x
  4. L49
    symm
  5. L50
    exact hstep_witness_right
  6. L51
    exact hresult_one
17Separate the logical casesL52–52

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

  1. L52
    cases hstep_parts
18Use earlier factsL53–53

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

  1. L53
    exact hstep_parts_right
19Separate the logical casesL54–54

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

  1. L54
    exfalso
20Use earlier factsL55–56

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

  1. L55
    apply hp_left
  2. L56
    exact hprime_one

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro p
  2. 0002intro one
  3. 0003intro e
  4. 0004intro hone
  5. 0005intro hp
  6. 0006intro hvaluation
  7. 0007cases hp
  8. 0008have hselected : PowerDivides(p,e,one)
    Exact native replay linehave hselected : exists bpv_result_bfv_one_selected. ((exists ff_b_bfv_one_selected_power ff_c_bfv_one_selected_power. ((forall ff_i_bfv_one_selected_power_repeat. (exists ff_lt_bfv_one_selected_power_repeat_bound. ff_lt_bfv_one_selected_power_repeat_bound + S ff_i_bfv_one_selected_power_repeat = e) -> (((exists ff_h_bfv_one_selected_power_repeat_decoded. ff_h_bfv_one_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_repeat_decoded. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_repeat_decoded * S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power) + (p)))) /\ (exists ff_u_bfv_one_selected_power_product ff_v_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_start. ff_h_bfv_one_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_start. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_start * S ((S (0)) * ff_v_bfv_one_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_one_selected_power_product_terminal. ff_h_bfv_one_selected_power_product_terminal + S (bpv_result_bfv_one_selected) = S ((S (e)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_terminal. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_one_selected_power_product) + (bpv_result_bfv_one_selected))) /\ forall ff_i_bfv_one_selected_power_product. (exists ff_lt_bfv_one_selected_power_product_bound. ff_lt_bfv_one_selected_power_product_bound + S ff_i_bfv_one_selected_power_product = e) -> exists ff_p_bfv_one_selected_power_product ff_r_bfv_one_selected_power_product ff_s_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_factor. ff_h_bfv_one_selected_power_product_factor + S (ff_p_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_product_factor. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_product_factor * S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power) + (ff_p_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_partial. ff_h_bfv_one_selected_power_product_partial + S (ff_r_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_partial. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_partial * S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_r_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_successor. ff_h_bfv_one_selected_power_product_successor + S (ff_s_bfv_one_selected_power_product) = S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_successor. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_successor * S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_s_bfv_one_selected_power_product))) /\ ff_s_bfv_one_selected_power_product = ff_r_bfv_one_selected_power_product * ff_p_bfv_one_selected_power_product)))))))) /\ (exists bpv_factor_bfv_one_selected_divides. one = bpv_result_bfv_one_selected * bpv_factor_bfv_one_selected_divides))
  9. 0009specialize power_valuation_power_divides p
  10. 0010specialize power_valuation_power_divides one
  11. 0011specialize power_valuation_power_divides e
  12. 0012apply power_valuation_power_divides
  13. 0013exact hvaluation
  14. 0014cases hselected
  15. 0015cases hselected_witness
  16. 0016cases hselected_witness_right
  17. 0017specialize zero_or_succ e
  18. 0018cases zero_or_succ
  19. 0019exact zero_or_succ_left
  20. 0020cases zero_or_succ_right
  21. 0021have hstep : ∃ R. Pow(p,x2,R) ∧ x = R · p
    Exact native replay linehave hstep : exists R. (exists ff_b_bfv_one_prefix ff_c_bfv_one_prefix. ((forall ff_i_bfv_one_prefix_repeat. (exists ff_lt_bfv_one_prefix_repeat_bound. ff_lt_bfv_one_prefix_repeat_bound + S ff_i_bfv_one_prefix_repeat = x2) -> (((exists ff_h_bfv_one_prefix_repeat_decoded. ff_h_bfv_one_prefix_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_prefix_repeat)) * ff_c_bfv_one_prefix)) /\ exists ff_q_bfv_one_prefix_repeat_decoded. ff_b_bfv_one_prefix = ff_q_bfv_one_prefix_repeat_decoded * S ((S (ff_i_bfv_one_prefix_repeat)) * ff_c_bfv_one_prefix) + (p)))) /\ (exists ff_u_bfv_one_prefix_product ff_v_bfv_one_prefix_product. ((((exists ff_h_bfv_one_prefix_product_start. ff_h_bfv_one_prefix_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_start. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_start * S ((S (0)) * ff_v_bfv_one_prefix_product) + (1))) /\ ((((exists ff_h_bfv_one_prefix_product_terminal. ff_h_bfv_one_prefix_product_terminal + S (R) = S ((S (x2)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_terminal. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_terminal * S ((S (x2)) * ff_v_bfv_one_prefix_product) + (R))) /\ forall ff_i_bfv_one_prefix_product. (exists ff_lt_bfv_one_prefix_product_bound. ff_lt_bfv_one_prefix_product_bound + S ff_i_bfv_one_prefix_product = x2) -> exists ff_p_bfv_one_prefix_product ff_r_bfv_one_prefix_product ff_s_bfv_one_prefix_product. ((((exists ff_h_bfv_one_prefix_product_factor. ff_h_bfv_one_prefix_product_factor + S (ff_p_bfv_one_prefix_product) = S ((S (ff_i_bfv_one_prefix_product)) * ff_c_bfv_one_prefix)) /\ exists ff_q_bfv_one_prefix_product_factor. ff_b_bfv_one_prefix = ff_q_bfv_one_prefix_product_factor * S ((S (ff_i_bfv_one_prefix_product)) * ff_c_bfv_one_prefix) + (ff_p_bfv_one_prefix_product))) /\ ((((exists ff_h_bfv_one_prefix_product_partial. ff_h_bfv_one_prefix_product_partial + S (ff_r_bfv_one_prefix_product) = S ((S (ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_partial. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_partial * S ((S (ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product) + (ff_r_bfv_one_prefix_product))) /\ ((((exists ff_h_bfv_one_prefix_product_successor. ff_h_bfv_one_prefix_product_successor + S (ff_s_bfv_one_prefix_product) = S ((S (S ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_successor. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_successor * S ((S (S ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product) + (ff_s_bfv_one_prefix_product))) /\ ff_s_bfv_one_prefix_product = ff_r_bfv_one_prefix_product * ff_p_bfv_one_prefix_product)))))))) /\ x = R * p
  22. 0022specialize pow_successor_decompose p
  23. 0023specialize pow_successor_decompose x2
  24. 0024specialize pow_successor_decompose e
  25. 0025specialize pow_successor_decompose x
  26. 0026apply pow_successor_decompose
  27. 0027exact zero_or_succ_right_witness
  28. 0028exact hselected_witness_left
  29. 0029cases hstep
  30. 0030cases hstep_witness
  31. 0031have hresult_one : x = 1
  32. 0032specialize mul_eq_one_components x
  33. 0033specialize mul_eq_one_components x1
  34. 0034have hresult_parts : x = 1 /\ x1 = 1
  35. 0035apply mul_eq_one_components
  36. 0036symm
  37. 0037trans one
  38. 0038symm
  39. 0039exact hone
  40. 0040exact hselected_witness_right_witness
  41. 0041cases hresult_parts
  42. 0042exact hresult_parts_left
  43. 0043have hprime_one : p = 1
  44. 0044specialize mul_eq_one_components x3
  45. 0045specialize mul_eq_one_components p
  46. 0046have hstep_parts : x3 = 1 /\ p = 1
  47. 0047apply mul_eq_one_components
  48. 0048trans x
  49. 0049symm
  50. 0050exact hstep_witness_right
  51. 0051exact hresult_one
  52. 0052cases hstep_parts
  53. 0053exact hstep_parts_right
  54. 0054exfalso
  55. 0055apply hp_left
  56. 0056exact hprime_one