BT0082 · Bertrand theorem

pow_functional

Stable checked-use theorem · independently kernel verified

Relational powers have a unique natural value.

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. ∀ n. ∀ m. Pow(a,e,n) → Pow(a,e,m) → n = m

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

PD0002 Lt PD0013 BetaAt PD0014 Product

4 occurrences

Exact expanded native-PA statement
forall a e n m. (exists ff_b_l ff_c_l. ((forall ff_i_l_repeat. (exists ff_lt_l_repeat_bound. ff_lt_l_repeat_bound + S ff_i_l_repeat = e) -> (((exists ff_h_l_repeat_decoded. ff_h_l_repeat_decoded + S (a) = S ((S (ff_i_l_repeat)) * ff_c_l)) /\ exists ff_q_l_repeat_decoded. ff_b_l = ff_q_l_repeat_decoded * S ((S (ff_i_l_repeat)) * ff_c_l) + (a)))) /\ (exists ff_u_l_product ff_v_l_product. ((((exists ff_h_l_product_start. ff_h_l_product_start + S (1) = S ((S (0)) * ff_v_l_product)) /\ exists ff_q_l_product_start. ff_u_l_product = ff_q_l_product_start * S ((S (0)) * ff_v_l_product) + (1))) /\ ((((exists ff_h_l_product_terminal. ff_h_l_product_terminal + S (n) = S ((S (e)) * ff_v_l_product)) /\ exists ff_q_l_product_terminal. ff_u_l_product = ff_q_l_product_terminal * S ((S (e)) * ff_v_l_product) + (n))) /\ forall ff_i_l_product. (exists ff_lt_l_product_bound. ff_lt_l_product_bound + S ff_i_l_product = e) -> exists ff_p_l_product ff_r_l_product ff_s_l_product. ((((exists ff_h_l_product_factor. ff_h_l_product_factor + S (ff_p_l_product) = S ((S (ff_i_l_product)) * ff_c_l)) /\ exists ff_q_l_product_factor. ff_b_l = ff_q_l_product_factor * S ((S (ff_i_l_product)) * ff_c_l) + (ff_p_l_product))) /\ ((((exists ff_h_l_product_partial. ff_h_l_product_partial + S (ff_r_l_product) = S ((S (ff_i_l_product)) * ff_v_l_product)) /\ exists ff_q_l_product_partial. ff_u_l_product = ff_q_l_product_partial * S ((S (ff_i_l_product)) * ff_v_l_product) + (ff_r_l_product))) /\ ((((exists ff_h_l_product_successor. ff_h_l_product_successor + S (ff_s_l_product) = S ((S (S ff_i_l_product)) * ff_v_l_product)) /\ exists ff_q_l_product_successor. ff_u_l_product = ff_q_l_product_successor * S ((S (S ff_i_l_product)) * ff_v_l_product) + (ff_s_l_product))) /\ ff_s_l_product = ff_r_l_product * ff_p_l_product)))))))) -> (exists ff_b_r ff_c_r. ((forall ff_i_r_repeat. (exists ff_lt_r_repeat_bound. ff_lt_r_repeat_bound + S ff_i_r_repeat = e) -> (((exists ff_h_r_repeat_decoded. ff_h_r_repeat_decoded + S (a) = S ((S (ff_i_r_repeat)) * ff_c_r)) /\ exists ff_q_r_repeat_decoded. ff_b_r = ff_q_r_repeat_decoded * S ((S (ff_i_r_repeat)) * ff_c_r) + (a)))) /\ (exists ff_u_r_product ff_v_r_product. ((((exists ff_h_r_product_start. ff_h_r_product_start + S (1) = S ((S (0)) * ff_v_r_product)) /\ exists ff_q_r_product_start. ff_u_r_product = ff_q_r_product_start * S ((S (0)) * ff_v_r_product) + (1))) /\ ((((exists ff_h_r_product_terminal. ff_h_r_product_terminal + S (m) = S ((S (e)) * ff_v_r_product)) /\ exists ff_q_r_product_terminal. ff_u_r_product = ff_q_r_product_terminal * S ((S (e)) * ff_v_r_product) + (m))) /\ forall ff_i_r_product. (exists ff_lt_r_product_bound. ff_lt_r_product_bound + S ff_i_r_product = e) -> exists ff_p_r_product ff_r_r_product ff_s_r_product. ((((exists ff_h_r_product_factor. ff_h_r_product_factor + S (ff_p_r_product) = S ((S (ff_i_r_product)) * ff_c_r)) /\ exists ff_q_r_product_factor. ff_b_r = ff_q_r_product_factor * S ((S (ff_i_r_product)) * ff_c_r) + (ff_p_r_product))) /\ ((((exists ff_h_r_product_partial. ff_h_r_product_partial + S (ff_r_r_product) = S ((S (ff_i_r_product)) * ff_v_r_product)) /\ exists ff_q_r_product_partial. ff_u_r_product = ff_q_r_product_partial * S ((S (ff_i_r_product)) * ff_v_r_product) + (ff_r_r_product))) /\ ((((exists ff_h_r_product_successor. ff_h_r_product_successor + S (ff_s_r_product) = S ((S (S ff_i_r_product)) * ff_v_r_product)) /\ exists ff_q_r_product_successor. ff_u_r_product = ff_q_r_product_successor * S ((S (S ff_i_r_product)) * ff_v_r_product) + (ff_s_r_product))) /\ ff_s_r_product = ff_r_r_product * ff_p_r_product)))))))) -> n = m

