FC0009

crt_gcd_lcm_distributes

Unconditional constructive gcd(lcm(a,b),n)=lcm(gcd(a,n),gcd(b,n)), including every zero boundary.

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. 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) · 10IsGCD(g,a,b) · 3

Actual proof prerequisites

eq_decidable · checked external prerequisitecrt_gcd_lcm_distributes_zero_leftcrt_gcd_lcm_distributes_zero_comparisoncrt_gcd_lcm_distributes_nonzero
Original expanded first-order statement 
forall a b n L ga gb g. ((((exists hscale_left_factor_gfull_full_L. L = a * hscale_left_factor_gfull_full_L) /\ (exists hscale_right_factor_gfull_full_L. L = b * hscale_right_factor_gfull_full_L)) /\ forall hscale_common_gfull_full_L. (exists hscale_left_common_gfull_full_L. hscale_common_gfull_full_L = a * hscale_left_common_gfull_full_L) -> (exists hscale_right_common_gfull_full_L. hscale_common_gfull_full_L = b * hscale_right_common_gfull_full_L) -> exists hscale_least_factor_gfull_full_L. hscale_common_gfull_full_L = L * hscale_least_factor_gfull_full_L)) -> ((((exists ec_gcd_left_gfull_full_ga. a = ga * ec_gcd_left_gfull_full_ga) /\ (exists ec_gcd_right_gfull_full_ga. n = ga * ec_gcd_right_gfull_full_ga)) /\ forall ec_gcd_common_gfull_full_ga. (exists ec_gcd_common_left_gfull_full_ga. a = ec_gcd_common_gfull_full_ga * ec_gcd_common_left_gfull_full_ga) -> (exists ec_gcd_common_right_gfull_full_ga. n = ec_gcd_common_gfull_full_ga * ec_gcd_common_right_gfull_full_ga) -> exists ec_gcd_greatest_gfull_full_ga. ga = ec_gcd_common_gfull_full_ga * ec_gcd_greatest_gfull_full_ga)) -> ((((exists ec_gcd_left_gfull_full_gb. b = gb * ec_gcd_left_gfull_full_gb) /\ (exists ec_gcd_right_gfull_full_gb. n = gb * ec_gcd_right_gfull_full_gb)) /\ forall ec_gcd_common_gfull_full_gb. (exists ec_gcd_common_left_gfull_full_gb. b = ec_gcd_common_gfull_full_gb * ec_gcd_common_left_gfull_full_gb) -> (exists ec_gcd_common_right_gfull_full_gb. n = ec_gcd_common_gfull_full_gb * ec_gcd_common_right_gfull_full_gb) -> exists ec_gcd_greatest_gfull_full_gb. gb = ec_gcd_common_gfull_full_gb * ec_gcd_greatest_gfull_full_gb)) -> ((((exists ec_gcd_left_gfull_full_g. L = g * ec_gcd_left_gfull_full_g) /\ (exists ec_gcd_right_gfull_full_g. n = g * ec_gcd_right_gfull_full_g)) /\ forall ec_gcd_common_gfull_full_g. (exists ec_gcd_common_left_gfull_full_g. L = ec_gcd_common_gfull_full_g * ec_gcd_common_left_gfull_full_g) -> (exists ec_gcd_common_right_gfull_full_g. n = ec_gcd_common_gfull_full_g * ec_gcd_common_right_gfull_full_g) -> exists ec_gcd_greatest_gfull_full_g. g = ec_gcd_common_gfull_full_g * ec_gcd_greatest_gfull_full_g)) -> ((((exists hscale_left_factor_gfull_full_result. g = ga * hscale_left_factor_gfull_full_result) /\ (exists hscale_right_factor_gfull_full_result. g = gb * hscale_right_factor_gfull_full_result)) /\ forall hscale_common_gfull_full_result. (exists hscale_left_common_gfull_full_result. hscale_common_gfull_full_result = ga * hscale_left_common_gfull_full_result) -> (exists hscale_right_common_gfull_full_result. hscale_common_gfull_full_result = gb * hscale_right_common_gfull_full_result) -> exists hscale_least_factor_gfull_full_result. hscale_common_gfull_full_result = g * hscale_least_factor_gfull_full_result))

Complete tactic proof in conservative notation

All 61 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

61 script commands · 11 reading checkpoints · 2 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 (3)
crt gcd lcm distributes zero leftcrt gcd lcm distributes zero comparisoncrt gcd lcm distributes nonzero
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 hL
  9. L9
    intro hga
  10. L10
    intro hgb
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hg
03Establish haL12–15

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

  1. L12
    have ha : a = 0 \/ ~(a = 0)
  2. L13
    specialize eq_decidable a
  3. L14
    specialize eq_decidable 0
  4. L15
    apply eq_decidable
04Separate the logical casesL16–16

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

  1. L16
    cases ha
05Use earlier factsL17–26

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

  1. L17
    specialize crt_gcd_lcm_distributes_zero_left a
  2. L18
    specialize crt_gcd_lcm_distributes_zero_left b
  3. L19
    specialize crt_gcd_lcm_distributes_zero_left n
  4. L20
    specialize crt_gcd_lcm_distributes_zero_left L
  5. L21
    specialize crt_gcd_lcm_distributes_zero_left ga
  6. L22
    specialize crt_gcd_lcm_distributes_zero_left gb
  7. L23
    specialize crt_gcd_lcm_distributes_zero_left g
  8. L24
    apply crt_gcd_lcm_distributes_zero_left
  9. L25
    exact ha_left
  10. L26
    exact hL
