BT00QP · Bertrand theorem

power_valuation_exact_cofactor

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

A prime valuation extracts a nonzero cofactor not divisible by its prime.

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. ∀ a. ∀ e. Prime(p) → ¬a = 0 → PowerValuation(p,a,e) → ∃ x. ∃ y. Pow(p,e,x) ∧ (a = x · y ∧ (¬y = 0 ∧ ¬Dvd(p,y)))

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

PD0003 Dvd PD0004 Prime PD0020 Pow PD0046 PowerValuation

4 occurrences

In local proof propositions

PD0044 PowerDivides

2 occurrences

Exact expanded native-PA statement
forall p a e. ((~(p = 1) /\ forall frm_prime_left_bpd_prime frm_prime_right_bpd_prime. p = frm_prime_left_bpd_prime * frm_prime_right_bpd_prime -> frm_prime_left_bpd_prime = 1 \/ frm_prime_right_bpd_prime = 1)) -> ~(a = 0) -> (((exists bpv_gap_bpd_valuation_a_exponent_bound. bpv_gap_bpd_valuation_a_exponent_bound + e = a) /\ (exists bpv_result_bpd_valuation_a_selected. ((exists ff_b_bpd_valuation_a_selected_power ff_c_bpd_valuation_a_selected_power. ((forall ff_i_bpd_valuation_a_selected_power_repeat. (exists ff_lt_bpd_valuation_a_selected_power_repeat_bound. ff_lt_bpd_valuation_a_selected_power_repeat_bound + S ff_i_bpd_valuation_a_selected_power_repeat = e) -> (((exists ff_h_bpd_valuation_a_selected_power_repeat_decoded. ff_h_bpd_valuation_a_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpd_valuation_a_selected_power_repeat)) * ff_c_bpd_valuation_a_selected_power)) /\ exists ff_q_bpd_valuation_a_selected_power_repeat_decoded. ff_b_bpd_valuation_a_selected_power = ff_q_bpd_valuation_a_selected_power_repeat_decoded * S ((S (ff_i_bpd_valuation_a_selected_power_repeat)) * ff_c_bpd_valuation_a_selected_power) + (p)))) /\ (exists ff_u_bpd_valuation_a_selected_power_product ff_v_bpd_valuation_a_selected_power_product. ((((exists ff_h_bpd_valuation_a_selected_power_product_start. ff_h_bpd_valuation_a_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpd_valuation_a_selected_power_product)) /\ exists ff_q_bpd_valuation_a_selected_power_product_start. ff_u_bpd_valuation_a_selected_power_product = ff_q_bpd_valuation_a_selected_power_product_start * S ((S (0)) * ff_v_bpd_valuation_a_selected_power_product) + (1))) /\ ((((exists ff_h_bpd_valuation_a_selected_power_product_terminal. ff_h_bpd_valuation_a_selected_power_product_terminal + S (bpv_result_bpd_valuation_a_selected) = S ((S (e)) * ff_v_bpd_valuation_a_selected_power_product)) /\ exists ff_q_bpd_valuation_a_selected_power_product_terminal. ff_u_bpd_valuation_a_selected_power_product = ff_q_bpd_valuation_a_selected_power_product_terminal * S ((S (e)) * ff_v_bpd_valuation_a_selected_power_product) + (bpv_result_bpd_valuation_a_selected))) /\ forall ff_i_bpd_valuation_a_selected_power_product. (exists ff_lt_bpd_valuation_a_selected_power_product_bound. ff_lt_bpd_valuation_a_selected_power_product_bound + S ff_i_bpd_valuation_a_selected_power_product = e) -> exists ff_p_bpd_valuation_a_selected_power_product ff_r_bpd_valuation_a_selected_power_product ff_s_bpd_valuation_a_selected_power_product. ((((exists ff_h_bpd_valuation_a_selected_power_product_factor. ff_h_bpd_valuation_a_selected_power_product_factor + S (ff_p_bpd_valuation_a_selected_power_product) = S ((S (ff_i_bpd_valuation_a_selected_power_product)) * ff_c_bpd_valuation_a_selected_power)) /\ exists ff_q_bpd_valuation_a_selected_power_product_factor. ff_b_bpd_valuation_a_selected_power = ff_q_bpd_valuation_a_selected_power_product_factor * S ((S (ff_i_bpd_valuation_a_selected_power_product)) * ff_c_bpd_valuation_a_selected_power) + (ff_p_bpd_valuation_a_selected_power_product))) /\ ((((exists ff_h_bpd_valuation_a_selected_power_product_partial. ff_h_bpd_valuation_a_selected_power_product_partial + S (ff_r_bpd_valuation_a_selected_power_product) = S ((S (ff_i_bpd_valuation_a_selected_power_product)) * ff_v_bpd_valuation_a_selected_power_product)) /\ exists ff_q_bpd_valuation_a_selected_power_product_partial. ff_u_bpd_valuation_a_selected_power_product = ff_q_bpd_valuation_a_selected_power_product_partial * S ((S (ff_i_bpd_valuation_a_selected_power_product)) * ff_v_bpd_valuation_a_selected_power_product) + (ff_r_bpd_valuation_a_selected_power_product))) /\ ((((exists ff_h_bpd_valuation_a_selected_power_product_successor. ff_h_bpd_valuation_a_selected_power_product_successor + S (ff_s_bpd_valuation_a_selected_power_product) = S ((S (S ff_i_bpd_valuation_a_selected_power_product)) * ff_v_bpd_valuation_a_selected_power_product)) /\ exists ff_q_bpd_valuation_a_selected_power_product_successor. ff_u_bpd_valuation_a_selected_power_product = ff_q_bpd_valuation_a_selected_power_product_successor * S ((S (S ff_i_bpd_valuation_a_selected_power_product)) * ff_v_bpd_valuation_a_selected_power_product) + (ff_s_bpd_valuation_a_selected_power_product))) /\ ff_s_bpd_valuation_a_selected_power_product = ff_r_bpd_valuation_a_selected_power_product * ff_p_bpd_valuation_a_selected_power_product)))))))) /\ (exists bpv_factor_bpd_valuation_a_selected_divides. a = bpv_result_bpd_valuation_a_selected * bpv_factor_bpd_valuation_a_selected_divides)))) /\ forall bpv_candidate_bpd_valuation_a. (exists bpv_gap_bpd_valuation_a_candidate_bound. bpv_gap_bpd_valuation_a_candidate_bound + bpv_candidate_bpd_valuation_a = a) -> (exists bpv_result_bpd_valuation_a_candidate. ((exists ff_b_bpd_valuation_a_candidate_power ff_c_bpd_valuation_a_candidate_power. ((forall ff_i_bpd_valuation_a_candidate_power_repeat. (exists ff_lt_bpd_valuation_a_candidate_power_repeat_bound. ff_lt_bpd_valuation_a_candidate_power_repeat_bound + S ff_i_bpd_valuation_a_candidate_power_repeat = bpv_candidate_bpd_valuation_a) -> (((exists ff_h_bpd_valuation_a_candidate_power_repeat_decoded. ff_h_bpd_valuation_a_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bpd_valuation_a_candidate_power_repeat)) * ff_c_bpd_valuation_a_candidate_power)) /\ exists ff_q_bpd_valuation_a_candidate_power_repeat_decoded. ff_b_bpd_valuation_a_candidate_power = ff_q_bpd_valuation_a_candidate_power_repeat_decoded * S ((S (ff_i_bpd_valuation_a_candidate_power_repeat)) * ff_c_bpd_valuation_a_candidate_power) + (p)))) /\ (exists ff_u_bpd_valuation_a_candidate_power_product ff_v_bpd_valuation_a_candidate_power_product. ((((exists ff_h_bpd_valuation_a_candidate_power_product_start. ff_h_bpd_valuation_a_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpd_valuation_a_candidate_power_product)) /\ exists ff_q_bpd_valuation_a_candidate_power_product_start. ff_u_bpd_valuation_a_candidate_power_product = ff_q_bpd_valuation_a_candidate_power_product_start * S ((S (0)) * ff_v_bpd_valuation_a_candidate_power_product) + (1))) /\ ((((exists ff_h_bpd_valuation_a_candidate_power_product_terminal. ff_h_bpd_valuation_a_candidate_power_product_terminal + S (bpv_result_bpd_valuation_a_candidate) = S ((S (bpv_candidate_bpd_valuation_a)) * ff_v_bpd_valuation_a_candidate_power_product)) /\ exists ff_q_bpd_valuation_a_candidate_power_product_terminal. ff_u_bpd_valuation_a_candidate_power_product = ff_q_bpd_valuation_a_candidate_power_product_terminal * S ((S (bpv_candidate_bpd_valuation_a)) * ff_v_bpd_valuation_a_candidate_power_product) + (bpv_result_bpd_valuation_a_candidate))) /\ forall ff_i_bpd_valuation_a_candidate_power_product. (exists ff_lt_bpd_valuation_a_candidate_power_product_bound. ff_lt_bpd_valuation_a_candidate_power_product_bound + S ff_i_bpd_valuation_a_candidate_power_product = bpv_candidate_bpd_valuation_a) -> exists ff_p_bpd_valuation_a_candidate_power_product ff_r_bpd_valuation_a_candidate_power_product ff_s_bpd_valuation_a_candidate_power_product. ((((exists ff_h_bpd_valuation_a_candidate_power_product_factor. ff_h_bpd_valuation_a_candidate_power_product_factor + S (ff_p_bpd_valuation_a_candidate_power_product) = S ((S (ff_i_bpd_valuation_a_candidate_power_product)) * ff_c_bpd_valuation_a_candidate_power)) /\ exists ff_q_bpd_valuation_a_candidate_power_product_factor. ff_b_bpd_valuation_a_candidate_power = ff_q_bpd_valuation_a_candidate_power_product_factor * S ((S (ff_i_bpd_valuation_a_candidate_power_product)) * ff_c_bpd_valuation_a_candidate_power) + (ff_p_bpd_valuation_a_candidate_power_product))) /\ ((((exists ff_h_bpd_valuation_a_candidate_power_product_partial. ff_h_bpd_valuation_a_candidate_power_product_partial + S (ff_r_bpd_valuation_a_candidate_power_product) = S ((S (ff_i_bpd_valuation_a_candidate_power_product)) * ff_v_bpd_valuation_a_candidate_power_product)) /\ exists ff_q_bpd_valuation_a_candidate_power_product_partial. ff_u_bpd_valuation_a_candidate_power_product = ff_q_bpd_valuation_a_candidate_power_product_partial * S ((S (ff_i_bpd_valuation_a_candidate_power_product)) * ff_v_bpd_valuation_a_candidate_power_product) + (ff_r_bpd_valuation_a_candidate_power_product))) /\ ((((exists ff_h_bpd_valuation_a_candidate_power_product_successor. ff_h_bpd_valuation_a_candidate_power_product_successor + S (ff_s_bpd_valuation_a_candidate_power_product) = S ((S (S ff_i_bpd_valuation_a_candidate_power_product)) * ff_v_bpd_valuation_a_candidate_power_product)) /\ exists ff_q_bpd_valuation_a_candidate_power_product_successor. ff_u_bpd_valuation_a_candidate_power_product = ff_q_bpd_valuation_a_candidate_power_product_successor * S ((S (S ff_i_bpd_valuation_a_candidate_power_product)) * ff_v_bpd_valuation_a_candidate_power_product) + (ff_s_bpd_valuation_a_candidate_power_product))) /\ ff_s_bpd_valuation_a_candidate_power_product = ff_r_bpd_valuation_a_candidate_power_product * ff_p_bpd_valuation_a_candidate_power_product)))))))) /\ (exists bpv_factor_bpd_valuation_a_candidate_divides. a = bpv_result_bpd_valuation_a_candidate * bpv_factor_bpd_valuation_a_candidate_divides))) -> (exists bpv_gap_bpd_valuation_a_maximal. bpv_gap_bpd_valuation_a_maximal + bpv_candidate_bpd_valuation_a = e)) -> (exists bpd_result_valuation_exact bpd_cofactor_valuation_exact. ((exists ff_b_valuation_exact_power ff_c_valuation_exact_power. ((forall ff_i_valuation_exact_power_repeat. (exists ff_lt_valuation_exact_power_repeat_bound. ff_lt_valuation_exact_power_repeat_bound + S ff_i_valuation_exact_power_repeat = e) -> (((exists ff_h_valuation_exact_power_repeat_decoded. ff_h_valuation_exact_power_repeat_decoded + S (p) = S ((S (ff_i_valuation_exact_power_repeat)) * ff_c_valuation_exact_power)) /\ exists ff_q_valuation_exact_power_repeat_decoded. ff_b_valuation_exact_power = ff_q_valuation_exact_power_repeat_decoded * S ((S (ff_i_valuation_exact_power_repeat)) * ff_c_valuation_exact_power) + (p)))) /\ (exists ff_u_valuation_exact_power_product ff_v_valuation_exact_power_product. ((((exists ff_h_valuation_exact_power_product_start. ff_h_valuation_exact_power_product_start + S (1) = S ((S (0)) * ff_v_valuation_exact_power_product)) /\ exists ff_q_valuation_exact_power_product_start. ff_u_valuation_exact_power_product = ff_q_valuation_exact_power_product_start * S ((S (0)) * ff_v_valuation_exact_power_product) + (1))) /\ ((((exists ff_h_valuation_exact_power_product_terminal. ff_h_valuation_exact_power_product_terminal + S (bpd_result_valuation_exact) = S ((S (e)) * ff_v_valuation_exact_power_product)) /\ exists ff_q_valuation_exact_power_product_terminal. ff_u_valuation_exact_power_product = ff_q_valuation_exact_power_product_terminal * S ((S (e)) * ff_v_valuation_exact_power_product) + (bpd_result_valuation_exact))) /\ forall ff_i_valuation_exact_power_product. (exists ff_lt_valuation_exact_power_product_bound. ff_lt_valuation_exact_power_product_bound + S ff_i_valuation_exact_power_product = e) -> exists ff_p_valuation_exact_power_product ff_r_valuation_exact_power_product ff_s_valuation_exact_power_product. ((((exists ff_h_valuation_exact_power_product_factor. ff_h_valuation_exact_power_product_factor + S (ff_p_valuation_exact_power_product) = S ((S (ff_i_valuation_exact_power_product)) * ff_c_valuation_exact_power)) /\ exists ff_q_valuation_exact_power_product_factor. ff_b_valuation_exact_power = ff_q_valuation_exact_power_product_factor * S ((S (ff_i_valuation_exact_power_product)) * ff_c_valuation_exact_power) + (ff_p_valuation_exact_power_product))) /\ ((((exists ff_h_valuation_exact_power_product_partial. ff_h_valuation_exact_power_product_partial + S (ff_r_valuation_exact_power_product) = S ((S (ff_i_valuation_exact_power_product)) * ff_v_valuation_exact_power_product)) /\ exists ff_q_valuation_exact_power_product_partial. ff_u_valuation_exact_power_product = ff_q_valuation_exact_power_product_partial * S ((S (ff_i_valuation_exact_power_product)) * ff_v_valuation_exact_power_product) + (ff_r_valuation_exact_power_product))) /\ ((((exists ff_h_valuation_exact_power_product_successor. ff_h_valuation_exact_power_product_successor + S (ff_s_valuation_exact_power_product) = S ((S (S ff_i_valuation_exact_power_product)) * ff_v_valuation_exact_power_product)) /\ exists ff_q_valuation_exact_power_product_successor. ff_u_valuation_exact_power_product = ff_q_valuation_exact_power_product_successor * S ((S (S ff_i_valuation_exact_power_product)) * ff_v_valuation_exact_power_product) + (ff_s_valuation_exact_power_product))) /\ ff_s_valuation_exact_power_product = ff_r_valuation_exact_power_product * ff_p_valuation_exact_power_product)))))))) /\ ((a = bpd_result_valuation_exact * bpd_cofactor_valuation_exact) /\ ((~(bpd_cofactor_valuation_exact = 0)) /\ (~(exists bpd_factor_valuation_exact_prime. bpd_cofactor_valuation_exact = (p) * bpd_factor_valuation_exact_prime))))))

