MX000C

coprime_divisor_gcd_product

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The two genuine gcds multiply to the given positive divisor of a coprime product.

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 expanded first-order arithmetic statement

forall m n d a b. ~(d=0) -> (forall sfd_common_divisor_cdp_product_coprime. (exists pvs_factor_cdp_product_coprimeleft. (m) = (sfd_common_divisor_cdp_product_coprime) * pvs_factor_cdp_product_coprimeleft) -> (exists pvs_factor_cdp_product_coprimeright. (n) = (sfd_common_divisor_cdp_product_coprime) * pvs_factor_cdp_product_coprimeright) -> sfd_common_divisor_cdp_product_coprime = 1) -> (exists pvs_factor_cdp_product_divisor. (m*n) = (d) * pvs_factor_cdp_product_divisor) -> ((((exists ec_gcd_left_cor_cdp_product_left. m = a * ec_gcd_left_cor_cdp_product_left) /\ (exists ec_gcd_right_cor_cdp_product_left. d = a * ec_gcd_right_cor_cdp_product_left)) /\ forall ec_gcd_common_cor_cdp_product_left. (exists ec_gcd_common_left_cor_cdp_product_left. m = ec_gcd_common_cor_cdp_product_left * ec_gcd_common_left_cor_cdp_product_left) -> (exists ec_gcd_common_right_cor_cdp_product_left. d = ec_gcd_common_cor_cdp_product_left * ec_gcd_common_right_cor_cdp_product_left) -> exists ec_gcd_greatest_cor_cdp_product_left. a = ec_gcd_common_cor_cdp_product_left * ec_gcd_greatest_cor_cdp_product_left)) -> ((((exists ec_gcd_left_cor_cdp_product_right. n = b * ec_gcd_left_cor_cdp_product_right) /\ (exists ec_gcd_right_cor_cdp_product_right. d = b * ec_gcd_right_cor_cdp_product_right)) /\ forall ec_gcd_common_cor_cdp_product_right. (exists ec_gcd_common_left_cor_cdp_product_right. n = ec_gcd_common_cor_cdp_product_right * ec_gcd_common_left_cor_cdp_product_right) -> (exists ec_gcd_common_right_cor_cdp_product_right. d = ec_gcd_common_cor_cdp_product_right * ec_gcd_common_right_cor_cdp_product_right) -> exists ec_gcd_greatest_cor_cdp_product_right. b = ec_gcd_common_cor_cdp_product_right * ec_gcd_greatest_cor_cdp_product_right)) -> d=a*b

Constructive proof overview

Generated structural guide

The two genuine gcds multiply to the given positive divisor of a coprime product.

The unchanged tactic script uses 4 declared prerequisites and contains 43 exact native proof lines.

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

Proof neighborhood

Direct dependencies

crt_is_gcd_coprime_product Alpha theorem; checked-use authorized is_gcd_of_dvd Stable theorem; checked-use authorized is_gcd_symm Stable theorem; checked-use authorized is_gcd_unique Stable theorem; checked-use authorized

Direct dependents

MX000F coprime_divisor_factor_pair_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

43 script commands · 7 reading checkpoints · 3 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro hd
  7. L7
    intro hc
  8. L8
    intro hdiv
  9. L9
    intro ha
  10. L10
    intro hb
