BT004R · Bertrand theorem

coprime_mul_left

Stable checked-use theorem · independently kernel verified

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.

Statement with defined notation

∀ a. ∀ b. ∀ n. Coprime(a,n) → Coprime(b,n) → Coprime(a · b,n)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0005 Coprime

3 occurrences

In local proof propositions

PD0003 Dvd PD0005 Coprime

3 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

BT002C multiple_trans BT0039 gauss_coprime_cancel

Direct theorem dependents

BT004S coprime_mul_right BT0059 beta_exclusive_accumulated_product_step BT00DH beta_product_pointwise_coprime BT00YV coprime_powers

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

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 (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
  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
  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
  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 defined 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 : Coprime(d,a)
    Exact native replay linehave 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 : Dvd(e,n)
    Exact native replay linehave 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 : Dvd(d,b)
    Exact native replay linehave 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