BT00XF · Bertrand theorem

division_zero_quotient_of_lt

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A dividend below its divisor has quotient zero.

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. ∀ n. ∀ q. ∀ r. DivRem(n,d,q,r) → Lt(n,d) → q = 0

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 PD0007 DivRem

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall d n q r. (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_bdzq_source_bound. bcf_lt_gap_bdzq_source_bound + S (r) = d))) -> (exists bcf_lt_gap_bdzq_bound. bcf_lt_gap_bdzq_bound + S (n) = d) -> q = 0

Proof neighborhood

Direct theorem prerequisites

BT0000 zero_add BT001U division_remainder_unique

Direct theorem dependents

BT00XO prime_power_quotient_zero_of_exponent_gt BT00YC double_quotient_carry_prefix_entries_zero

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

26 script commands · 7 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 (2)
zero adddivision remainder unique
01Fix variables and assumptionsL1–6

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro hdivision
  6. L6
    intro hbound
02Separate the logical casesL7–7

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

  1. L7
    cases hdivision
03Establish hzeroL8–12

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

  1. L8
    have hzero : n = d * 0 + n
  2. L9
    rewrite PA5
  3. L10
    symm
  4. L11
    specialize zero_add n
  5. L12
    apply zero_add
04Establish huniqueL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder unique.

  1. L13
    have hunique : q = 0 /\ r = n
  2. L14
    specialize division_remainder_unique d
  3. L15
    specialize division_remainder_unique n
  4. L16
    specialize division_remainder_unique q
  5. L17
    specialize division_remainder_unique r
  6. L18
    specialize division_remainder_unique 0
  7. L19
    specialize division_remainder_unique n
  8. L20
    apply division_remainder_unique
  9. L21
    exact hdivision_left
  10. L22
    exact hdivision_right
05Use earlier factsL23–24

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

  1. L23
    exact hzero
  2. L24
    exact hbound
06Separate the logical casesL25–25

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

  1. L25
    cases hunique
07Use earlier factsL26–26

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

  1. L26
    exact hunique_left

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hdivision
  6. 0006intro hbound
  7. 0007cases hdivision
  8. 0008have hzero : n = d * 0 + n
  9. 0009rewrite PA5
  10. 0010symm
  11. 0011specialize zero_add n
  12. 0012apply zero_add
  13. 0013have hunique : q = 0 /\ r = n
  14. 0014specialize division_remainder_unique d
  15. 0015specialize division_remainder_unique n
  16. 0016specialize division_remainder_unique q
  17. 0017specialize division_remainder_unique r
  18. 0018specialize division_remainder_unique 0
  19. 0019specialize division_remainder_unique n
  20. 0020apply division_remainder_unique
  21. 0021exact hdivision_left
  22. 0022exact hdivision_right
  23. 0023exact hzero
  24. 0024exact hbound
  25. 0025cases hunique
  26. 0026exact hunique_left