02Establish hprodL11–20

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

  1. L11
    have hprod : (((exists ec_gcd_left_cor_cdp_product. (m * n) = (a * b) * ec_gcd_left_cor_cdp_product) /\ (exists ec_gcd_right_cor_cdp_product. d = (a * b) * ec_gcd_right_cor_cdp_product)) /\ forall ec_gcd_common_cor_cdp_product. (exists ec_gcd_common_left_cor_cdp_product. (m * n) = ec_gcd_common_cor_cdp_product * ec_gcd_common_left_cor_cdp_product) -> (exists ec_gcd_common_right_cor_cdp_product. d = ec_gcd_common_cor_cdp_product * ec_gcd_common_right_cor_cdp_product) -> exists ec_gcd_greatest_cor_cdp_product. (a * b) = ec_gcd_common_cor_cdp_product * ec_gcd_greatest_cor_cdp_product)
  2. L12
    specialize crt_is_gcd_coprime_product (m)
  3. L13
    specialize crt_is_gcd_coprime_product (n)
  4. L14
    specialize crt_is_gcd_coprime_product (d)
  5. L15
    specialize crt_is_gcd_coprime_product (a)
  6. L16
    specialize crt_is_gcd_coprime_product (b)
  7. L17
    specialize crt_is_gcd_coprime_product (a*b)
  8. L18
    specialize crt_is_gcd_coprime_product (m*n)
  9. L19
    apply crt_is_gcd_coprime_product
  10. L20
    exact hd
03Calculate and transport equalitiesL21–22

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

  1. L21
    refl
  2. L22
    refl
04Use earlier factsL23–25

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

  1. L23
    exact hc
  2. L24
    exact ha
  3. L25
    exact hb
05Establish hselfL26–30

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

  1. L26
    have hself : (((exists ec_gcd_left_cor_cdp_self. d = d * ec_gcd_left_cor_cdp_self) /\ (exists ec_gcd_right_cor_cdp_self. (m * n) = d * ec_gcd_right_cor_cdp_self)) /\ forall ec_gcd_common_cor_cdp_self. (exists ec_gcd_common_left_cor_cdp_self. d = ec_gcd_common_cor_cdp_self * ec_gcd_common_left_cor_cdp_self) -> (exists ec_gcd_common_right_cor_cdp_self. (m * n) = ec_gcd_common_cor_cdp_self * ec_gcd_common_right_cor_cdp_self) -> exists ec_gcd_greatest_cor_cdp_self. d = ec_gcd_common_cor_cdp_self * ec_gcd_greatest_cor_cdp_self)
  2. L27
    specialize is_gcd_of_dvd (d)
  3. L28
    specialize is_gcd_of_dvd (m*n)
  4. L29
    apply is_gcd_of_dvd
  5. L30
    exact hdiv
06Establish hswapL31–40

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

  1. L31
    have hswap : (((exists ec_gcd_left_cor_cdp_swap. (m * n) = d * ec_gcd_left_cor_cdp_swap) /\ (exists ec_gcd_right_cor_cdp_swap. d = d * ec_gcd_right_cor_cdp_swap)) /\ forall ec_gcd_common_cor_cdp_swap. (exists ec_gcd_common_left_cor_cdp_swap. (m * n) = ec_gcd_common_cor_cdp_swap * ec_gcd_common_left_cor_cdp_swap) -> (exists ec_gcd_common_right_cor_cdp_swap. d = ec_gcd_common_cor_cdp_swap * ec_gcd_common_right_cor_cdp_swap) -> exists ec_gcd_greatest_cor_cdp_swap. d = ec_gcd_common_cor_cdp_swap * ec_gcd_greatest_cor_cdp_swap)
  2. L32
    specialize is_gcd_symm (d)
  3. L33
    specialize is_gcd_symm (d)
  4. L34
    specialize is_gcd_symm (m*n)
  5. L35
    apply is_gcd_symm
  6. L36
    exact hself
  7. L37
    specialize is_gcd_unique (d)
  8. L38
    specialize is_gcd_unique (a*b)
  9. L39
    specialize is_gcd_unique (m*n)
  10. L40
    specialize is_gcd_unique (d)
07Use earlier factsL41–43

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

  1. L41
    apply is_gcd_unique
  2. L42
    exact hswap
  3. L43
    exact hprod

Library-wide reading audit

