BT0083 · Bertrand theorem

pow_successor_decompose

Stable checked-use theorem · independently kernel verified

A successor relational power is its predecessor power times the base.

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

∀ a. ∀ e. ∀ se. ∀ n. se = S e → Pow(a,se,n) → ∃ x. Pow(a,e,x) ∧ n = x · a

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

PD0020 Pow

2 occurrences

In local proof propositions

PD0013 BetaAt PD0014 Product

2 occurrences

Exact expanded native-PA statement
forall a e se n. se = S e -> (exists ff_b_s ff_c_s. ((forall ff_i_s_repeat. (exists ff_lt_s_repeat_bound. ff_lt_s_repeat_bound + S ff_i_s_repeat = se) -> (((exists ff_h_s_repeat_decoded. ff_h_s_repeat_decoded + S (a) = S ((S (ff_i_s_repeat)) * ff_c_s)) /\ exists ff_q_s_repeat_decoded. ff_b_s = ff_q_s_repeat_decoded * S ((S (ff_i_s_repeat)) * ff_c_s) + (a)))) /\ (exists ff_u_s_product ff_v_s_product. ((((exists ff_h_s_product_start. ff_h_s_product_start + S (1) = S ((S (0)) * ff_v_s_product)) /\ exists ff_q_s_product_start. ff_u_s_product = ff_q_s_product_start * S ((S (0)) * ff_v_s_product) + (1))) /\ ((((exists ff_h_s_product_terminal. ff_h_s_product_terminal + S (n) = S ((S (se)) * ff_v_s_product)) /\ exists ff_q_s_product_terminal. ff_u_s_product = ff_q_s_product_terminal * S ((S (se)) * ff_v_s_product) + (n))) /\ forall ff_i_s_product. (exists ff_lt_s_product_bound. ff_lt_s_product_bound + S ff_i_s_product = se) -> exists ff_p_s_product ff_r_s_product ff_s_s_product. ((((exists ff_h_s_product_factor. ff_h_s_product_factor + S (ff_p_s_product) = S ((S (ff_i_s_product)) * ff_c_s)) /\ exists ff_q_s_product_factor. ff_b_s = ff_q_s_product_factor * S ((S (ff_i_s_product)) * ff_c_s) + (ff_p_s_product))) /\ ((((exists ff_h_s_product_partial. ff_h_s_product_partial + S (ff_r_s_product) = S ((S (ff_i_s_product)) * ff_v_s_product)) /\ exists ff_q_s_product_partial. ff_u_s_product = ff_q_s_product_partial * S ((S (ff_i_s_product)) * ff_v_s_product) + (ff_r_s_product))) /\ ((((exists ff_h_s_product_successor. ff_h_s_product_successor + S (ff_s_s_product) = S ((S (S ff_i_s_product)) * ff_v_s_product)) /\ exists ff_q_s_product_successor. ff_u_s_product = ff_q_s_product_successor * S ((S (S ff_i_s_product)) * ff_v_s_product) + (ff_s_s_product))) /\ ff_s_s_product = ff_r_s_product * ff_p_s_product)))))))) -> exists r. (exists ff_b_p ff_c_p. ((forall ff_i_p_repeat. (exists ff_lt_p_repeat_bound. ff_lt_p_repeat_bound + S ff_i_p_repeat = e) -> (((exists ff_h_p_repeat_decoded. ff_h_p_repeat_decoded + S (a) = S ((S (ff_i_p_repeat)) * ff_c_p)) /\ exists ff_q_p_repeat_decoded. ff_b_p = ff_q_p_repeat_decoded * S ((S (ff_i_p_repeat)) * ff_c_p) + (a)))) /\ (exists ff_u_p_product ff_v_p_product. ((((exists ff_h_p_product_start. ff_h_p_product_start + S (1) = S ((S (0)) * ff_v_p_product)) /\ exists ff_q_p_product_start. ff_u_p_product = ff_q_p_product_start * S ((S (0)) * ff_v_p_product) + (1))) /\ ((((exists ff_h_p_product_terminal. ff_h_p_product_terminal + S (r) = S ((S (e)) * ff_v_p_product)) /\ exists ff_q_p_product_terminal. ff_u_p_product = ff_q_p_product_terminal * S ((S (e)) * ff_v_p_product) + (r))) /\ forall ff_i_p_product. (exists ff_lt_p_product_bound. ff_lt_p_product_bound + S ff_i_p_product = e) -> exists ff_p_p_product ff_r_p_product ff_s_p_product. ((((exists ff_h_p_product_factor. ff_h_p_product_factor + S (ff_p_p_product) = S ((S (ff_i_p_product)) * ff_c_p)) /\ exists ff_q_p_product_factor. ff_b_p = ff_q_p_product_factor * S ((S (ff_i_p_product)) * ff_c_p) + (ff_p_p_product))) /\ ((((exists ff_h_p_product_partial. ff_h_p_product_partial + S (ff_r_p_product) = S ((S (ff_i_p_product)) * ff_v_p_product)) /\ exists ff_q_p_product_partial. ff_u_p_product = ff_q_p_product_partial * S ((S (ff_i_p_product)) * ff_v_p_product) + (ff_r_p_product))) /\ ((((exists ff_h_p_product_successor. ff_h_p_product_successor + S (ff_s_p_product) = S ((S (S ff_i_p_product)) * ff_v_p_product)) /\ exists ff_q_p_product_successor. ff_u_p_product = ff_q_p_product_successor * S ((S (S ff_i_p_product)) * ff_v_p_product) + (ff_s_p_product))) /\ ff_s_p_product = ff_r_p_product * ff_p_p_product)))))))) /\ n = r * a

