PA001T

coprime_mul_left

Stable checked-use theorem · independently closed

Coprimality with a fixed right operand is closed under multiplication on the left.

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.

Exact expanded PA statement

forall a b n. (forall d. (exists x. a = d * x) -> (exists y. n = d * y) -> d = 1) -> (forall d. (exists x. b = d * x) -> (exists y. n = d * y) -> d = 1) -> forall d. (exists x. a * b = d * x) -> (exists y. n = d * y) -> d = 1

Structural proof guide

Generated structural guide

Coprimality with a fixed right operand is closed under multiplication on the left.

Use the direct prerequisites multiple_trans, gauss_coprime_cancel as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA0018 multiple_trans PA001P gauss_coprime_cancel

Proof neighborhood

Direct dependencies

PA0018 multiple_trans PA001P gauss_coprime_cancel

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA0081 beta_product_pointwise_coprime

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

34 script commands · 6 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.

Named ingredients (2)
multiple transgauss coprime cancel
01Fix variables and assumptionsL1–8

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 han
  5. L5
    intro hbn
  6. L6
    intro d
  7. L7
    intro hab
  8. L8
    intro hdn
02Establish hdaL9–12

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hda : forall e. (exists u. d = e * u) -> (exists v. a = e * v) -> e = 1
  2. L10
    intro e
  3. L11
    intro hed
  4. L12
    intro hea
03Establish henL13–22

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

  1. L13
    have hen : exists q. n = e * q
  2. L14
    specialize multiple_trans d
  3. L15
    specialize multiple_trans e
  4. L16
    specialize multiple_trans n
  5. L17
    apply multiple_trans
  6. L18
    exact hdn
  7. L19
    exact hed
  8. L20
    specialize han e
  9. L21
    apply han
  10. L22
    exact hea
04Use earlier factsL23–23

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

  1. L23
    exact hen
05Establish hdbL24–33

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

  1. L24
    have hdb : exists w. b = d * w
  2. L25
    specialize gauss_coprime_cancel d
  3. L26
    specialize gauss_coprime_cancel a
  4. L27
    specialize gauss_coprime_cancel b
  5. L28
    apply gauss_coprime_cancel
  6. L29
    exact hda
  7. L30
    exact hab
  8. L31
    specialize hbn d
  9. L32
    apply hbn
  10. L33
    exact hdb
06Use earlier factsL34–34

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

  1. L34
    exact hdn

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro han
  5. 0005intro hbn
  6. 0006intro d
  7. 0007intro hab
  8. 0008intro hdn
  9. 0009have hda : forall e. (exists u. d = e * u) -> (exists v. a = e * v) -> e = 1
  10. 0010intro e
  11. 0011intro hed
  12. 0012intro hea
  13. 0013have hen : exists q. n = e * q
  14. 0014specialize multiple_trans d
  15. 0015specialize multiple_trans e
  16. 0016specialize multiple_trans n
  17. 0017apply multiple_trans
  18. 0018exact hdn
  19. 0019exact hed
  20. 0020specialize han e
  21. 0021apply han
  22. 0022exact hea
  23. 0023exact hen
  24. 0024have hdb : exists w. b = d * w
  25. 0025specialize gauss_coprime_cancel d
  26. 0026specialize gauss_coprime_cancel a
  27. 0027specialize gauss_coprime_cancel b
  28. 0028apply gauss_coprime_cancel
  29. 0029exact hda
  30. 0030exact hab
  31. 0031specialize hbn d
  32. 0032apply hbn
  33. 0033exact hdb
  34. 0034exact hdn