Original exact command ledger · 43 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro d
  4. 0004intro a
  5. 0005intro b
  6. 0006intro hd
  7. 0007intro hc
  8. 0008intro hdiv
  9. 0009intro ha
  10. 0010intro hb
  11. 0011have hprod : (((exists ec_gcd_left_cor_cdp_product. (m * n) = (a * b) * ec_gcd_left_cor_cdp_product) /\ (exists ec_gcd_right_cor_cdp_product. d = (a * b) * ec_gcd_right_cor_cdp_product)) /\ forall ec_gcd_common_cor_cdp_product. (exists ec_gcd_common_left_cor_cdp_product. (m * n) = ec_gcd_common_cor_cdp_product * ec_gcd_common_left_cor_cdp_product) -> (exists ec_gcd_common_right_cor_cdp_product. d = ec_gcd_common_cor_cdp_product * ec_gcd_common_right_cor_cdp_product) -> exists ec_gcd_greatest_cor_cdp_product. (a * b) = ec_gcd_common_cor_cdp_product * ec_gcd_greatest_cor_cdp_product)
  12. 0012specialize crt_is_gcd_coprime_product (m)
  13. 0013specialize crt_is_gcd_coprime_product (n)
  14. 0014specialize crt_is_gcd_coprime_product (d)
  15. 0015specialize crt_is_gcd_coprime_product (a)
  16. 0016specialize crt_is_gcd_coprime_product (b)
  17. 0017specialize crt_is_gcd_coprime_product (a*b)
  18. 0018specialize crt_is_gcd_coprime_product (m*n)
  19. 0019apply crt_is_gcd_coprime_product
  20. 0020exact hd
  21. 0021refl
  22. 0022refl
  23. 0023exact hc
  24. 0024exact ha
  25. 0025exact hb
  26. 0026have hself : (((exists ec_gcd_left_cor_cdp_self. d = d * ec_gcd_left_cor_cdp_self) /\ (exists ec_gcd_right_cor_cdp_self. (m * n) = d * ec_gcd_right_cor_cdp_self)) /\ forall ec_gcd_common_cor_cdp_self. (exists ec_gcd_common_left_cor_cdp_self. d = ec_gcd_common_cor_cdp_self * ec_gcd_common_left_cor_cdp_self) -> (exists ec_gcd_common_right_cor_cdp_self. (m * n) = ec_gcd_common_cor_cdp_self * ec_gcd_common_right_cor_cdp_self) -> exists ec_gcd_greatest_cor_cdp_self. d = ec_gcd_common_cor_cdp_self * ec_gcd_greatest_cor_cdp_self)
  27. 0027specialize is_gcd_of_dvd (d)
  28. 0028specialize is_gcd_of_dvd (m*n)
  29. 0029apply is_gcd_of_dvd
  30. 0030exact hdiv
  31. 0031have hswap : (((exists ec_gcd_left_cor_cdp_swap. (m * n) = d * ec_gcd_left_cor_cdp_swap) /\ (exists ec_gcd_right_cor_cdp_swap. d = d * ec_gcd_right_cor_cdp_swap)) /\ forall ec_gcd_common_cor_cdp_swap. (exists ec_gcd_common_left_cor_cdp_swap. (m * n) = ec_gcd_common_cor_cdp_swap * ec_gcd_common_left_cor_cdp_swap) -> (exists ec_gcd_common_right_cor_cdp_swap. d = ec_gcd_common_cor_cdp_swap * ec_gcd_common_right_cor_cdp_swap) -> exists ec_gcd_greatest_cor_cdp_swap. d = ec_gcd_common_cor_cdp_swap * ec_gcd_greatest_cor_cdp_swap)
  32. 0032specialize is_gcd_symm (d)
  33. 0033specialize is_gcd_symm (d)
  34. 0034specialize is_gcd_symm (m*n)
  35. 0035apply is_gcd_symm
  36. 0036exact hself
  37. 0037specialize is_gcd_unique (d)
  38. 0038specialize is_gcd_unique (a*b)
  39. 0039specialize is_gcd_unique (m*n)
  40. 0040specialize is_gcd_unique (d)
  41. 0041apply is_gcd_unique
  42. 0042exact hswap
  43. 0043exact hprod