BT00YU · Bertrand theorem

coprime_power_right

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

A power preserves coprimality with a fixed left operand.

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

3 occurrences

In local proof propositions

PD0005 Coprime PD0020 Pow

2 occurrences

Exact expanded native-PA statement
forall p q e z. (forall bpr_coprime_divisor_bcpr_source. (exists bpr_coprime_left_bcpr_source. p = bpr_coprime_divisor_bcpr_source * bpr_coprime_left_bcpr_source) -> (exists bpr_coprime_right_bcpr_source. q = bpr_coprime_divisor_bcpr_source * bpr_coprime_right_bcpr_source) -> bpr_coprime_divisor_bcpr_source = 1) -> (exists bpr_power_code_bcpr_power bpr_power_scale_bcpr_power. ((forall bpr_power_index_bcpr_power. (exists bpr_gap_bcpr_power_repeat_bound. bpr_gap_bcpr_power_repeat_bound + S (bpr_power_index_bcpr_power) = e) -> (((exists bpr_height_bcpr_power_repeat_entry. bpr_height_bcpr_power_repeat_entry + S (q) = S ((S (bpr_power_index_bcpr_power)) * bpr_power_scale_bcpr_power)) /\ exists bpr_quotient_bcpr_power_repeat_entry. bpr_power_code_bcpr_power = bpr_quotient_bcpr_power_repeat_entry * S ((S (bpr_power_index_bcpr_power)) * bpr_power_scale_bcpr_power) + (q)))) /\ (exists ff_u_bcpr_power_product ff_v_bcpr_power_product. ((((exists ff_h_bcpr_power_product_start. ff_h_bcpr_power_product_start + S (1) = S ((S (0)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_start. ff_u_bcpr_power_product = ff_q_bcpr_power_product_start * S ((S (0)) * ff_v_bcpr_power_product) + (1))) /\ ((((exists ff_h_bcpr_power_product_terminal. ff_h_bcpr_power_product_terminal + S (z) = S ((S (e)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_terminal. ff_u_bcpr_power_product = ff_q_bcpr_power_product_terminal * S ((S (e)) * ff_v_bcpr_power_product) + (z))) /\ forall ff_i_bcpr_power_product. (exists ff_lt_bcpr_power_product_bound. ff_lt_bcpr_power_product_bound + S ff_i_bcpr_power_product = e) -> exists ff_p_bcpr_power_product ff_r_bcpr_power_product ff_s_bcpr_power_product. ((((exists ff_h_bcpr_power_product_factor. ff_h_bcpr_power_product_factor + S (ff_p_bcpr_power_product) = S ((S (ff_i_bcpr_power_product)) * bpr_power_scale_bcpr_power)) /\ exists ff_q_bcpr_power_product_factor. bpr_power_code_bcpr_power = ff_q_bcpr_power_product_factor * S ((S (ff_i_bcpr_power_product)) * bpr_power_scale_bcpr_power) + (ff_p_bcpr_power_product))) /\ ((((exists ff_h_bcpr_power_product_partial. ff_h_bcpr_power_product_partial + S (ff_r_bcpr_power_product) = S ((S (ff_i_bcpr_power_product)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_partial. ff_u_bcpr_power_product = ff_q_bcpr_power_product_partial * S ((S (ff_i_bcpr_power_product)) * ff_v_bcpr_power_product) + (ff_r_bcpr_power_product))) /\ ((((exists ff_h_bcpr_power_product_successor. ff_h_bcpr_power_product_successor + S (ff_s_bcpr_power_product) = S ((S (S ff_i_bcpr_power_product)) * ff_v_bcpr_power_product)) /\ exists ff_q_bcpr_power_product_successor. ff_u_bcpr_power_product = ff_q_bcpr_power_product_successor * S ((S (S ff_i_bcpr_power_product)) * ff_v_bcpr_power_product) + (ff_s_bcpr_power_product))) /\ ff_s_bcpr_power_product = ff_r_bcpr_power_product * ff_p_bcpr_power_product)))))))) -> (forall bpr_coprime_divisor_bcpr_result. (exists bpr_coprime_left_bcpr_result. p = bpr_coprime_divisor_bcpr_result * bpr_coprime_left_bcpr_result) -> (exists bpr_coprime_right_bcpr_result. z = bpr_coprime_divisor_bcpr_result * bpr_coprime_right_bcpr_result) -> bpr_coprime_divisor_bcpr_result = 1)

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0083 pow_successor_decompose BT002X coprime_one_right BT004S coprime_mul_right

Direct theorem dependents

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

38 script commands · 7 reading checkpoints · 3 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)
pow zeropow successor decomposecoprime one rightcoprime mul 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–6

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 z
  3. L5
    intro hcoprime
  4. L6
    intro hpower
03Establish hvalueL7–16

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

  1. L7
    have hvalue : z = 1
  2. L8
    specialize pow_zero q
  3. L9
    specialize pow_zero 0
  4. L10
    specialize pow_zero z
  5. L11
    apply pow_zero
  6. L12
    refl
  7. L13
    exact hpower
  8. L14
    rewrite hvalue
  9. L15
    specialize coprime_one_right p
  10. L16
    apply coprime_one_right
04Fix variables and assumptionsL17–19

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

  1. L17
    intro z
  2. L18
    intro hcoprime
  3. L19
    intro hpower
05Establish hdecompositionL20–27

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

  1. L20
    have hdecomposition : ∃ r. Pow(q,e,r) ∧ z = r · qDefinitions: Pow(q,e,r)Original native command in the exact edition
  2. L21
    specialize pow_successor_decompose q
  3. L22
    specialize pow_successor_decompose e
  4. L23
    specialize pow_successor_decompose (S e)
  5. L24
    specialize pow_successor_decompose z
  6. L25
    apply pow_successor_decompose
  7. L26
    refl
  8. L27
    exact hpower
06Separate the logical casesL28–29

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

  1. L28
    cases hdecomposition
  2. L29
    cases hdecomposition_witness
07Establish hprefixL30–38

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

  1. L30
    have hprefix : Coprime(p,x)Definitions: Coprime(p,x)Original native command in the exact edition
  2. L31
    specialize IH x
  3. L32
    apply IH
  4. L33
    exact hcoprime
  5. L34
    exact hdecomposition_witness_left
  6. L35
    rewrite hdecomposition_witness_right
  7. L36
    apply coprime_mul_right
  8. L37
    exact hprefix
  9. L38
    exact hcoprime

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003induction e
  4. 0004intro z
  5. 0005intro hcoprime
  6. 0006intro hpower
  7. 0007have hvalue : z = 1
  8. 0008specialize pow_zero q
  9. 0009specialize pow_zero 0
  10. 0010specialize pow_zero z
  11. 0011apply pow_zero
  12. 0012refl
  13. 0013exact hpower
  14. 0014rewrite hvalue
  15. 0015specialize coprime_one_right p
  16. 0016apply coprime_one_right
  17. 0017intro z
  18. 0018intro hcoprime
  19. 0019intro hpower
  20. 0020have hdecomposition : ∃ r. Pow(q,e,r) ∧ z = r · q
    Exact native replay linehave hdecomposition : exists r. (exists bpr_power_code_bcpr_previous bpr_power_scale_bcpr_previous. ((forall bpr_power_index_bcpr_previous. (exists bpr_gap_bcpr_previous_repeat_bound. bpr_gap_bcpr_previous_repeat_bound + S (bpr_power_index_bcpr_previous) = e) -> (((exists bpr_height_bcpr_previous_repeat_entry. bpr_height_bcpr_previous_repeat_entry + S (q) = S ((S (bpr_power_index_bcpr_previous)) * bpr_power_scale_bcpr_previous)) /\ exists bpr_quotient_bcpr_previous_repeat_entry. bpr_power_code_bcpr_previous = bpr_quotient_bcpr_previous_repeat_entry * S ((S (bpr_power_index_bcpr_previous)) * bpr_power_scale_bcpr_previous) + (q)))) /\ (exists ff_u_bcpr_previous_product ff_v_bcpr_previous_product. ((((exists ff_h_bcpr_previous_product_start. ff_h_bcpr_previous_product_start + S (1) = S ((S (0)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_start. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_start * S ((S (0)) * ff_v_bcpr_previous_product) + (1))) /\ ((((exists ff_h_bcpr_previous_product_terminal. ff_h_bcpr_previous_product_terminal + S (r) = S ((S (e)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_terminal. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_terminal * S ((S (e)) * ff_v_bcpr_previous_product) + (r))) /\ forall ff_i_bcpr_previous_product. (exists ff_lt_bcpr_previous_product_bound. ff_lt_bcpr_previous_product_bound + S ff_i_bcpr_previous_product = e) -> exists ff_p_bcpr_previous_product ff_r_bcpr_previous_product ff_s_bcpr_previous_product. ((((exists ff_h_bcpr_previous_product_factor. ff_h_bcpr_previous_product_factor + S (ff_p_bcpr_previous_product) = S ((S (ff_i_bcpr_previous_product)) * bpr_power_scale_bcpr_previous)) /\ exists ff_q_bcpr_previous_product_factor. bpr_power_code_bcpr_previous = ff_q_bcpr_previous_product_factor * S ((S (ff_i_bcpr_previous_product)) * bpr_power_scale_bcpr_previous) + (ff_p_bcpr_previous_product))) /\ ((((exists ff_h_bcpr_previous_product_partial. ff_h_bcpr_previous_product_partial + S (ff_r_bcpr_previous_product) = S ((S (ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_partial. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_partial * S ((S (ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product) + (ff_r_bcpr_previous_product))) /\ ((((exists ff_h_bcpr_previous_product_successor. ff_h_bcpr_previous_product_successor + S (ff_s_bcpr_previous_product) = S ((S (S ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product)) /\ exists ff_q_bcpr_previous_product_successor. ff_u_bcpr_previous_product = ff_q_bcpr_previous_product_successor * S ((S (S ff_i_bcpr_previous_product)) * ff_v_bcpr_previous_product) + (ff_s_bcpr_previous_product))) /\ ff_s_bcpr_previous_product = ff_r_bcpr_previous_product * ff_p_bcpr_previous_product)))))))) /\ z = r * q
  21. 0021specialize pow_successor_decompose q
  22. 0022specialize pow_successor_decompose e
  23. 0023specialize pow_successor_decompose (S e)
  24. 0024specialize pow_successor_decompose z
  25. 0025apply pow_successor_decompose
  26. 0026refl
  27. 0027exact hpower
  28. 0028cases hdecomposition
  29. 0029cases hdecomposition_witness
  30. 0030have hprefix : Coprime(p,x)
    Exact native replay linehave hprefix : forall d. (exists a. p = d * a) -> (exists b. x = d * b) -> d = 1
  31. 0031specialize IH x
  32. 0032apply IH
  33. 0033exact hcoprime
  34. 0034exact hdecomposition_witness_left
  35. 0035rewrite hdecomposition_witness_right
  36. 0036apply coprime_mul_right
  37. 0037exact hprefix
  38. 0038exact hcoprime