GC0015

crt_gcd_lcm_distributes_divisibility

GCD genuinely distributes over binary LCM whenever one modulus divides the other, including arbitrary zero inputs.

Alpha v34 checked-use · first admitted v25 · 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.

Historical partial components only: this chapter proves canonical solutions under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ n. ∀ L. ∀ ga. ∀ gb. ∀ g. Dvd(a,b) → 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) · 11IsGCD(g,a,b) · 3

Actual proof prerequisites

is_lcm_of_dvd · checked external prerequisiteis_lcm_unique · checked external prerequisiteis_gcd_unique · checked external prerequisitecrt_gcd_monotone_under_divisibility
Original expanded first-order statement 
forall a b n L ga gb g. (exists q. b = a * q) -> ((((exists hlcm_left_factor_gcomp_distribute_lcm. L = a * hlcm_left_factor_gcomp_distribute_lcm) /\ (exists hlcm_right_factor_gcomp_distribute_lcm. L = b * hlcm_right_factor_gcomp_distribute_lcm)) /\ forall hlcm_common_gcomp_distribute_lcm. (exists hlcm_left_common_gcomp_distribute_lcm. hlcm_common_gcomp_distribute_lcm = a * hlcm_left_common_gcomp_distribute_lcm) -> (exists hlcm_right_common_gcomp_distribute_lcm. hlcm_common_gcomp_distribute_lcm = b * hlcm_right_common_gcomp_distribute_lcm) -> exists hlcm_least_factor_gcomp_distribute_lcm. hlcm_common_gcomp_distribute_lcm = L * hlcm_least_factor_gcomp_distribute_lcm)) -> ((((exists hag_left_factor_gcomp_distribute_small. a = ga * hag_left_factor_gcomp_distribute_small) /\ (exists hag_right_factor_gcomp_distribute_small. n = ga * hag_right_factor_gcomp_distribute_small)) /\ forall hag_divisor_gcomp_distribute_small. (exists hag_common_left_gcomp_distribute_small. a = hag_divisor_gcomp_distribute_small * hag_common_left_gcomp_distribute_small) -> (exists hag_common_right_gcomp_distribute_small. n = hag_divisor_gcomp_distribute_small * hag_common_right_gcomp_distribute_small) -> exists hag_greatest_factor_gcomp_distribute_small. ga = hag_divisor_gcomp_distribute_small * hag_greatest_factor_gcomp_distribute_small)) -> ((((exists hag_left_factor_gcomp_distribute_large. b = gb * hag_left_factor_gcomp_distribute_large) /\ (exists hag_right_factor_gcomp_distribute_large. n = gb * hag_right_factor_gcomp_distribute_large)) /\ forall hag_divisor_gcomp_distribute_large. (exists hag_common_left_gcomp_distribute_large. b = hag_divisor_gcomp_distribute_large * hag_common_left_gcomp_distribute_large) -> (exists hag_common_right_gcomp_distribute_large. n = hag_divisor_gcomp_distribute_large * hag_common_right_gcomp_distribute_large) -> exists hag_greatest_factor_gcomp_distribute_large. gb = hag_divisor_gcomp_distribute_large * hag_greatest_factor_gcomp_distribute_large)) -> ((((exists hag_left_factor_gcomp_distribute_result_gcd. L = g * hag_left_factor_gcomp_distribute_result_gcd) /\ (exists hag_right_factor_gcomp_distribute_result_gcd. n = g * hag_right_factor_gcomp_distribute_result_gcd)) /\ forall hag_divisor_gcomp_distribute_result_gcd. (exists hag_common_left_gcomp_distribute_result_gcd. L = hag_divisor_gcomp_distribute_result_gcd * hag_common_left_gcomp_distribute_result_gcd) -> (exists hag_common_right_gcomp_distribute_result_gcd. n = hag_divisor_gcomp_distribute_result_gcd * hag_common_right_gcomp_distribute_result_gcd) -> exists hag_greatest_factor_gcomp_distribute_result_gcd. g = hag_divisor_gcomp_distribute_result_gcd * hag_greatest_factor_gcomp_distribute_result_gcd)) -> ((((exists hlcm_left_factor_gcomp_distribute_result_lcm. g = ga * hlcm_left_factor_gcomp_distribute_result_lcm) /\ (exists hlcm_right_factor_gcomp_distribute_result_lcm. g = gb * hlcm_right_factor_gcomp_distribute_result_lcm)) /\ forall hlcm_common_gcomp_distribute_result_lcm. (exists hlcm_left_common_gcomp_distribute_result_lcm. hlcm_common_gcomp_distribute_result_lcm = ga * hlcm_left_common_gcomp_distribute_result_lcm) -> (exists hlcm_right_common_gcomp_distribute_result_lcm. hlcm_common_gcomp_distribute_result_lcm = gb * hlcm_right_common_gcomp_distribute_result_lcm) -> exists hlcm_least_factor_gcomp_distribute_result_lcm. hlcm_common_gcomp_distribute_result_lcm = g * hlcm_least_factor_gcomp_distribute_result_lcm))

