BT00BG

coprime_product_is_lcm

Stable · empty-context checked

The product of coprime naturals satisfies the universal relational LCM specification.

Exact expanded PA statement

forall a b. (forall d. (exists u. a = d * u) -> (exists v. b = d * v) -> d = 1) -> ((((exists hlcm_left_factor_coprime_product. a * b = a * hlcm_left_factor_coprime_product) /\ (exists hlcm_right_factor_coprime_product. a * b = b * hlcm_right_factor_coprime_product)) /\ forall hlcm_common_coprime_product. (exists hlcm_left_common_coprime_product. hlcm_common_coprime_product = a * hlcm_left_common_coprime_product) -> (exists hlcm_right_common_coprime_product. hlcm_common_coprime_product = b * hlcm_right_common_coprime_product) -> exists hlcm_least_factor_coprime_product. hlcm_common_coprime_product = a * b * hlcm_least_factor_coprime_product))

Structural proof guide

The product of coprime naturals satisfies the universal relational LCM specification.

Direct prerequisites: mul_comm, gauss_coprime_cancel, mul_assoc. The authored body proceeds by case analysis (3), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT0039 gauss_coprime_cancel BT0008 mul_assoc

Direct dependents

BT00VD beta_pairwise_coprime_product_divides_common_multiple

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro hcop
  4. 0004split
  5. 0005split
  6. 0006exists b
  7. 0007refl
  8. 0008exists a
  9. 0009apply mul_comm
  10. 0010intro c
  11. 0011intro ha
  12. 0012intro hb
  13. 0013cases ha
  14. 0014cases hb
  15. 0015have hdiv : exists q. b * x1 = a * q
  16. 0016exists x
  17. 0017trans c
  18. 0018symm
  19. 0019exact hb_witness
  20. 0020exact ha_witness
  21. 0021have hfactor : exists w. x1 = a * w
  22. 0022specialize gauss_coprime_cancel a
  23. 0023specialize gauss_coprime_cancel b
  24. 0024specialize gauss_coprime_cancel x1
  25. 0025apply gauss_coprime_cancel
  26. 0026exact hcop
  27. 0027exact hdiv
  28. 0028cases hfactor
  29. 0029exists x2
  30. 0030trans b * x1
  31. 0031exact hb_witness
  32. 0032trans b * (a * x2)
  33. 0033rewrite hfactor_witness
  34. 0034refl
  35. 0035trans (b * a) * x2
  36. 0036symm
  37. 0037apply mul_assoc
  38. 0038congr
  39. 0039apply mul_comm
  40. 0040refl