FC0006

crt_gcd_lcm_distributes_nonzero

GCD distributes over the actual binary LCM for a nonzero left input and nonzero comparison input; the right input may be zero.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ n. ∀ L. ∀ ga. ∀ gb. ∀ g. ¬a = 0 → ¬n = 0 → Dvd(a,L) ∧ Dvd(b,L) ∧ (∀ x. Dvd(a,x) → Dvd(b,x) → Dvd(L,x)) → IsGCD(ga,a,n) → IsGCD(gb,b,n) → IsGCD(g,L,n) → Dvd(ga,g) ∧ Dvd(gb,g) ∧ (∀ x. Dvd(ga,x) → Dvd(gb,x) → Dvd(g,x))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Dvd(d,n) · 14IsGCD(g,a,b) · 5

Actual proof prerequisites

canonical_gcd_exists · checked external prerequisitecrt_gcd_nonzero_leftcrt_gcd_nonzero_rightcrt_gcd_coprime_cofactorsfactor_nonzero_right · checked external prerequisitecrt_lcm_gcd_cofactor_product · checked external prerequisitecrt_gcd_lcm_distributes_scaled_coprime
Original expanded first-order statement 
forall a b n L ga gb g. ~(a = 0) -> ~(n = 0) -> ((((exists hscale_left_factor_gfull_nonzero_L. L = a * hscale_left_factor_gfull_nonzero_L) /\ (exists hscale_right_factor_gfull_nonzero_L. L = b * hscale_right_factor_gfull_nonzero_L)) /\ forall hscale_common_gfull_nonzero_L. (exists hscale_left_common_gfull_nonzero_L. hscale_common_gfull_nonzero_L = a * hscale_left_common_gfull_nonzero_L) -> (exists hscale_right_common_gfull_nonzero_L. hscale_common_gfull_nonzero_L = b * hscale_right_common_gfull_nonzero_L) -> exists hscale_least_factor_gfull_nonzero_L. hscale_common_gfull_nonzero_L = L * hscale_least_factor_gfull_nonzero_L)) -> ((((exists ec_gcd_left_gfull_nonzero_ga. a = ga * ec_gcd_left_gfull_nonzero_ga) /\ (exists ec_gcd_right_gfull_nonzero_ga. n = ga * ec_gcd_right_gfull_nonzero_ga)) /\ forall ec_gcd_common_gfull_nonzero_ga. (exists ec_gcd_common_left_gfull_nonzero_ga. a = ec_gcd_common_gfull_nonzero_ga * ec_gcd_common_left_gfull_nonzero_ga) -> (exists ec_gcd_common_right_gfull_nonzero_ga. n = ec_gcd_common_gfull_nonzero_ga * ec_gcd_common_right_gfull_nonzero_ga) -> exists ec_gcd_greatest_gfull_nonzero_ga. ga = ec_gcd_common_gfull_nonzero_ga * ec_gcd_greatest_gfull_nonzero_ga)) -> ((((exists ec_gcd_left_gfull_nonzero_gb. b = gb * ec_gcd_left_gfull_nonzero_gb) /\ (exists ec_gcd_right_gfull_nonzero_gb. n = gb * ec_gcd_right_gfull_nonzero_gb)) /\ forall ec_gcd_common_gfull_nonzero_gb. (exists ec_gcd_common_left_gfull_nonzero_gb. b = ec_gcd_common_gfull_nonzero_gb * ec_gcd_common_left_gfull_nonzero_gb) -> (exists ec_gcd_common_right_gfull_nonzero_gb. n = ec_gcd_common_gfull_nonzero_gb * ec_gcd_common_right_gfull_nonzero_gb) -> exists ec_gcd_greatest_gfull_nonzero_gb. gb = ec_gcd_common_gfull_nonzero_gb * ec_gcd_greatest_gfull_nonzero_gb)) -> ((((exists ec_gcd_left_gfull_nonzero_g. L = g * ec_gcd_left_gfull_nonzero_g) /\ (exists ec_gcd_right_gfull_nonzero_g. n = g * ec_gcd_right_gfull_nonzero_g)) /\ forall ec_gcd_common_gfull_nonzero_g. (exists ec_gcd_common_left_gfull_nonzero_g. L = ec_gcd_common_gfull_nonzero_g * ec_gcd_common_left_gfull_nonzero_g) -> (exists ec_gcd_common_right_gfull_nonzero_g. n = ec_gcd_common_gfull_nonzero_g * ec_gcd_common_right_gfull_nonzero_g) -> exists ec_gcd_greatest_gfull_nonzero_g. g = ec_gcd_common_gfull_nonzero_g * ec_gcd_greatest_gfull_nonzero_g)) -> ((((exists hscale_left_factor_gfull_nonzero_result. g = ga * hscale_left_factor_gfull_nonzero_result) /\ (exists hscale_right_factor_gfull_nonzero_result. g = gb * hscale_right_factor_gfull_nonzero_result)) /\ forall hscale_common_gfull_nonzero_result. (exists hscale_left_common_gfull_nonzero_result. hscale_common_gfull_nonzero_result = ga * hscale_left_common_gfull_nonzero_result) -> (exists hscale_right_common_gfull_nonzero_result. hscale_common_gfull_nonzero_result = gb * hscale_right_common_gfull_nonzero_result) -> exists hscale_least_factor_gfull_nonzero_result. hscale_common_gfull_nonzero_result = g * hscale_least_factor_gfull_nonzero_result))