Proof neighborhood

Direct theorem prerequisites

BT005J beta_product_succ_decompose BT007X beta_repeat_entry_eq BT000E le_refl BT0018 le_succ

Direct theorem dependents

BT0093 pow_one_from_zero_successor BT0095 pow_successor_pair_mul BT009V pow_two_from_one_successor BT009X pow_add BT00PY pow_base_monotone BT00Q0 one_le_pow BT00QF prime_power_exponent_le BT00QV pow_mul_base BT00RL prime_power_valuation_one_zero BT00SM pow_mul_exp_from_total BT00U1 pow_four_four_exact BT00U4 four_pow_lt_mul_central_binom BT00VM central_binom_strong_upper_of_laws BT00YU coprime_power_right BT00YV coprime_powers

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

54 script commands · 16 reading checkpoints · 2 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)
beta product succ decomposebeta repeat entry eqle reflle succ
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro e
  3. L3
    intro se
  4. L4
    intro n
  5. L5
    intro hse
  6. L6
    intro hpow
02Calculate and transport equalitiesL7–10

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

  1. L7
    rewrite hse at hpow
  2. L8
    rewrite hse at hpow
  3. L9
    rewrite hse at hpow
  4. L10
    rewrite hse at hpow
03Separate the logical casesL11–13

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

  1. L11
    cases hpow
  2. L12
    cases hpow_witness
  3. L13
    cases hpow_witness_witness
04Establish hdecompL14–20

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

  1. L14
    have hdecomp : ∃ p. ∃ r. BetaAt(x,x1,e,p) ∧ (Product(x,x1,e,r) ∧ n = r · p)Definitions: BetaAt(x,x1,e,p)Product(x,x1,e,r)Original native command in the exact edition
  2. L15
    specialize beta_product_succ_decompose x
  3. L16
    specialize beta_product_succ_decompose x1
  4. L17
    specialize beta_product_succ_decompose e
  5. L18
    specialize beta_product_succ_decompose n
  6. L19
    apply beta_product_succ_decompose
  7. L20
    exact hpow_witness_witness_right
05Separate the logical casesL21–24

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

  1. L21
    cases hdecomp
  2. L22
    cases hdecomp_witness
  3. L23
    cases hdecomp_witness_witness
  4. L24
    cases hdecomp_witness_witness_right
06Establish hpaL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta repeat entry eq.

  1. L25
    have hpa : x2 = a
  2. L26
    specialize beta_repeat_entry_eq x
  3. L27
    specialize beta_repeat_entry_eq x1
  4. L28
    specialize beta_repeat_entry_eq a
  5. L29
    specialize beta_repeat_entry_eq (S e)
  6. L30
    specialize beta_repeat_entry_eq e
  7. L31
    specialize beta_repeat_entry_eq x2
  8. L32
    apply beta_repeat_entry_eq
  9. L33
    exact hpow_witness_witness_left
  10. L34
    specialize le_refl (S e)
07Use earlier factsL35–36

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

  1. L35
    exact le_refl
  2. L36
    exact hdecomp_witness_witness_left
08Construct an explicit witnessL37–37

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

  1. L37
    exists x3
09Separate the logical casesL38–38

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

  1. L38
    split
10Construct an explicit witnessL39–40

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

  1. L39
    exists x
  2. L40
    exists x1
11Separate the logical casesL41–41

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

  1. L41
    split
12Fix variables and assumptionsL42–43

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

  1. L42
    intro i
  2. L43
    intro hi
13Use earlier factsL44–50

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

  1. L44
    specialize hpow_witness_witness_left i
  2. L45
    apply hpow_witness_witness_left
  3. L46
    specialize le_succ (S i)
  4. L47
    specialize le_succ e
  5. L48
    apply le_succ
  6. L49
    exact hi
  7. L50
    exact hdecomp_witness_witness_right_left
14Calculate and transport equalitiesL51–51

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

  1. L51
    trans x3 * x2
15Use earlier factsL52–52

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

  1. L52
    exact hdecomp_witness_witness_right_right