Complete unchanged native tactic proof

All 48 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

48 script commands · 9 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 (1)
crt gcd monotone under divisibility
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 hab
  9. L9
    intro hL
  10. L10
    intro hga
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hgb
  2. L12
    intro hg
03Establish hLeqL13–22

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

  1. L13
    have hLeq : L = b
  2. L14
    specialize is_lcm_unique L
  3. L15
    specialize is_lcm_unique b
  4. L16
    specialize is_lcm_unique a
  5. L17
    specialize is_lcm_unique b
  6. L18
    apply is_lcm_unique
  7. L19
    exact hL
  8. L20
    specialize is_lcm_of_dvd a
  9. L21
    specialize is_lcm_of_dvd b
  10. L22
    apply is_lcm_of_dvd
04Use earlier factsL23–23

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

  1. L23
    exact hab
05Calculate and transport equalitiesL24–25

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

  1. L24
    rewrite hLeq at hg
  2. L25
    rewrite hLeq at hg
06Establish hgeqL26–35

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

  1. L26
    have hgeq : g = gb
  2. L27
    specialize is_gcd_unique g
  3. L28
    specialize is_gcd_unique gb
  4. L29
    specialize is_gcd_unique b
  5. L30
    specialize is_gcd_unique n
  6. L31
    apply is_gcd_unique
  7. L32
    exact hg
  8. L33
    exact hgb
  9. L34
    rewrite hgeq
  10. L35
    rewrite hgeq
07Calculate and transport equalitiesL36–36

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

  1. L36
    rewrite hgeq
08Use earlier factsL37–46

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

  1. L37
    specialize is_lcm_of_dvd ga
  2. L38
    specialize is_lcm_of_dvd gb
  3. L39
    apply is_lcm_of_dvd
  4. L40
    specialize crt_gcd_monotone_under_divisibility a
  5. L41
    specialize crt_gcd_monotone_under_divisibility b
  6. L42
    specialize crt_gcd_monotone_under_divisibility n
  7. L43
    specialize crt_gcd_monotone_under_divisibility ga
  8. L44
    specialize crt_gcd_monotone_under_divisibility gb
  9. L45
    apply crt_gcd_monotone_under_divisibility
  10. L46
    exact hab
09Use earlier factsL47–48

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

  1. L47
    exact hga
  2. L48
    exact hgb

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro L
  5. 0005intro ga
  6. 0006intro gb
  7. 0007intro g
  8. 0008intro hab
  9. 0009intro hL
  10. 0010intro hga
  11. 0011intro hgb
  12. 0012intro hg
  13. 0013have hLeq : L = b
  14. 0014specialize is_lcm_unique L
  15. 0015specialize is_lcm_unique b
  16. 0016specialize is_lcm_unique a
  17. 0017specialize is_lcm_unique b
  18. 0018apply is_lcm_unique
  19. 0019exact hL
  20. 0020specialize is_lcm_of_dvd a
  21. 0021specialize is_lcm_of_dvd b
  22. 0022apply is_lcm_of_dvd
  23. 0023exact hab
  24. 0024rewrite hLeq at hg
  25. 0025rewrite hLeq at hg
  26. 0026have hgeq : g = gb
  27. 0027specialize is_gcd_unique g
  28. 0028specialize is_gcd_unique gb
  29. 0029specialize is_gcd_unique b
  30. 0030specialize is_gcd_unique n
  31. 0031apply is_gcd_unique
  32. 0032exact hg
  33. 0033exact hgb
  34. 0034rewrite hgeq
  35. 0035rewrite hgeq
  36. 0036rewrite hgeq
  37. 0037specialize is_lcm_of_dvd ga
  38. 0038specialize is_lcm_of_dvd gb
  39. 0039apply is_lcm_of_dvd
  40. 0040specialize crt_gcd_monotone_under_divisibility a
  41. 0041specialize crt_gcd_monotone_under_divisibility b
  42. 0042specialize crt_gcd_monotone_under_divisibility n
  43. 0043specialize crt_gcd_monotone_under_divisibility ga
  44. 0044specialize crt_gcd_monotone_under_divisibility gb
  45. 0045apply crt_gcd_monotone_under_divisibility
  46. 0046exact hab
  47. 0047exact hga
  48. 0048exact hgb