BT00YV · Bertrand theorem

coprime_powers

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

Powers of coprime bases are coprime.

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. ∀ q. ∀ e. ∀ f. ∀ a. ∀ z. Coprime(p,q) → Pow(p,e,a) → Pow(q,f,z) → Coprime(a,z)

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

PD0005 Coprime PD0020 Pow

4 occurrences

In local proof propositions

PD0005 Coprime PD0020 Pow

3 occurrences

Exact expanded native-PA statement
forall p q e f a z. (forall bpr_coprime_divisor_bcpowers_source. (exists bpr_coprime_left_bcpowers_source. p = bpr_coprime_divisor_bcpowers_source * bpr_coprime_left_bcpowers_source) -> (exists bpr_coprime_right_bcpowers_source. q = bpr_coprime_divisor_bcpowers_source * bpr_coprime_right_bcpowers_source) -> bpr_coprime_divisor_bcpowers_source = 1) -> (exists bpr_power_code_bcpowers_left bpr_power_scale_bcpowers_left. ((forall bpr_power_index_bcpowers_left. (exists bpr_gap_bcpowers_left_repeat_bound. bpr_gap_bcpowers_left_repeat_bound + S (bpr_power_index_bcpowers_left) = e) -> (((exists bpr_height_bcpowers_left_repeat_entry. bpr_height_bcpowers_left_repeat_entry + S (p) = S ((S (bpr_power_index_bcpowers_left)) * bpr_power_scale_bcpowers_left)) /\ exists bpr_quotient_bcpowers_left_repeat_entry. bpr_power_code_bcpowers_left = bpr_quotient_bcpowers_left_repeat_entry * S ((S (bpr_power_index_bcpowers_left)) * bpr_power_scale_bcpowers_left) + (p)))) /\ (exists ff_u_bcpowers_left_product ff_v_bcpowers_left_product. ((((exists ff_h_bcpowers_left_product_start. ff_h_bcpowers_left_product_start + S (1) = S ((S (0)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_start. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_start * S ((S (0)) * ff_v_bcpowers_left_product) + (1))) /\ ((((exists ff_h_bcpowers_left_product_terminal. ff_h_bcpowers_left_product_terminal + S (a) = S ((S (e)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_terminal. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_terminal * S ((S (e)) * ff_v_bcpowers_left_product) + (a))) /\ forall ff_i_bcpowers_left_product. (exists ff_lt_bcpowers_left_product_bound. ff_lt_bcpowers_left_product_bound + S ff_i_bcpowers_left_product = e) -> exists ff_p_bcpowers_left_product ff_r_bcpowers_left_product ff_s_bcpowers_left_product. ((((exists ff_h_bcpowers_left_product_factor. ff_h_bcpowers_left_product_factor + S (ff_p_bcpowers_left_product) = S ((S (ff_i_bcpowers_left_product)) * bpr_power_scale_bcpowers_left)) /\ exists ff_q_bcpowers_left_product_factor. bpr_power_code_bcpowers_left = ff_q_bcpowers_left_product_factor * S ((S (ff_i_bcpowers_left_product)) * bpr_power_scale_bcpowers_left) + (ff_p_bcpowers_left_product))) /\ ((((exists ff_h_bcpowers_left_product_partial. ff_h_bcpowers_left_product_partial + S (ff_r_bcpowers_left_product) = S ((S (ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_partial. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_partial * S ((S (ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product) + (ff_r_bcpowers_left_product))) /\ ((((exists ff_h_bcpowers_left_product_successor. ff_h_bcpowers_left_product_successor + S (ff_s_bcpowers_left_product) = S ((S (S ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product)) /\ exists ff_q_bcpowers_left_product_successor. ff_u_bcpowers_left_product = ff_q_bcpowers_left_product_successor * S ((S (S ff_i_bcpowers_left_product)) * ff_v_bcpowers_left_product) + (ff_s_bcpowers_left_product))) /\ ff_s_bcpowers_left_product = ff_r_bcpowers_left_product * ff_p_bcpowers_left_product)))))))) -> (exists bpr_power_code_bcpowers_right bpr_power_scale_bcpowers_right. ((forall bpr_power_index_bcpowers_right. (exists bpr_gap_bcpowers_right_repeat_bound. bpr_gap_bcpowers_right_repeat_bound + S (bpr_power_index_bcpowers_right) = f) -> (((exists bpr_height_bcpowers_right_repeat_entry. bpr_height_bcpowers_right_repeat_entry + S (q) = S ((S (bpr_power_index_bcpowers_right)) * bpr_power_scale_bcpowers_right)) /\ exists bpr_quotient_bcpowers_right_repeat_entry. bpr_power_code_bcpowers_right = bpr_quotient_bcpowers_right_repeat_entry * S ((S (bpr_power_index_bcpowers_right)) * bpr_power_scale_bcpowers_right) + (q)))) /\ (exists ff_u_bcpowers_right_product ff_v_bcpowers_right_product. ((((exists ff_h_bcpowers_right_product_start. ff_h_bcpowers_right_product_start + S (1) = S ((S (0)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_start. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_start * S ((S (0)) * ff_v_bcpowers_right_product) + (1))) /\ ((((exists ff_h_bcpowers_right_product_terminal. ff_h_bcpowers_right_product_terminal + S (z) = S ((S (f)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_terminal. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_terminal * S ((S (f)) * ff_v_bcpowers_right_product) + (z))) /\ forall ff_i_bcpowers_right_product. (exists ff_lt_bcpowers_right_product_bound. ff_lt_bcpowers_right_product_bound + S ff_i_bcpowers_right_product = f) -> exists ff_p_bcpowers_right_product ff_r_bcpowers_right_product ff_s_bcpowers_right_product. ((((exists ff_h_bcpowers_right_product_factor. ff_h_bcpowers_right_product_factor + S (ff_p_bcpowers_right_product) = S ((S (ff_i_bcpowers_right_product)) * bpr_power_scale_bcpowers_right)) /\ exists ff_q_bcpowers_right_product_factor. bpr_power_code_bcpowers_right = ff_q_bcpowers_right_product_factor * S ((S (ff_i_bcpowers_right_product)) * bpr_power_scale_bcpowers_right) + (ff_p_bcpowers_right_product))) /\ ((((exists ff_h_bcpowers_right_product_partial. ff_h_bcpowers_right_product_partial + S (ff_r_bcpowers_right_product) = S ((S (ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_partial. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_partial * S ((S (ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product) + (ff_r_bcpowers_right_product))) /\ ((((exists ff_h_bcpowers_right_product_successor. ff_h_bcpowers_right_product_successor + S (ff_s_bcpowers_right_product) = S ((S (S ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product)) /\ exists ff_q_bcpowers_right_product_successor. ff_u_bcpowers_right_product = ff_q_bcpowers_right_product_successor * S ((S (S ff_i_bcpowers_right_product)) * ff_v_bcpowers_right_product) + (ff_s_bcpowers_right_product))) /\ ff_s_bcpowers_right_product = ff_r_bcpowers_right_product * ff_p_bcpowers_right_product)))))))) -> (forall bpr_coprime_divisor_bcpowers_result. (exists bpr_coprime_left_bcpowers_result. a = bpr_coprime_divisor_bcpowers_result * bpr_coprime_left_bcpowers_result) -> (exists bpr_coprime_right_bcpowers_result. z = bpr_coprime_divisor_bcpowers_result * bpr_coprime_right_bcpowers_result) -> bpr_coprime_divisor_bcpowers_result = 1)

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0083 pow_successor_decompose BT002Y coprime_one_left BT004R coprime_mul_left BT00YU coprime_power_right

Direct theorem dependents

BT00YW prime_contribution_prefix_pairwise_coprime

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

55 script commands · 9 reading checkpoints · 4 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 (5)
pow zeropow successor decomposecoprime one leftcoprime mul leftcoprime power right
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro q
02Induction on eL3–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction e
  2. L4
    intro f
  3. L5
    intro a
  4. L6
    intro z
  5. L7
    intro hcoprime
  6. L8
    intro hleft
  7. L9
    intro hright
03Establish hvalueL10–19

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

  1. L10
    have hvalue : a = 1
  2. L11
    specialize pow_zero p
  3. L12
    specialize pow_zero 0
  4. L13
    specialize pow_zero a
  5. L14
    apply pow_zero
  6. L15
    refl
  7. L16
    exact hleft
  8. L17
    rewrite hvalue
  9. L18
    specialize coprime_one_left z
  10. L19
    apply coprime_one_left
04Fix variables and assumptionsL20–25

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

  1. L20
    intro f
  2. L21
    intro a
  3. L22
    intro z
  4. L23
    intro hcoprime
  5. L24
    intro hleft
  6. L25
    intro hright
05Establish hdecompositionL26–33

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

  1. L26
    have hdecomposition : ∃ r. Pow(p,e,r) ∧ a = r · pDefinitions: Pow(p,e,r)Original native command in the exact edition
  2. L27
    specialize pow_successor_decompose p
  3. L28
    specialize pow_successor_decompose e
  4. L29
    specialize pow_successor_decompose (S e)
  5. L30
    specialize pow_successor_decompose a
  6. L31
    apply pow_successor_decompose
  7. L32
    refl
  8. L33
    exact hleft
06Separate the logical casesL34–35

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

  1. L34
    cases hdecomposition
  2. L35
    cases hdecomposition_witness
07Establish hprefixL36–43

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

  1. L36
    have hprefix : Coprime(x,z)Definitions: Coprime(x,z)Original native command in the exact edition
  2. L37
    specialize IH f
  3. L38
    specialize IH x
  4. L39
    specialize IH z
  5. L40
    apply IH
  6. L41
    exact hcoprime
  7. L42
    exact hdecomposition_witness_left
  8. L43
    exact hright
08Establish hlastL44–53

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

  1. L44
    have hlast : Coprime(p,z)Definitions: Coprime(p,z)Original native command in the exact edition
  2. L45
    specialize coprime_power_right p
  3. L46
    specialize coprime_power_right q
  4. L47
    specialize coprime_power_right f
  5. L48
    specialize coprime_power_right z
  6. L49
    apply coprime_power_right
  7. L50
    exact hcoprime
  8. L51
    exact hright
  9. L52
    rewrite hdecomposition_witness_right
  10. L53
    apply coprime_mul_left
09Use earlier factsL54–55

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

  1. L54
    exact hprefix
  2. L55
    exact hlast

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003induction e
  4. 0004intro f
  5. 0005intro a
  6. 0006intro z
  7. 0007intro hcoprime
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010have hvalue : a = 1
  11. 0011specialize pow_zero p
  12. 0012specialize pow_zero 0
  13. 0013specialize pow_zero a
  14. 0014apply pow_zero
  15. 0015refl
  16. 0016exact hleft
  17. 0017rewrite hvalue
  18. 0018specialize coprime_one_left z
  19. 0019apply coprime_one_left
  20. 0020intro f
  21. 0021intro a
  22. 0022intro z
  23. 0023intro hcoprime
  24. 0024intro hleft
  25. 0025intro hright
  26. 0026have hdecomposition : ∃ r. Pow(p,e,r) ∧ a = r · p
    Exact native replay linehave hdecomposition : exists r. (exists bpr_power_code_bcpowers_previous bpr_power_scale_bcpowers_previous. ((forall bpr_power_index_bcpowers_previous. (exists bpr_gap_bcpowers_previous_repeat_bound. bpr_gap_bcpowers_previous_repeat_bound + S (bpr_power_index_bcpowers_previous) = e) -> (((exists bpr_height_bcpowers_previous_repeat_entry. bpr_height_bcpowers_previous_repeat_entry + S (p) = S ((S (bpr_power_index_bcpowers_previous)) * bpr_power_scale_bcpowers_previous)) /\ exists bpr_quotient_bcpowers_previous_repeat_entry. bpr_power_code_bcpowers_previous = bpr_quotient_bcpowers_previous_repeat_entry * S ((S (bpr_power_index_bcpowers_previous)) * bpr_power_scale_bcpowers_previous) + (p)))) /\ (exists ff_u_bcpowers_previous_product ff_v_bcpowers_previous_product. ((((exists ff_h_bcpowers_previous_product_start. ff_h_bcpowers_previous_product_start + S (1) = S ((S (0)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_start. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_start * S ((S (0)) * ff_v_bcpowers_previous_product) + (1))) /\ ((((exists ff_h_bcpowers_previous_product_terminal. ff_h_bcpowers_previous_product_terminal + S (r) = S ((S (e)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_terminal. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_terminal * S ((S (e)) * ff_v_bcpowers_previous_product) + (r))) /\ forall ff_i_bcpowers_previous_product. (exists ff_lt_bcpowers_previous_product_bound. ff_lt_bcpowers_previous_product_bound + S ff_i_bcpowers_previous_product = e) -> exists ff_p_bcpowers_previous_product ff_r_bcpowers_previous_product ff_s_bcpowers_previous_product. ((((exists ff_h_bcpowers_previous_product_factor. ff_h_bcpowers_previous_product_factor + S (ff_p_bcpowers_previous_product) = S ((S (ff_i_bcpowers_previous_product)) * bpr_power_scale_bcpowers_previous)) /\ exists ff_q_bcpowers_previous_product_factor. bpr_power_code_bcpowers_previous = ff_q_bcpowers_previous_product_factor * S ((S (ff_i_bcpowers_previous_product)) * bpr_power_scale_bcpowers_previous) + (ff_p_bcpowers_previous_product))) /\ ((((exists ff_h_bcpowers_previous_product_partial. ff_h_bcpowers_previous_product_partial + S (ff_r_bcpowers_previous_product) = S ((S (ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_partial. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_partial * S ((S (ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product) + (ff_r_bcpowers_previous_product))) /\ ((((exists ff_h_bcpowers_previous_product_successor. ff_h_bcpowers_previous_product_successor + S (ff_s_bcpowers_previous_product) = S ((S (S ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product)) /\ exists ff_q_bcpowers_previous_product_successor. ff_u_bcpowers_previous_product = ff_q_bcpowers_previous_product_successor * S ((S (S ff_i_bcpowers_previous_product)) * ff_v_bcpowers_previous_product) + (ff_s_bcpowers_previous_product))) /\ ff_s_bcpowers_previous_product = ff_r_bcpowers_previous_product * ff_p_bcpowers_previous_product)))))))) /\ a = r * p
  27. 0027specialize pow_successor_decompose p
  28. 0028specialize pow_successor_decompose e
  29. 0029specialize pow_successor_decompose (S e)
  30. 0030specialize pow_successor_decompose a
  31. 0031apply pow_successor_decompose
  32. 0032refl
  33. 0033exact hleft
  34. 0034cases hdecomposition
  35. 0035cases hdecomposition_witness
  36. 0036have hprefix : Coprime(x,z)
    Exact native replay linehave hprefix : forall d. (exists u. x = d * u) -> (exists v. z = d * v) -> d = 1
  37. 0037specialize IH f
  38. 0038specialize IH x
  39. 0039specialize IH z
  40. 0040apply IH
  41. 0041exact hcoprime
  42. 0042exact hdecomposition_witness_left
  43. 0043exact hright
  44. 0044have hlast : Coprime(p,z)
    Exact native replay linehave hlast : forall d. (exists u. p = d * u) -> (exists v. z = d * v) -> d = 1
  45. 0045specialize coprime_power_right p
  46. 0046specialize coprime_power_right q
  47. 0047specialize coprime_power_right f
  48. 0048specialize coprime_power_right z
  49. 0049apply coprime_power_right
  50. 0050exact hcoprime
  51. 0051exact hright
  52. 0052rewrite hdecomposition_witness_right
  53. 0053apply coprime_mul_left
  54. 0054exact hprefix
  55. 0055exact hlast