Complete tactic proof in conservative notation

All 111 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

111 script commands · 21 reading checkpoints · 8 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)
crt gcd nonzero leftcrt gcd coprime cofactorscrt gcd nonzero rightcrt gcd lcm distributes scaled coprime
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro n
  4. L4
    intro L
  5. L5
    intro ga
  6. L6
    intro gb
  7. L7
    intro g
  8. L8
    intro ha
  9. L9
    intro hn
  10. L10
    intro hL
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hga
  2. L12
    intro hgb
  3. L13
    intro hg
03Establish hdL14–17

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

  1. L14
    have hd : ∃ d. IsGCD(d,a,b)Definitions: IsGCD(d,a,b)Original native command in the exact edition
  2. L15
    specialize canonical_gcd_exists a
  3. L16
    specialize canonical_gcd_exists b
  4. L17
    apply canonical_gcd_exists
04Separate the logical casesL18–18

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

  1. L18
    cases hd
05Establish hdnonzeroL19–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt gcd nonzero left.

  1. L19
    have hdnonzero : ~(x = 0)
  2. L20
    intro hz
  3. L21
    specialize crt_gcd_nonzero_left a
  4. L22
    specialize crt_gcd_nonzero_left b
  5. L23
    specialize crt_gcd_nonzero_left x
  6. L24
    apply crt_gcd_nonzero_left
  7. L25
    exact ha
  8. L26
    exact hd_witness
  9. L27
    exact hz
06Establish habL28–34

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

  1. L28
    have hab : ∃ A. ∃ B. a = x · A ∧ (b = x · B ∧ (∀ y. Dvd(y,A) → Dvd(y,B) → y = 1))Definitions: Dvd(y,A)Dvd(y,B)Original native command in the exact edition
  2. L29
    specialize crt_gcd_coprime_cofactors a
  3. L30
    specialize crt_gcd_coprime_cofactors b
  4. L31
    specialize crt_gcd_coprime_cofactors x
  5. L32
    apply crt_gcd_coprime_cofactors
  6. L33
    exact hdnonzero
  7. L34
    exact hd_witness
07Separate the logical casesL35–38

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

  1. L35
    cases hab
  2. L36
    cases hab_witness
  3. L37
    cases hab_witness_witness
  4. L38
    cases hab_witness_witness_right
08Establish heL39–42

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

  1. L39
    have he : ∃ e. IsGCD(e,x,n)Definitions: IsGCD(e,x,n)Original native command in the exact edition
  2. L40
    specialize canonical_gcd_exists x
  3. L41
    specialize canonical_gcd_exists n
  4. L42
    apply canonical_gcd_exists
09Separate the logical casesL43–43

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

  1. L43
    cases he
10Establish henonzeroL44–52

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

  1. L44
    have henonzero : ~(x3 = 0)
  2. L45
    intro hz
  3. L46
    specialize crt_gcd_nonzero_right x
  4. L47
    specialize crt_gcd_nonzero_right n
  5. L48
    specialize crt_gcd_nonzero_right x3
  6. L49
    apply crt_gcd_nonzero_right
  7. L50
    exact hn
  8. L51
    exact he_witness
  9. L52
    exact hz
11Establish hdnL53–59

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

  1. L53
    have hdn : ∃ D. ∃ N. x = x3 · D ∧ (n = x3 · N ∧ (∀ y. Dvd(y,D) → Dvd(y,N) → y = 1))Definitions: Dvd(y,D)Dvd(y,N)Original native command in the exact edition
  2. L54
    specialize crt_gcd_coprime_cofactors x
  3. L55
    specialize crt_gcd_coprime_cofactors n
  4. L56
    specialize crt_gcd_coprime_cofactors x3
  5. L57
    apply crt_gcd_coprime_cofactors
  6. L58
    exact henonzero
  7. L59
    exact he_witness