Proof neighborhood

Direct theorem prerequisites

BT007Y beta_repeat_transport_entry BT005L beta_product_transport_prefix BT005G beta_product_functional

Direct theorem dependents

BT0095 pow_successor_pair_mul BT009X pow_add BT00Q3 power_divides_decidable BT00S1 power_quotient_prefix_transport BT00SK power_quotient_successor_pointwise_add BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00XV double_quotient_carry_choice BT00YO prime_contribution_choice_functional BT00YX prime_contribution_factor_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

56 script commands · 9 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 (3)
beta repeat transport entrybeta product transport prefixbeta product functional
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 n
  4. L4
    intro m
  5. L5
    intro hn
  6. L6
    intro hm
02Separate the logical casesL7–12

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

  1. L7
    cases hn
  2. L8
    cases hn_witness
  3. L9
    cases hn_witness_witness
  4. L10
    cases hm
  5. L11
    cases hm_witness
  6. L12
    cases hm_witness_witness
03Establish htransportL13–22

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

  1. L13
    have htransport : Product(x2,x3,e,n)Definitions: Product(x2,x3,e,n)Original native command in the exact edition
  2. L14
    specialize beta_product_transport_prefix x
  3. L15
    specialize beta_product_transport_prefix x1
  4. L16
    specialize beta_product_transport_prefix x2
  5. L17
    specialize beta_product_transport_prefix x3
  6. L18
    specialize beta_product_transport_prefix e
  7. L19
    specialize beta_product_transport_prefix n
  8. L20
    apply beta_product_transport_prefix
  9. L21
    exact hn_witness_witness_right
  10. L22
    intro i
04Fix variables and assumptionsL23–25

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

  1. L23
    intro p
  2. L24
    intro hi
  3. L25
    intro hp
05Use earlier factsL26–31

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

  1. L26
    specialize beta_repeat_transport_entry x
  2. L27
    specialize beta_repeat_transport_entry x1
  3. L28
    specialize beta_repeat_transport_entry x2
  4. L29
    specialize beta_repeat_transport_entry x3
  5. L30
    specialize beta_repeat_transport_entry a
  6. L31
    specialize beta_repeat_transport_entry e
06Establish hentriesL32–40

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

  1. L32
    have hentries : ∀ i. ∀ p. Lt(i,e) → BetaAt(x,x1,i,p) → BetaAt(x2,x3,i,p)Definitions: Lt(i,e)BetaAt(x,x1,i,p)BetaAt(x2,x3,i,p)Original native command in the exact edition
  2. L33
    apply beta_repeat_transport_entry
  3. L34
    exact hn_witness_witness_left
  4. L35
    exact hm_witness_witness_left
  5. L36
    specialize hentries i
  6. L37
    specialize hentries p
  7. L38
    apply hentries
  8. L39
    exact hi
  9. L40
    exact hp
07Separate the logical casesL41–44

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

  1. L41
    cases htransport
  2. L42
    cases htransport_witness
  3. L43
    cases hm_witness_witness_right
  4. L44
    cases hm_witness_witness_right_witness
08Use earlier factsL45–54

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

  1. L45
    specialize beta_product_functional x2
  2. L46
    specialize beta_product_functional x3
  3. L47
    specialize beta_product_functional e
  4. L48
    specialize beta_product_functional n
  5. L49
    specialize beta_product_functional x4
  6. L50
    specialize beta_product_functional x5
  7. L51
    specialize beta_product_functional m
  8. L52
    specialize beta_product_functional x6
  9. L53
    specialize beta_product_functional x7
  10. L54
    apply beta_product_functional
