BT00DH · Bertrand theorem

beta_product_pointwise_coprime

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

A finite product of factors pointwise coprime to m is coprime to m.

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

∀ m. ∀ b. ∀ c. ∀ l. ∀ z. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → Coprime(y,m)) → Product(b,c,l,z) → Coprime(z,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

PD0002 Lt PD0005 Coprime PD0013 BetaAt PD0014 Product

5 occurrences

In local proof propositions

PD0002 Lt PD0005 Coprime PD0013 BetaAt PD0014 Product

7 occurrences

Exact expanded native-PA statement
forall m b c l z. (forall frp_index_pointwise frp_factor_pointwise. (exists frp_gap_pointwise_bound. frp_gap_pointwise_bound + S frp_index_pointwise = l) -> (((exists ff_h_frp_pointwise_decoded. ff_h_frp_pointwise_decoded + S (frp_factor_pointwise) = S ((S (frp_index_pointwise)) * c)) /\ exists ff_q_frp_pointwise_decoded. b = ff_q_frp_pointwise_decoded * S ((S (frp_index_pointwise)) * c) + (frp_factor_pointwise))) -> (forall frp_divisor_pointwise_coprime. (exists frp_left_factor_pointwise_coprime. frp_factor_pointwise = frp_divisor_pointwise_coprime * frp_left_factor_pointwise_coprime) -> (exists frp_right_factor_pointwise_coprime. m = frp_divisor_pointwise_coprime * frp_right_factor_pointwise_coprime) -> frp_divisor_pointwise_coprime = 1)) -> (exists ff_u_pointwise_product ff_v_pointwise_product. ((((exists ff_h_pointwise_product_start. ff_h_pointwise_product_start + S (1) = S ((S (0)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_start. ff_u_pointwise_product = ff_q_pointwise_product_start * S ((S (0)) * ff_v_pointwise_product) + (1))) /\ ((((exists ff_h_pointwise_product_terminal. ff_h_pointwise_product_terminal + S (z) = S ((S (l)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_terminal. ff_u_pointwise_product = ff_q_pointwise_product_terminal * S ((S (l)) * ff_v_pointwise_product) + (z))) /\ forall ff_i_pointwise_product. (exists ff_lt_pointwise_product_bound. ff_lt_pointwise_product_bound + S ff_i_pointwise_product = l) -> exists ff_p_pointwise_product ff_r_pointwise_product ff_s_pointwise_product. ((((exists ff_h_pointwise_product_factor. ff_h_pointwise_product_factor + S (ff_p_pointwise_product) = S ((S (ff_i_pointwise_product)) * c)) /\ exists ff_q_pointwise_product_factor. b = ff_q_pointwise_product_factor * S ((S (ff_i_pointwise_product)) * c) + (ff_p_pointwise_product))) /\ ((((exists ff_h_pointwise_product_partial. ff_h_pointwise_product_partial + S (ff_r_pointwise_product) = S ((S (ff_i_pointwise_product)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_partial. ff_u_pointwise_product = ff_q_pointwise_product_partial * S ((S (ff_i_pointwise_product)) * ff_v_pointwise_product) + (ff_r_pointwise_product))) /\ ((((exists ff_h_pointwise_product_successor. ff_h_pointwise_product_successor + S (ff_s_pointwise_product) = S ((S (S ff_i_pointwise_product)) * ff_v_pointwise_product)) /\ exists ff_q_pointwise_product_successor. ff_u_pointwise_product = ff_q_pointwise_product_successor * S ((S (S ff_i_pointwise_product)) * ff_v_pointwise_product) + (ff_s_pointwise_product))) /\ ff_s_pointwise_product = ff_r_pointwise_product * ff_p_pointwise_product)))))) -> (forall frp_divisor_pointwise_result. (exists frp_left_factor_pointwise_result. z = frp_divisor_pointwise_result * frp_left_factor_pointwise_result) -> (exists frp_right_factor_pointwise_result. m = frp_divisor_pointwise_result * frp_right_factor_pointwise_result) -> frp_divisor_pointwise_result = 1)

Proof neighborhood

Direct theorem prerequisites

BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT002Y coprime_one_left BT004R coprime_mul_left

Direct theorem dependents

BT00VD beta_pairwise_coprime_product_divides_common_multiple

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

62 script commands · 11 reading checkpoints · 5 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 (6)
beta product zerobeta product succ decomposele succle reflcoprime one leftcoprime mul left
01Fix variables and assumptionsL1–3

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

  1. L1
    intro m
  2. L2
    intro b
  3. L3
    intro c
02Induction on lL4–7

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

  1. L4
    induction l
  2. L5
    intro z
  3. L6
    intro hpw
  4. L7
    intro hproduct
03Establish hzL8–17

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

  1. L8
    have hz : z = 1
  2. L9
    specialize beta_product_zero b
  3. L10
    specialize beta_product_zero c
  4. L11
    specialize beta_product_zero z
  5. L12
    apply beta_product_zero
  6. L13
    exact hproduct
  7. L14
    rewrite hz
  8. L15
    specialize coprime_one_left m
  9. L16
    exact coprime_one_left
  10. L17
    intro z
04Fix variables and assumptionsL18–19

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

  1. L18
    intro hpw
  2. L19
    intro hproduct
05Establish hdecompL20–26

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

  1. L20
    have hdecomp : ∃ p. ∃ r. BetaAt(b,c,l,p) ∧ (Product(b,c,l,r) ∧ z = r · p)Definitions: BetaAt(b,c,l,p)Product(b,c,l,r)Original native command in the exact edition
  2. L21
    specialize beta_product_succ_decompose b
  3. L22
    specialize beta_product_succ_decompose c
  4. L23
    specialize beta_product_succ_decompose l
  5. L24
    specialize beta_product_succ_decompose z
  6. L25
    apply beta_product_succ_decompose
  7. L26
    exact hproduct
06Separate the logical casesL27–30

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

  1. L27
    cases hdecomp
  2. L28
    cases hdecomp_witness
  3. L29
    cases hdecomp_witness_witness
  4. L30
    cases hdecomp_witness_witness_right
07Establish hpw_prefixL31–40

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

  1. L31
    have hpw_prefix : ∀ frp_index_pointwise_prefix. ∀ frp_factor_pointwise_prefix. Lt(frp_index_pointwise_prefix,l) → BetaAt(b,c,frp_index_pointwise_prefix,frp_factor_pointwise_prefix) → Coprime(frp_factor_pointwise_prefix,m)Definitions: Lt(frp_index_pointwise_prefix,l)BetaAt(b,c,frp_index_pointwise_prefix,frp_factor_pointwise_prefix)Coprime(frp_factor_pointwise_prefix,m)Original native command in the exact edition
  2. L32
    intro i
  3. L33
    intro x2
  4. L34
    intro hi
  5. L35
    intro hx2
  6. L36
    specialize hpw i
  7. L37
    specialize hpw x2
  8. L38
    apply hpw
  9. L39
    specialize le_succ (S i)
  10. L40
    specialize le_succ l
08Use earlier factsL41–43

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

  1. L41
    apply le_succ
  2. L42
    exact hi
  3. L43
    exact hx2
09Establish hprefixL44–48

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

  1. L44
    have hprefix : Coprime(x1,m)Definitions: Coprime(x1,m)Original native command in the exact edition
  2. L45
    specialize IH x1
  3. L46
    apply IH
  4. L47
    exact hpw_prefix
  5. L48
    exact hdecomp_witness_witness_right_left
10Establish hfactorL49–58

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

  1. L49
    have hfactor : Coprime(x,m)Definitions: Coprime(x,m)Original native command in the exact edition
  2. L50
    specialize hpw l
  3. L51
    specialize hpw x
  4. L52
    apply hpw
  5. L53
    specialize le_refl (S l)
  6. L54
    exact le_refl
  7. L55
    exact hdecomp_witness_witness_left
  8. L56
    rewrite hdecomp_witness_witness_right_right
  9. L57
    specialize coprime_mul_left x1
  10. L58
    specialize coprime_mul_left x
11Use earlier factsL59–62

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

  1. L59
    specialize coprime_mul_left m
  2. L60
    apply coprime_mul_left
  3. L61
    exact hprefix
  4. L62
    exact hfactor

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro m
  2. 0002intro b
  3. 0003intro c
  4. 0004induction l
  5. 0005intro z
  6. 0006intro hpw
  7. 0007intro hproduct
  8. 0008have hz : z = 1
  9. 0009specialize beta_product_zero b
  10. 0010specialize beta_product_zero c
  11. 0011specialize beta_product_zero z
  12. 0012apply beta_product_zero
  13. 0013exact hproduct
  14. 0014rewrite hz
  15. 0015specialize coprime_one_left m
  16. 0016exact coprime_one_left
  17. 0017intro z
  18. 0018intro hpw
  19. 0019intro hproduct
  20. 0020have hdecomp : ∃ p. ∃ r. BetaAt(b,c,l,p) ∧ (Product(b,c,l,r) ∧ z = r · p)
    Exact native replay linehave hdecomp : exists p r. (((exists ff_h_frp_final_factor. ff_h_frp_final_factor + S (p) = S ((S (l)) * c)) /\ exists ff_q_frp_final_factor. b = ff_q_frp_final_factor * S ((S (l)) * c) + (p))) /\ ((exists ff_u_pointwise_prefix_product ff_v_pointwise_prefix_product. ((((exists ff_h_pointwise_prefix_product_start. ff_h_pointwise_prefix_product_start + S (1) = S ((S (0)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_start. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_start * S ((S (0)) * ff_v_pointwise_prefix_product) + (1))) /\ ((((exists ff_h_pointwise_prefix_product_terminal. ff_h_pointwise_prefix_product_terminal + S (r) = S ((S (l)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_terminal. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_terminal * S ((S (l)) * ff_v_pointwise_prefix_product) + (r))) /\ forall ff_i_pointwise_prefix_product. (exists ff_lt_pointwise_prefix_product_bound. ff_lt_pointwise_prefix_product_bound + S ff_i_pointwise_prefix_product = l) -> exists ff_p_pointwise_prefix_product ff_r_pointwise_prefix_product ff_s_pointwise_prefix_product. ((((exists ff_h_pointwise_prefix_product_factor. ff_h_pointwise_prefix_product_factor + S (ff_p_pointwise_prefix_product) = S ((S (ff_i_pointwise_prefix_product)) * c)) /\ exists ff_q_pointwise_prefix_product_factor. b = ff_q_pointwise_prefix_product_factor * S ((S (ff_i_pointwise_prefix_product)) * c) + (ff_p_pointwise_prefix_product))) /\ ((((exists ff_h_pointwise_prefix_product_partial. ff_h_pointwise_prefix_product_partial + S (ff_r_pointwise_prefix_product) = S ((S (ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_partial. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_partial * S ((S (ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product) + (ff_r_pointwise_prefix_product))) /\ ((((exists ff_h_pointwise_prefix_product_successor. ff_h_pointwise_prefix_product_successor + S (ff_s_pointwise_prefix_product) = S ((S (S ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product)) /\ exists ff_q_pointwise_prefix_product_successor. ff_u_pointwise_prefix_product = ff_q_pointwise_prefix_product_successor * S ((S (S ff_i_pointwise_prefix_product)) * ff_v_pointwise_prefix_product) + (ff_s_pointwise_prefix_product))) /\ ff_s_pointwise_prefix_product = ff_r_pointwise_prefix_product * ff_p_pointwise_prefix_product)))))) /\ z = r * p)
  21. 0021specialize beta_product_succ_decompose b
  22. 0022specialize beta_product_succ_decompose c
  23. 0023specialize beta_product_succ_decompose l
  24. 0024specialize beta_product_succ_decompose z
  25. 0025apply beta_product_succ_decompose
  26. 0026exact hproduct
  27. 0027cases hdecomp
  28. 0028cases hdecomp_witness
  29. 0029cases hdecomp_witness_witness
  30. 0030cases hdecomp_witness_witness_right
  31. 0031have hpw_prefix : ∀ frp_index_pointwise_prefix. ∀ frp_factor_pointwise_prefix. Lt(frp_index_pointwise_prefix,l) → BetaAt(b,c,frp_index_pointwise_prefix,frp_factor_pointwise_prefix) → Coprime(frp_factor_pointwise_prefix,m)
    Exact native replay linehave hpw_prefix : forall frp_index_pointwise_prefix frp_factor_pointwise_prefix. (exists frp_gap_pointwise_prefix_bound. frp_gap_pointwise_prefix_bound + S frp_index_pointwise_prefix = l) -> (((exists ff_h_frp_pointwise_prefix_decoded. ff_h_frp_pointwise_prefix_decoded + S (frp_factor_pointwise_prefix) = S ((S (frp_index_pointwise_prefix)) * c)) /\ exists ff_q_frp_pointwise_prefix_decoded. b = ff_q_frp_pointwise_prefix_decoded * S ((S (frp_index_pointwise_prefix)) * c) + (frp_factor_pointwise_prefix))) -> (forall frp_divisor_pointwise_prefix_coprime. (exists frp_left_factor_pointwise_prefix_coprime. frp_factor_pointwise_prefix = frp_divisor_pointwise_prefix_coprime * frp_left_factor_pointwise_prefix_coprime) -> (exists frp_right_factor_pointwise_prefix_coprime. m = frp_divisor_pointwise_prefix_coprime * frp_right_factor_pointwise_prefix_coprime) -> frp_divisor_pointwise_prefix_coprime = 1)
  32. 0032intro i
  33. 0033intro x2
  34. 0034intro hi
  35. 0035intro hx2
  36. 0036specialize hpw i
  37. 0037specialize hpw x2
  38. 0038apply hpw
  39. 0039specialize le_succ (S i)
  40. 0040specialize le_succ l
  41. 0041apply le_succ
  42. 0042exact hi
  43. 0043exact hx2
  44. 0044have hprefix : Coprime(x1,m)
    Exact native replay linehave hprefix : forall frp_divisor_prefix_result. (exists frp_left_factor_prefix_result. x1 = frp_divisor_prefix_result * frp_left_factor_prefix_result) -> (exists frp_right_factor_prefix_result. m = frp_divisor_prefix_result * frp_right_factor_prefix_result) -> frp_divisor_prefix_result = 1
  45. 0045specialize IH x1
  46. 0046apply IH
  47. 0047exact hpw_prefix
  48. 0048exact hdecomp_witness_witness_right_left
  49. 0049have hfactor : Coprime(x,m)
    Exact native replay linehave hfactor : forall frp_divisor_last_factor. (exists frp_left_factor_last_factor. x = frp_divisor_last_factor * frp_left_factor_last_factor) -> (exists frp_right_factor_last_factor. m = frp_divisor_last_factor * frp_right_factor_last_factor) -> frp_divisor_last_factor = 1
  50. 0050specialize hpw l
  51. 0051specialize hpw x
  52. 0052apply hpw
  53. 0053specialize le_refl (S l)
  54. 0054exact le_refl
  55. 0055exact hdecomp_witness_witness_left
  56. 0056rewrite hdecomp_witness_witness_right_right
  57. 0057specialize coprime_mul_left x1
  58. 0058specialize coprime_mul_left x
  59. 0059specialize coprime_mul_left m
  60. 0060apply coprime_mul_left
  61. 0061exact hprefix
  62. 0062exact hfactor