06Use earlier factsL27–29

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

  1. L27
    exact hga
  2. L28
    exact hgb
  3. L29
    exact hg
07Establish hnL30–33

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

  1. L30
    have hn : n = 0 \/ ~(n = 0)
  2. L31
    specialize eq_decidable n
  3. L32
    specialize eq_decidable 0
  4. L33
    apply eq_decidable
08Separate the logical casesL34–34

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

  1. L34
    cases hn
09Use earlier factsL35–44

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

  1. L35
    specialize crt_gcd_lcm_distributes_zero_comparison a
  2. L36
    specialize crt_gcd_lcm_distributes_zero_comparison b
  3. L37
    specialize crt_gcd_lcm_distributes_zero_comparison n
  4. L38
    specialize crt_gcd_lcm_distributes_zero_comparison L
  5. L39
    specialize crt_gcd_lcm_distributes_zero_comparison ga
  6. L40
    specialize crt_gcd_lcm_distributes_zero_comparison gb
  7. L41
    specialize crt_gcd_lcm_distributes_zero_comparison g
  8. L42
    apply crt_gcd_lcm_distributes_zero_comparison
  9. L43
    exact hn_left
  10. L44
    exact hL
10Use earlier factsL45–54

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

  1. L45
    exact hga
  2. L46
    exact hgb
  3. L47
    exact hg
  4. L48
    specialize crt_gcd_lcm_distributes_nonzero a
  5. L49
    specialize crt_gcd_lcm_distributes_nonzero b
  6. L50
    specialize crt_gcd_lcm_distributes_nonzero n
  7. L51
    specialize crt_gcd_lcm_distributes_nonzero L
  8. L52
    specialize crt_gcd_lcm_distributes_nonzero ga
  9. L53
    specialize crt_gcd_lcm_distributes_nonzero gb
  10. L54
    specialize crt_gcd_lcm_distributes_nonzero g
11Use earlier factsL55–61

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

  1. L55
    apply crt_gcd_lcm_distributes_nonzero
  2. L56
    exact ha_right
  3. L57
    exact hn_right
  4. L58
    exact hL
  5. L59
    exact hga
  6. L60
    exact hgb
  7. L61
    exact hg

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro L
  5. 0005intro ga
  6. 0006intro gb
  7. 0007intro g
  8. 0008intro hL
  9. 0009intro hga
  10. 0010intro hgb
  11. 0011intro hg
  12. 0012have ha : a = 0 \/ ~(a = 0)
  13. 0013specialize eq_decidable a
  14. 0014specialize eq_decidable 0
  15. 0015apply eq_decidable
  16. 0016cases ha
  17. 0017specialize crt_gcd_lcm_distributes_zero_left a
  18. 0018specialize crt_gcd_lcm_distributes_zero_left b
  19. 0019specialize crt_gcd_lcm_distributes_zero_left n
  20. 0020specialize crt_gcd_lcm_distributes_zero_left L
  21. 0021specialize crt_gcd_lcm_distributes_zero_left ga
  22. 0022specialize crt_gcd_lcm_distributes_zero_left gb
  23. 0023specialize crt_gcd_lcm_distributes_zero_left g
  24. 0024apply crt_gcd_lcm_distributes_zero_left
  25. 0025exact ha_left
  26. 0026exact hL
  27. 0027exact hga
  28. 0028exact hgb
  29. 0029exact hg
  30. 0030have hn : n = 0 \/ ~(n = 0)
  31. 0031specialize eq_decidable n
  32. 0032specialize eq_decidable 0
  33. 0033apply eq_decidable
  34. 0034cases hn
  35. 0035specialize crt_gcd_lcm_distributes_zero_comparison a
  36. 0036specialize crt_gcd_lcm_distributes_zero_comparison b
  37. 0037specialize crt_gcd_lcm_distributes_zero_comparison n
  38. 0038specialize crt_gcd_lcm_distributes_zero_comparison L
  39. 0039specialize crt_gcd_lcm_distributes_zero_comparison ga
  40. 0040specialize crt_gcd_lcm_distributes_zero_comparison gb
  41. 0041specialize crt_gcd_lcm_distributes_zero_comparison g
  42. 0042apply crt_gcd_lcm_distributes_zero_comparison
  43. 0043exact hn_left
  44. 0044exact hL
  45. 0045exact hga
  46. 0046exact hgb
  47. 0047exact hg
  48. 0048specialize crt_gcd_lcm_distributes_nonzero a
  49. 0049specialize crt_gcd_lcm_distributes_nonzero b
  50. 0050specialize crt_gcd_lcm_distributes_nonzero n
  51. 0051specialize crt_gcd_lcm_distributes_nonzero L
  52. 0052specialize crt_gcd_lcm_distributes_nonzero ga
  53. 0053specialize crt_gcd_lcm_distributes_nonzero gb
  54. 0054specialize crt_gcd_lcm_distributes_nonzero g
  55. 0055apply crt_gcd_lcm_distributes_nonzero
  56. 0056exact ha_right
  57. 0057exact hn_right
  58. 0058exact hL
  59. 0059exact hga
  60. 0060exact hgb
  61. 0061exact hg