09Use earlier factsL55–56

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

  1. L55
    exact htransport_witness_witness
  2. L56
    exact hm_witness_witness_right_witness_witness

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003intro n
  4. 0004intro m
  5. 0005intro hn
  6. 0006intro hm
  7. 0007cases hn
  8. 0008cases hn_witness
  9. 0009cases hn_witness_witness
  10. 0010cases hm
  11. 0011cases hm_witness
  12. 0012cases hm_witness_witness
  13. 0013have htransport : Product(x2,x3,e,n)
    Exact native replay linehave htransport : exists ff_u_transport ff_v_transport. ((((exists ff_h_transport_start. ff_h_transport_start + S (1) = S ((S (0)) * ff_v_transport)) /\ exists ff_q_transport_start. ff_u_transport = ff_q_transport_start * S ((S (0)) * ff_v_transport) + (1))) /\ ((((exists ff_h_transport_terminal. ff_h_transport_terminal + S (n) = S ((S (e)) * ff_v_transport)) /\ exists ff_q_transport_terminal. ff_u_transport = ff_q_transport_terminal * S ((S (e)) * ff_v_transport) + (n))) /\ forall ff_i_transport. (exists ff_lt_transport_bound. ff_lt_transport_bound + S ff_i_transport = e) -> exists ff_p_transport ff_r_transport ff_s_transport. ((((exists ff_h_transport_factor. ff_h_transport_factor + S (ff_p_transport) = S ((S (ff_i_transport)) * x3)) /\ exists ff_q_transport_factor. x2 = ff_q_transport_factor * S ((S (ff_i_transport)) * x3) + (ff_p_transport))) /\ ((((exists ff_h_transport_partial. ff_h_transport_partial + S (ff_r_transport) = S ((S (ff_i_transport)) * ff_v_transport)) /\ exists ff_q_transport_partial. ff_u_transport = ff_q_transport_partial * S ((S (ff_i_transport)) * ff_v_transport) + (ff_r_transport))) /\ ((((exists ff_h_transport_successor. ff_h_transport_successor + S (ff_s_transport) = S ((S (S ff_i_transport)) * ff_v_transport)) /\ exists ff_q_transport_successor. ff_u_transport = ff_q_transport_successor * S ((S (S ff_i_transport)) * ff_v_transport) + (ff_s_transport))) /\ ff_s_transport = ff_r_transport * ff_p_transport)))))
  14. 0014specialize beta_product_transport_prefix x
  15. 0015specialize beta_product_transport_prefix x1
  16. 0016specialize beta_product_transport_prefix x2
  17. 0017specialize beta_product_transport_prefix x3
  18. 0018specialize beta_product_transport_prefix e
  19. 0019specialize beta_product_transport_prefix n
  20. 0020apply beta_product_transport_prefix
  21. 0021exact hn_witness_witness_right
  22. 0022intro i
  23. 0023intro p
  24. 0024intro hi
  25. 0025intro hp
  26. 0026specialize beta_repeat_transport_entry x
  27. 0027specialize beta_repeat_transport_entry x1
  28. 0028specialize beta_repeat_transport_entry x2
  29. 0029specialize beta_repeat_transport_entry x3
  30. 0030specialize beta_repeat_transport_entry a
  31. 0031specialize beta_repeat_transport_entry e
  32. 0032have hentries : ∀ i. ∀ p. Lt(i,e) → BetaAt(x,x1,i,p) → BetaAt(x2,x3,i,p)
    Exact native replay linehave hentries : forall i p. (exists h. h + S i = e) -> (((exists ff_h_pow_transport_l. ff_h_pow_transport_l + S (p) = S ((S (i)) * x1)) /\ exists ff_q_pow_transport_l. x = ff_q_pow_transport_l * S ((S (i)) * x1) + (p))) -> (((exists ff_h_pow_transport_r. ff_h_pow_transport_r + S (p) = S ((S (i)) * x3)) /\ exists ff_q_pow_transport_r. x2 = ff_q_pow_transport_r * S ((S (i)) * x3) + (p)))
  33. 0033apply beta_repeat_transport_entry
  34. 0034exact hn_witness_witness_left
  35. 0035exact hm_witness_witness_left
  36. 0036specialize hentries i
  37. 0037specialize hentries p
  38. 0038apply hentries
  39. 0039exact hi
  40. 0040exact hp
  41. 0041cases htransport
  42. 0042cases htransport_witness
  43. 0043cases hm_witness_witness_right
  44. 0044cases hm_witness_witness_right_witness
  45. 0045specialize beta_product_functional x2
  46. 0046specialize beta_product_functional x3
  47. 0047specialize beta_product_functional e
  48. 0048specialize beta_product_functional n
  49. 0049specialize beta_product_functional x4
  50. 0050specialize beta_product_functional x5
  51. 0051specialize beta_product_functional m
  52. 0052specialize beta_product_functional x6
  53. 0053specialize beta_product_functional x7
  54. 0054apply beta_product_functional
  55. 0055exact htransport_witness_witness
  56. 0056exact hm_witness_witness_right_witness_witness