BT002S · Bertrand theorem

is_gcd_euclid_forward

Stable checked-use theorem · independently kernel verified

A relational gcd of divisor and remainder is a gcd of dividend and divisor.

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

∀ d. ∀ a. ∀ b. ∀ q. ∀ r. a = b · q + r → IsGCD(d,b,r) → IsGCD(d,a,b)

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

PD0006 IsGCD

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall d a b q r. a = b * q + r -> (((exists x. b = d * x) /\ (exists y. r = d * y)) /\ forall c. (exists u. b = c * u) -> (exists v. r = c * v) -> exists w. d = c * w) -> (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

Proof neighborhood

Direct theorem prerequisites

BT002H divides_remainder BT002I divides_linear_step

Direct theorem dependents

BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to

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

35 script commands · 7 reading checkpoints · 0 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)
divides remainderdivides linear step
01Fix variables and assumptionsL1–7

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro hstep
  7. L7
    intro hg
02Separate the logical casesL8–11

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

  1. L8
    cases hg
  2. L9
    cases hg_left
  3. L10
    split
  4. L11
    split
03Calculate and transport equalitiesL12–12

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

  1. L12
    rewrite hstep
04Use earlier factsL13–20

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

  1. L13
    specialize divides_linear_step d
  2. L14
    specialize divides_linear_step b
  3. L15
    specialize divides_linear_step q
  4. L16
    specialize divides_linear_step r
  5. L17
    apply divides_linear_step
  6. L18
    exact hg_left_left
  7. L19
    exact hg_left_right
  8. L20
    exact hg_left_left
05Fix variables and assumptionsL21–23

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

  1. L21
    intro c
  2. L22
    intro hca
  3. L23
    intro hcb
06Use earlier factsL24–33

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

  1. L24
    specialize hg_right c
  2. L25
    apply hg_right
  3. L26
    exact hcb
  4. L27
    specialize divides_remainder c
  5. L28
    specialize divides_remainder a
  6. L29
    specialize divides_remainder b
  7. L30
    specialize divides_remainder q
  8. L31
    specialize divides_remainder r
  9. L32
    apply divides_remainder
  10. L33
    exact hca
07Use earlier factsL34–35

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

  1. L34
    exact hcb
  2. L35
    exact hstep

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro q
  5. 0005intro r
  6. 0006intro hstep
  7. 0007intro hg
  8. 0008cases hg
  9. 0009cases hg_left
  10. 0010split
  11. 0011split
  12. 0012rewrite hstep
  13. 0013specialize divides_linear_step d
  14. 0014specialize divides_linear_step b
  15. 0015specialize divides_linear_step q
  16. 0016specialize divides_linear_step r
  17. 0017apply divides_linear_step
  18. 0018exact hg_left_left
  19. 0019exact hg_left_right
  20. 0020exact hg_left_left
  21. 0021intro c
  22. 0022intro hca
  23. 0023intro hcb
  24. 0024specialize hg_right c
  25. 0025apply hg_right
  26. 0026exact hcb
  27. 0027specialize divides_remainder c
  28. 0028specialize divides_remainder a
  29. 0029specialize divides_remainder b
  30. 0030specialize divides_remainder q
  31. 0031specialize divides_remainder r
  32. 0032apply divides_remainder
  33. 0033exact hca
  34. 0034exact hcb
  35. 0035exact hstep