12Separate the logical casesL60–63

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

  1. L60
    cases hdn
  2. L61
    cases hdn_witness
  3. L62
    cases hdn_witness_witness
  4. L63
    cases hdn_witness_witness_right
13Establish hNL64–72

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

  1. L64
    have hN : ~(x5 = 0)
  2. L65
    intro hz
  3. L66
    specialize factor_nonzero_right n
  4. L67
    specialize factor_nonzero_right x3
  5. L68
    specialize factor_nonzero_right x5
  6. L69
    apply factor_nonzero_right
  7. L70
    exact hn
  8. L71
    exact hdn_witness_witness_right_left
  9. L72
    exact hz
14Establish hLeqL73–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt lcm gcd cofactor product.

  1. L73
    have hLeq : L = x * (x1 * x2)
  2. L74
    specialize crt_lcm_gcd_cofactor_product a
  3. L75
    specialize crt_lcm_gcd_cofactor_product b
  4. L76
    specialize crt_lcm_gcd_cofactor_product x
  5. L77
    specialize crt_lcm_gcd_cofactor_product x1
  6. L78
    specialize crt_lcm_gcd_cofactor_product x2
  7. L79
    specialize crt_lcm_gcd_cofactor_product L
  8. L80
    apply crt_lcm_gcd_cofactor_product
  9. L81
    exact hdnonzero
  10. L82
    exact hab_witness_witness_left
15Use earlier factsL83–92

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

  1. L83
    exact hab_witness_witness_right_left
  2. L84
    exact hd_witness
  3. L85
    exact hL
  4. L86
    specialize crt_gcd_lcm_distributes_scaled_coprime x
  5. L87
    specialize crt_gcd_lcm_distributes_scaled_coprime n
  6. L88
    specialize crt_gcd_lcm_distributes_scaled_coprime x3
  7. L89
    specialize crt_gcd_lcm_distributes_scaled_coprime x4
  8. L90
    specialize crt_gcd_lcm_distributes_scaled_coprime x5
  9. L91
    specialize crt_gcd_lcm_distributes_scaled_coprime x1
  10. L92
    specialize crt_gcd_lcm_distributes_scaled_coprime x2
16Use earlier factsL93–102

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

  1. L93
    specialize crt_gcd_lcm_distributes_scaled_coprime L
  2. L94
    specialize crt_gcd_lcm_distributes_scaled_coprime ga
  3. L95
    specialize crt_gcd_lcm_distributes_scaled_coprime gb
  4. L96
    specialize crt_gcd_lcm_distributes_scaled_coprime g
  5. L97
    apply crt_gcd_lcm_distributes_scaled_coprime
  6. L98
    exact hdn_witness_witness_left
  7. L99
    exact hdn_witness_witness_right_left
  8. L100
    exact henonzero
  9. L101
    exact hN
  10. L102
    exact hdn_witness_witness_right_right
17Use earlier factsL103–104

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

  1. L103
    exact hab_witness_witness_right_right
  2. L104
    exact hLeq
18Calculate and transport equalitiesL105–106

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L105
    rewrite <- hab_witness_witness_left
  2. L106
    rewrite <- hab_witness_witness_left
19Use earlier factsL107–107

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

  1. L107
    exact hga
20Calculate and transport equalitiesL108–109

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L108
    rewrite <- hab_witness_witness_right_left
  2. L109
    rewrite <- hab_witness_witness_right_left
21Use earlier factsL110–111

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

  1. L110
    exact hgb
  2. L111
    exact hg

Library-wide reading audit