Proof neighborhood

Direct theorem prerequisites

BT00QI power_valuation_selected_and_successor_not_divides BT00QM power_divides_successor_of_cofactor

Direct theorem dependents

BT00QQ power_valuation_mul_successor_not_divides

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

42 script commands · 17 reading checkpoints · 1 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 (2)
power valuation selected and successor not dividespower divides successor of cofactor
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro e
  4. L4
    intro hp
  5. L5
    intro ha
  6. L6
    intro hvaluation
02Establish hcharacterizationL7–14

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

  1. L7
    have hcharacterization : PowerDivides(p,e,a) ∧ ¬PowerDivides(p,S e,a)Definitions: PowerDivides(p,e,a)PowerDivides(p,S e,a)Original native command in the exact edition
  2. L8
    specialize power_valuation_selected_and_successor_not_divides p
  3. L9
    specialize power_valuation_selected_and_successor_not_divides a
  4. L10
    specialize power_valuation_selected_and_successor_not_divides e
  5. L11
    apply power_valuation_selected_and_successor_not_divides
  6. L12
    exact hp
  7. L13
    exact ha
  8. L14
    exact hvaluation
03Separate the logical casesL15–18

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

  1. L15
    cases hcharacterization
  2. L16
    cases hcharacterization_left
  3. L17
    cases hcharacterization_left_witness
  4. L18
    cases hcharacterization_left_witness_right