16Calculate and transport equalitiesL53–54

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

  1. L53
    rewrite hpa
  2. L54
    refl

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003intro se
  4. 0004intro n
  5. 0005intro hse
  6. 0006intro hpow
  7. 0007rewrite hse at hpow
  8. 0008rewrite hse at hpow
  9. 0009rewrite hse at hpow
  10. 0010rewrite hse at hpow
  11. 0011cases hpow
  12. 0012cases hpow_witness
  13. 0013cases hpow_witness_witness
  14. 0014have hdecomp : ∃ p. ∃ r. BetaAt(x,x1,e,p) ∧ (Product(x,x1,e,r) ∧ n = r · p)
    Exact native replay linehave hdecomp : exists p r. (((exists ff_h_pow_succ_factor. ff_h_pow_succ_factor + S (p) = S ((S (e)) * x1)) /\ exists ff_q_pow_succ_factor. x = ff_q_pow_succ_factor * S ((S (e)) * x1) + (p))) /\ ((exists ff_u_pow_succ_prefix ff_v_pow_succ_prefix. ((((exists ff_h_pow_succ_prefix_start. ff_h_pow_succ_prefix_start + S (1) = S ((S (0)) * ff_v_pow_succ_prefix)) /\ exists ff_q_pow_succ_prefix_start. ff_u_pow_succ_prefix = ff_q_pow_succ_prefix_start * S ((S (0)) * ff_v_pow_succ_prefix) + (1))) /\ ((((exists ff_h_pow_succ_prefix_terminal. ff_h_pow_succ_prefix_terminal + S (r) = S ((S (e)) * ff_v_pow_succ_prefix)) /\ exists ff_q_pow_succ_prefix_terminal. ff_u_pow_succ_prefix = ff_q_pow_succ_prefix_terminal * S ((S (e)) * ff_v_pow_succ_prefix) + (r))) /\ forall ff_i_pow_succ_prefix. (exists ff_lt_pow_succ_prefix_bound. ff_lt_pow_succ_prefix_bound + S ff_i_pow_succ_prefix = e) -> exists ff_p_pow_succ_prefix ff_r_pow_succ_prefix ff_s_pow_succ_prefix. ((((exists ff_h_pow_succ_prefix_factor. ff_h_pow_succ_prefix_factor + S (ff_p_pow_succ_prefix) = S ((S (ff_i_pow_succ_prefix)) * x1)) /\ exists ff_q_pow_succ_prefix_factor. x = ff_q_pow_succ_prefix_factor * S ((S (ff_i_pow_succ_prefix)) * x1) + (ff_p_pow_succ_prefix))) /\ ((((exists ff_h_pow_succ_prefix_partial. ff_h_pow_succ_prefix_partial + S (ff_r_pow_succ_prefix) = S ((S (ff_i_pow_succ_prefix)) * ff_v_pow_succ_prefix)) /\ exists ff_q_pow_succ_prefix_partial. ff_u_pow_succ_prefix = ff_q_pow_succ_prefix_partial * S ((S (ff_i_pow_succ_prefix)) * ff_v_pow_succ_prefix) + (ff_r_pow_succ_prefix))) /\ ((((exists ff_h_pow_succ_prefix_successor. ff_h_pow_succ_prefix_successor + S (ff_s_pow_succ_prefix) = S ((S (S ff_i_pow_succ_prefix)) * ff_v_pow_succ_prefix)) /\ exists ff_q_pow_succ_prefix_successor. ff_u_pow_succ_prefix = ff_q_pow_succ_prefix_successor * S ((S (S ff_i_pow_succ_prefix)) * ff_v_pow_succ_prefix) + (ff_s_pow_succ_prefix))) /\ ff_s_pow_succ_prefix = ff_r_pow_succ_prefix * ff_p_pow_succ_prefix)))))) /\ n = r * p)
  15. 0015specialize beta_product_succ_decompose x
  16. 0016specialize beta_product_succ_decompose x1
  17. 0017specialize beta_product_succ_decompose e
  18. 0018specialize beta_product_succ_decompose n
  19. 0019apply beta_product_succ_decompose
  20. 0020exact hpow_witness_witness_right
  21. 0021cases hdecomp
  22. 0022cases hdecomp_witness
  23. 0023cases hdecomp_witness_witness
  24. 0024cases hdecomp_witness_witness_right
  25. 0025have hpa : x2 = a
  26. 0026specialize beta_repeat_entry_eq x
  27. 0027specialize beta_repeat_entry_eq x1
  28. 0028specialize beta_repeat_entry_eq a
  29. 0029specialize beta_repeat_entry_eq (S e)
  30. 0030specialize beta_repeat_entry_eq e
  31. 0031specialize beta_repeat_entry_eq x2
  32. 0032apply beta_repeat_entry_eq
  33. 0033exact hpow_witness_witness_left
  34. 0034specialize le_refl (S e)
  35. 0035exact le_refl
  36. 0036exact hdecomp_witness_witness_left
  37. 0037exists x3
  38. 0038split
  39. 0039exists x
  40. 0040exists x1
  41. 0041split
  42. 0042intro i
  43. 0043intro hi
  44. 0044specialize hpow_witness_witness_left i
  45. 0045apply hpow_witness_witness_left
  46. 0046specialize le_succ (S i)
  47. 0047specialize le_succ e
  48. 0048apply le_succ
  49. 0049exact hi
  50. 0050exact hdecomp_witness_witness_right_left
  51. 0051trans x3 * x2
  52. 0052exact hdecomp_witness_witness_right_right
  53. 0053rewrite hpa
  54. 0054refl