BT00YV

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.

Exact expanded 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)

Structural proof guide

Powers of coprime bases are coprime.

Direct prerequisites: pow_zero, pow_successor_decompose, coprime_one_left, coprime_mul_left, coprime_power_right. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (4), equality transport (2).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0083 pow_successor_decompose BT002Y coprime_one_left BT004R coprime_mul_left BT00YU coprime_power_right

Direct dependents

BT00YW prime_contribution_prefix_pairwise_coprime

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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.

Named ingredients (5)
pow zeropow successor decomposecoprime one leftcoprime mul leftcoprime power right

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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 : forall d. (exists u. x = d * u) -> (exists v. z = d * v) -> d = 1
  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 : forall d. (exists u. p = d * u) -> (exists v. z = d * v) -> d = 1
  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 exact 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 : 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 : 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 : 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