BT001S · Bertrand theorem

positive_quotient_gap_impossible

Stable checked-use theorem · independently kernel verified

A positive gap between quotients makes two bounded-remainder decompositions unequal.

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

∀ m. ∀ q. ∀ q2. ∀ r. ∀ s. ∀ k. Lt(r,m) → S k + q = q2 → ¬m · q + r = m · q2 + s

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

PD0002 Lt

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall m q q2 r s k. (exists z. z + S r = m) -> S k + q = q2 -> ~(m * q + r = m * q2 + s)

Proof neighborhood

Direct theorem prerequisites

BT0002 add_comm BT0003 add_assoc BT0007 mul_add BT000V add_left_cancel BT001K lt_not_eq_add_middle

Direct theorem dependents

BT001U division_remainder_unique

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 · 10 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 (5)
add commadd assocmul addadd left cancellt not eq add middle
01Fix variables and assumptionsL1–9

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

  1. L1
    intro m
  2. L2
    intro q
  3. L3
    intro q2
  4. L4
    intro r
  5. L5
    intro s
  6. L6
    intro k
  7. L7
    intro hr
  8. L8
    intro hgap
  9. L9
    intro heq
02Use earlier factsL10–19

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

  1. L10
    specialize lt_not_eq_add_middle r
  2. L11
    specialize lt_not_eq_add_middle m
  3. L12
    specialize lt_not_eq_add_middle (m * k)
  4. L13
    specialize lt_not_eq_add_middle s
  5. L14
    apply lt_not_eq_add_middle
  6. L15
    exact hr
  7. L16
    specialize add_left_cancel (m * q)
  8. L17
    specialize add_left_cancel r
  9. L18
    specialize add_left_cancel ((m * k + m) + s)
  10. L19
    apply add_left_cancel
03Calculate and transport equalitiesL20–20

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

  1. L20
    trans m * q2 + s
04Use earlier factsL21–21

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

  1. L21
    exact heq
05Calculate and transport equalitiesL22–22

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

  1. L22
    rewrite <- hgap
06Use earlier factsL23–24

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

  1. L23
    specialize add_comm S k
  2. L24
    specialize add_comm q
07Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite add_comm
08Use earlier factsL26–28

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

  1. L26
    specialize mul_add m
  2. L27
    specialize mul_add q
  3. L28
    specialize mul_add S k
09Calculate and transport equalitiesL29–30

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

  1. L29
    rewrite mul_add
  2. L30
    rewrite PA6
10Use earlier factsL31–34

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

  1. L31
    specialize add_assoc (m * q)
  2. L32
    specialize add_assoc (m * k + m)
  3. L33
    specialize add_assoc s
  4. L34
    apply add_assoc

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro m
  2. 0002intro q
  3. 0003intro q2
  4. 0004intro r
  5. 0005intro s
  6. 0006intro k
  7. 0007intro hr
  8. 0008intro hgap
  9. 0009intro heq
  10. 0010specialize lt_not_eq_add_middle r
  11. 0011specialize lt_not_eq_add_middle m
  12. 0012specialize lt_not_eq_add_middle (m * k)
  13. 0013specialize lt_not_eq_add_middle s
  14. 0014apply lt_not_eq_add_middle
  15. 0015exact hr
  16. 0016specialize add_left_cancel (m * q)
  17. 0017specialize add_left_cancel r
  18. 0018specialize add_left_cancel ((m * k + m) + s)
  19. 0019apply add_left_cancel
  20. 0020trans m * q2 + s
  21. 0021exact heq
  22. 0022rewrite <- hgap
  23. 0023specialize add_comm S k
  24. 0024specialize add_comm q
  25. 0025rewrite add_comm
  26. 0026specialize mul_add m
  27. 0027specialize mul_add q
  28. 0028specialize mul_add S k
  29. 0029rewrite mul_add
  30. 0030rewrite PA6
  31. 0031specialize add_assoc (m * q)
  32. 0032specialize add_assoc (m * k + m)
  33. 0033specialize add_assoc s
  34. 0034apply add_assoc