04Construct an explicit witnessL19–20

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

  1. L19
    exists x
  2. L20
    exists x1
05Separate the logical casesL21–21

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

  1. L21
    split
06Use earlier factsL22–22

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

  1. L22
    exact hcharacterization_left_witness_left
07Separate the logical casesL23–23

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

  1. L23
    split
08Use earlier factsL24–24

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

  1. L24
    exact hcharacterization_left_witness_right_witness
09Separate the logical casesL25–25

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

  1. L25
    split
10Fix variables and assumptionsL26–26

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

  1. L26
    intro hcofactor_zero
11Use earlier factsL27–27

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

  1. L27
    apply ha
12Calculate and transport equalitiesL28–28

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

  1. L28
    trans x * x1
13Use earlier factsL29–29

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

  1. L29
    exact hcharacterization_left_witness_right_witness
14Calculate and transport equalitiesL30–30

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

  1. L30
    rewrite hcofactor_zero
15Use earlier factsL31–31

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

  1. L31
    apply PA5
16Fix variables and assumptionsL32–32

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

  1. L32
    intro hcofactor_prime
17Use earlier factsL33–42

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

  1. L33
    apply hcharacterization_right
  2. L34
    specialize power_divides_successor_of_cofactor p
  3. L35
    specialize power_divides_successor_of_cofactor e
  4. L36
    specialize power_divides_successor_of_cofactor a
  5. L37
    specialize power_divides_successor_of_cofactor x
  6. L38
    specialize power_divides_successor_of_cofactor x1
  7. L39
    apply power_divides_successor_of_cofactor
  8. L40
    exact hcharacterization_left_witness_left
  9. L41
    exact hcharacterization_left_witness_right_witness
  10. L42
    exact hcofactor_prime

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro ha
  6. 0006intro hvaluation
  7. 0007have hcharacterization : PowerDivides(p,e,a) ∧ ¬PowerDivides(p,S e,a)
    Exact native replay linehave hcharacterization : (exists bpv_result_bpd_exact_selected. ((exists ff_b_bpd_exact_selected_power ff_c_bpd_exact_selected_power. ((forall ff_i_bpd_exact_selected_power_repeat. (exists ff_lt_bpd_exact_selected_power_repeat_bound. ff_lt_bpd_exact_selected_power_repeat_bound + S ff_i_bpd_exact_selected_power_repeat = e) -> (((exists ff_h_bpd_exact_selected_power_repeat_decoded. ff_h_bpd_exact_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpd_exact_selected_power_repeat)) * ff_c_bpd_exact_selected_power)) /\ exists ff_q_bpd_exact_selected_power_repeat_decoded. ff_b_bpd_exact_selected_power = ff_q_bpd_exact_selected_power_repeat_decoded * S ((S (ff_i_bpd_exact_selected_power_repeat)) * ff_c_bpd_exact_selected_power) + (p)))) /\ (exists ff_u_bpd_exact_selected_power_product ff_v_bpd_exact_selected_power_product. ((((exists ff_h_bpd_exact_selected_power_product_start. ff_h_bpd_exact_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpd_exact_selected_power_product)) /\ exists ff_q_bpd_exact_selected_power_product_start. ff_u_bpd_exact_selected_power_product = ff_q_bpd_exact_selected_power_product_start * S ((S (0)) * ff_v_bpd_exact_selected_power_product) + (1))) /\ ((((exists ff_h_bpd_exact_selected_power_product_terminal. ff_h_bpd_exact_selected_power_product_terminal + S (bpv_result_bpd_exact_selected) = S ((S (e)) * ff_v_bpd_exact_selected_power_product)) /\ exists ff_q_bpd_exact_selected_power_product_terminal. ff_u_bpd_exact_selected_power_product = ff_q_bpd_exact_selected_power_product_terminal * S ((S (e)) * ff_v_bpd_exact_selected_power_product) + (bpv_result_bpd_exact_selected))) /\ forall ff_i_bpd_exact_selected_power_product. (exists ff_lt_bpd_exact_selected_power_product_bound. ff_lt_bpd_exact_selected_power_product_bound + S ff_i_bpd_exact_selected_power_product = e) -> exists ff_p_bpd_exact_selected_power_product ff_r_bpd_exact_selected_power_product ff_s_bpd_exact_selected_power_product. ((((exists ff_h_bpd_exact_selected_power_product_factor. ff_h_bpd_exact_selected_power_product_factor + S (ff_p_bpd_exact_selected_power_product) = S ((S (ff_i_bpd_exact_selected_power_product)) * ff_c_bpd_exact_selected_power)) /\ exists ff_q_bpd_exact_selected_power_product_factor. ff_b_bpd_exact_selected_power = ff_q_bpd_exact_selected_power_product_factor * S ((S (ff_i_bpd_exact_selected_power_product)) * ff_c_bpd_exact_selected_power) + (ff_p_bpd_exact_selected_power_product))) /\ ((((exists ff_h_bpd_exact_selected_power_product_partial. ff_h_bpd_exact_selected_power_product_partial + S (ff_r_bpd_exact_selected_power_product) = S ((S (ff_i_bpd_exact_selected_power_product)) * ff_v_bpd_exact_selected_power_product)) /\ exists ff_q_bpd_exact_selected_power_product_partial. ff_u_bpd_exact_selected_power_product = ff_q_bpd_exact_selected_power_product_partial * S ((S (ff_i_bpd_exact_selected_power_product)) * ff_v_bpd_exact_selected_power_product) + (ff_r_bpd_exact_selected_power_product))) /\ ((((exists ff_h_bpd_exact_selected_power_product_successor. ff_h_bpd_exact_selected_power_product_successor + S (ff_s_bpd_exact_selected_power_product) = S ((S (S ff_i_bpd_exact_selected_power_product)) * ff_v_bpd_exact_selected_power_product)) /\ exists ff_q_bpd_exact_selected_power_product_successor. ff_u_bpd_exact_selected_power_product = ff_q_bpd_exact_selected_power_product_successor * S ((S (S ff_i_bpd_exact_selected_power_product)) * ff_v_bpd_exact_selected_power_product) + (ff_s_bpd_exact_selected_power_product))) /\ ff_s_bpd_exact_selected_power_product = ff_r_bpd_exact_selected_power_product * ff_p_bpd_exact_selected_power_product)))))))) /\ (exists bpv_factor_bpd_exact_selected_divides. a = bpv_result_bpd_exact_selected * bpv_factor_bpd_exact_selected_divides))) /\ ~(exists bpvi_result_bpd_exact_successor. ((exists bpvi_b_bpd_exact_successor_power bpvi_c_bpd_exact_successor_power. ((forall bpvi_i_bpd_exact_successor_power. (exists bpvi_repeat_gap_bpd_exact_successor_power. bpvi_repeat_gap_bpd_exact_successor_power + S bpvi_i_bpd_exact_successor_power = S e) -> (((exists bpvi_h_bpd_exact_successor_power_repeat. bpvi_h_bpd_exact_successor_power_repeat + S (p) = S ((S (bpvi_i_bpd_exact_successor_power)) * bpvi_c_bpd_exact_successor_power)) /\ exists bpvi_q_bpd_exact_successor_power_repeat. bpvi_b_bpd_exact_successor_power = bpvi_q_bpd_exact_successor_power_repeat * S ((S (bpvi_i_bpd_exact_successor_power)) * bpvi_c_bpd_exact_successor_power) + (p)))) /\ (exists bpvi_u_bpd_exact_successor_power bpvi_v_bpd_exact_successor_power. ((((exists bpvi_h_bpd_exact_successor_power_start. bpvi_h_bpd_exact_successor_power_start + S (1) = S ((S (0)) * bpvi_v_bpd_exact_successor_power)) /\ exists bpvi_q_bpd_exact_successor_power_start. bpvi_u_bpd_exact_successor_power = bpvi_q_bpd_exact_successor_power_start * S ((S (0)) * bpvi_v_bpd_exact_successor_power) + (1))) /\ ((((exists bpvi_h_bpd_exact_successor_power_terminal. bpvi_h_bpd_exact_successor_power_terminal + S (bpvi_result_bpd_exact_successor) = S ((S (S e)) * bpvi_v_bpd_exact_successor_power)) /\ exists bpvi_q_bpd_exact_successor_power_terminal. bpvi_u_bpd_exact_successor_power = bpvi_q_bpd_exact_successor_power_terminal * S ((S (S e)) * bpvi_v_bpd_exact_successor_power) + (bpvi_result_bpd_exact_successor))) /\ forall bpvi_j_bpd_exact_successor_power. (exists bpvi_product_gap_bpd_exact_successor_power. bpvi_product_gap_bpd_exact_successor_power + S bpvi_j_bpd_exact_successor_power = S e) -> exists bpvi_factor_bpd_exact_successor_power bpvi_partial_bpd_exact_successor_power bpvi_successor_bpd_exact_successor_power. ((((exists bpvi_h_bpd_exact_successor_power_factor. bpvi_h_bpd_exact_successor_power_factor + S (bpvi_factor_bpd_exact_successor_power) = S ((S (bpvi_j_bpd_exact_successor_power)) * bpvi_c_bpd_exact_successor_power)) /\ exists bpvi_q_bpd_exact_successor_power_factor. bpvi_b_bpd_exact_successor_power = bpvi_q_bpd_exact_successor_power_factor * S ((S (bpvi_j_bpd_exact_successor_power)) * bpvi_c_bpd_exact_successor_power) + (bpvi_factor_bpd_exact_successor_power))) /\ ((((exists bpvi_h_bpd_exact_successor_power_partial. bpvi_h_bpd_exact_successor_power_partial + S (bpvi_partial_bpd_exact_successor_power) = S ((S (bpvi_j_bpd_exact_successor_power)) * bpvi_v_bpd_exact_successor_power)) /\ exists bpvi_q_bpd_exact_successor_power_partial. bpvi_u_bpd_exact_successor_power = bpvi_q_bpd_exact_successor_power_partial * S ((S (bpvi_j_bpd_exact_successor_power)) * bpvi_v_bpd_exact_successor_power) + (bpvi_partial_bpd_exact_successor_power))) /\ ((((exists bpvi_h_bpd_exact_successor_power_successor. bpvi_h_bpd_exact_successor_power_successor + S (bpvi_successor_bpd_exact_successor_power) = S ((S (S bpvi_j_bpd_exact_successor_power)) * bpvi_v_bpd_exact_successor_power)) /\ exists bpvi_q_bpd_exact_successor_power_successor. bpvi_u_bpd_exact_successor_power = bpvi_q_bpd_exact_successor_power_successor * S ((S (S bpvi_j_bpd_exact_successor_power)) * bpvi_v_bpd_exact_successor_power) + (bpvi_successor_bpd_exact_successor_power))) /\ bpvi_successor_bpd_exact_successor_power = bpvi_partial_bpd_exact_successor_power * bpvi_factor_bpd_exact_successor_power)))))))) /\ exists bpvi_divisor_factor_bpd_exact_successor. a = bpvi_result_bpd_exact_successor * bpvi_divisor_factor_bpd_exact_successor))
  8. 0008specialize power_valuation_selected_and_successor_not_divides p
  9. 0009specialize power_valuation_selected_and_successor_not_divides a
  10. 0010specialize power_valuation_selected_and_successor_not_divides e
  11. 0011apply power_valuation_selected_and_successor_not_divides
  12. 0012exact hp
  13. 0013exact ha
  14. 0014exact hvaluation
  15. 0015cases hcharacterization
  16. 0016cases hcharacterization_left
  17. 0017cases hcharacterization_left_witness
  18. 0018cases hcharacterization_left_witness_right
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022exact hcharacterization_left_witness_left
  23. 0023split
  24. 0024exact hcharacterization_left_witness_right_witness
  25. 0025split
  26. 0026intro hcofactor_zero
  27. 0027apply ha
  28. 0028trans x * x1
  29. 0029exact hcharacterization_left_witness_right_witness
  30. 0030rewrite hcofactor_zero
  31. 0031apply PA5
  32. 0032intro hcofactor_prime
  33. 0033apply hcharacterization_right
  34. 0034specialize power_divides_successor_of_cofactor p
  35. 0035specialize power_divides_successor_of_cofactor e
  36. 0036specialize power_divides_successor_of_cofactor a
  37. 0037specialize power_divides_successor_of_cofactor x
  38. 0038specialize power_divides_successor_of_cofactor x1
  39. 0039apply power_divides_successor_of_cofactor
  40. 0040exact hcharacterization_left_witness_left
  41. 0041exact hcharacterization_left_witness_right_witness
  42. 0042exact hcofactor_prime