Original defined command ledger · 111 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro L
  5. 0005intro ga
  6. 0006intro gb
  7. 0007intro g
  8. 0008intro ha
  9. 0009intro hn
  10. 0010intro hL
  11. 0011intro hga
  12. 0012intro hgb
  13. 0013intro hg
  14. 0014have hd : ∃ d. IsGCD(d,a,b)
  15. 0015specialize canonical_gcd_exists a
  16. 0016specialize canonical_gcd_exists b
  17. 0017apply canonical_gcd_exists
  18. 0018cases hd
  19. 0019have hdnonzero : ~(x = 0)
  20. 0020intro hz
  21. 0021specialize crt_gcd_nonzero_left a
  22. 0022specialize crt_gcd_nonzero_left b
  23. 0023specialize crt_gcd_nonzero_left x
  24. 0024apply crt_gcd_nonzero_left
  25. 0025exact ha
  26. 0026exact hd_witness
  27. 0027exact hz
  28. 0028have hab : ∃ A. ∃ B. a = x · A ∧ (b = x · B ∧ (∀ y. Dvd(y,A) → Dvd(y,B) → y = 1))
  29. 0029specialize crt_gcd_coprime_cofactors a
  30. 0030specialize crt_gcd_coprime_cofactors b
  31. 0031specialize crt_gcd_coprime_cofactors x
  32. 0032apply crt_gcd_coprime_cofactors
  33. 0033exact hdnonzero
  34. 0034exact hd_witness
  35. 0035cases hab
  36. 0036cases hab_witness
  37. 0037cases hab_witness_witness
  38. 0038cases hab_witness_witness_right
  39. 0039have he : ∃ e. IsGCD(e,x,n)
  40. 0040specialize canonical_gcd_exists x
  41. 0041specialize canonical_gcd_exists n
  42. 0042apply canonical_gcd_exists
  43. 0043cases he
  44. 0044have henonzero : ~(x3 = 0)
  45. 0045intro hz
  46. 0046specialize crt_gcd_nonzero_right x
  47. 0047specialize crt_gcd_nonzero_right n
  48. 0048specialize crt_gcd_nonzero_right x3
  49. 0049apply crt_gcd_nonzero_right
  50. 0050exact hn
  51. 0051exact he_witness
  52. 0052exact hz
  53. 0053have hdn : ∃ D. ∃ N. x = x3 · D ∧ (n = x3 · N ∧ (∀ y. Dvd(y,D) → Dvd(y,N) → y = 1))
  54. 0054specialize crt_gcd_coprime_cofactors x
  55. 0055specialize crt_gcd_coprime_cofactors n
  56. 0056specialize crt_gcd_coprime_cofactors x3
  57. 0057apply crt_gcd_coprime_cofactors
  58. 0058exact henonzero
  59. 0059exact he_witness
  60. 0060cases hdn
  61. 0061cases hdn_witness
  62. 0062cases hdn_witness_witness
  63. 0063cases hdn_witness_witness_right
  64. 0064have hN : ~(x5 = 0)
  65. 0065intro hz
  66. 0066specialize factor_nonzero_right n
  67. 0067specialize factor_nonzero_right x3
  68. 0068specialize factor_nonzero_right x5
  69. 0069apply factor_nonzero_right
  70. 0070exact hn
  71. 0071exact hdn_witness_witness_right_left
  72. 0072exact hz
  73. 0073have hLeq : L = x * (x1 * x2)
  74. 0074specialize crt_lcm_gcd_cofactor_product a
  75. 0075specialize crt_lcm_gcd_cofactor_product b
  76. 0076specialize crt_lcm_gcd_cofactor_product x
  77. 0077specialize crt_lcm_gcd_cofactor_product x1
  78. 0078specialize crt_lcm_gcd_cofactor_product x2
  79. 0079specialize crt_lcm_gcd_cofactor_product L
  80. 0080apply crt_lcm_gcd_cofactor_product
  81. 0081exact hdnonzero
  82. 0082exact hab_witness_witness_left
  83. 0083exact hab_witness_witness_right_left
  84. 0084exact hd_witness
  85. 0085exact hL
  86. 0086specialize crt_gcd_lcm_distributes_scaled_coprime x
  87. 0087specialize crt_gcd_lcm_distributes_scaled_coprime n
  88. 0088specialize crt_gcd_lcm_distributes_scaled_coprime x3
  89. 0089specialize crt_gcd_lcm_distributes_scaled_coprime x4
  90. 0090specialize crt_gcd_lcm_distributes_scaled_coprime x5
  91. 0091specialize crt_gcd_lcm_distributes_scaled_coprime x1
  92. 0092specialize crt_gcd_lcm_distributes_scaled_coprime x2
  93. 0093specialize crt_gcd_lcm_distributes_scaled_coprime L
  94. 0094specialize crt_gcd_lcm_distributes_scaled_coprime ga
  95. 0095specialize crt_gcd_lcm_distributes_scaled_coprime gb
  96. 0096specialize crt_gcd_lcm_distributes_scaled_coprime g
  97. 0097apply crt_gcd_lcm_distributes_scaled_coprime
  98. 0098exact hdn_witness_witness_left
  99. 0099exact hdn_witness_witness_right_left
  100. 0100exact henonzero
  101. 0101exact hN
  102. 0102exact hdn_witness_witness_right_right
  103. 0103exact hab_witness_witness_right_right
  104. 0104exact hLeq
  105. 0105rewrite <- hab_witness_witness_left
  106. 0106rewrite <- hab_witness_witness_left
  107. 0107exact hga
  108. 0108rewrite <- hab_witness_witness_right_left
  109. 0109rewrite <- hab_witness_witness_right_left
  110. 0110exact hgb
  111. 0111exact hg