BT0039 · Bertrand theorem

gauss_coprime_cancel

Stable checked-use theorem · independently kernel verified

Cancel a coprime factor from a divisibility witness (Gauss cancellation).

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. ∀ z. Coprime(a,b) → Dvd(a,b · z) → Dvd(a,z)

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

PD0003 Dvd PD0005 Coprime

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b z. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> (exists q. b * z = a * q) -> exists w. z = a * w

Proof neighborhood

Direct theorem prerequisites

BT0028 multiple_refl BT0009 one_mul BT0038 coprime_balanced_bezout BT0036 balanced_combination_scale_right BT0037 common_divisor_divides_balanced_result

Direct theorem dependents

BT003N euclid_prime_dvd_product BT004K beta_moduli_coprime_of_gap_dvd BT004R coprime_mul_left BT00BG coprime_product_is_lcm

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

30 script commands · 5 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 (5)
multiple reflone mulcoprime balanced bezoutbalanced combination scale rightcommon divisor divides balanced result
01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro z
  4. L4
    intro hcop
  5. L5
    intro hdiv
02Establish hbezL6–8

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

  1. L6
    have hbez : exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)
  2. L7
    apply coprime_balanced_bezout
  3. L8
    exact hcop
03Separate the logical casesL9–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases hbez
  2. L10
    cases hbez_witness
  3. L11
    cases hbez_witness_witness
  4. L12
    cases hbez_witness_witness_witness
04Establish hscaledL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply balanced combination scale right.

  1. L13
    have hscaled : a * (x * z) + (b * z) * x1 = 1 * z + (a * (x2 * z) + (b * z) * x3)
  2. L14
    apply balanced_combination_scale_right
  3. L15
    exact hbez_witness_witness_witness_witness
  4. L16
    specialize one_mul z
  5. L17
    rewrite one_mul at hscaled
  6. L18
    specialize common_divisor_divides_balanced_result a
  7. L19
    specialize common_divisor_divides_balanced_result a
  8. L20
    specialize common_divisor_divides_balanced_result (b * z)
  9. L21
    specialize common_divisor_divides_balanced_result z
  10. L22
    specialize common_divisor_divides_balanced_result (x * z)
05Use earlier factsL23–30

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

  1. L23
    specialize common_divisor_divides_balanced_result x1
  2. L24
    specialize common_divisor_divides_balanced_result (x2 * z)
  3. L25
    specialize common_divisor_divides_balanced_result x3
  4. L26
    apply common_divisor_divides_balanced_result
  5. L27
    specialize multiple_refl a
  6. L28
    exact multiple_refl
  7. L29
    exact hdiv
  8. L30
    exact hscaled

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro z
  4. 0004intro hcop
  5. 0005intro hdiv
  6. 0006have hbez : exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)
  7. 0007apply coprime_balanced_bezout
  8. 0008exact hcop
  9. 0009cases hbez
  10. 0010cases hbez_witness
  11. 0011cases hbez_witness_witness
  12. 0012cases hbez_witness_witness_witness
  13. 0013have hscaled : a * (x * z) + (b * z) * x1 = 1 * z + (a * (x2 * z) + (b * z) * x3)
  14. 0014apply balanced_combination_scale_right
  15. 0015exact hbez_witness_witness_witness_witness
  16. 0016specialize one_mul z
  17. 0017rewrite one_mul at hscaled
  18. 0018specialize common_divisor_divides_balanced_result a
  19. 0019specialize common_divisor_divides_balanced_result a
  20. 0020specialize common_divisor_divides_balanced_result (b * z)
  21. 0021specialize common_divisor_divides_balanced_result z
  22. 0022specialize common_divisor_divides_balanced_result (x * z)
  23. 0023specialize common_divisor_divides_balanced_result x1
  24. 0024specialize common_divisor_divides_balanced_result (x2 * z)
  25. 0025specialize common_divisor_divides_balanced_result x3
  26. 0026apply common_divisor_divides_balanced_result
  27. 0027specialize multiple_refl a
  28. 0028exact multiple_refl
  29. 0029exact hdiv
  30. 0030exact hscaled