BT010E · Bertrand theorem

division_quotient_lower_of_scaled_le

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

A scaled lower bound forces the division quotient above its scale index.

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. ∀ s. DivRem(N,d,q,r) → Le(d · s,N) → Le(s,q)

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

PD0001 Le PD0007 DivRem

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

6 occurrences

Exact expanded native-PA statement
forall d N q r s. (((N) = (d) * (q) + (r) /\ (exists bcf_lt_gap_b5rbdqlosl_division_bound. bcf_lt_gap_b5rbdqlosl_division_bound + S (r) = d))) -> (exists bcf_le_gap_b5rbdqlosl_scaled. bcf_le_gap_b5rbdqlosl_scaled + (d * s) = N) -> (exists bcf_le_gap_b5rbdqlosl_result. bcf_le_gap_b5rbdqlosl_result + (s) = q)

Proof neighborhood

Direct theorem prerequisites

BT001R division_block_upper BT001G le_or_lt BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT001I lt_not_le

Direct theorem dependents

BT010F floor_sqrt_le_third_quotient

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

42 script commands · 11 reading checkpoints · 5 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)
division block upperle or ltmul le mul leftlt of lt of lelt not le
01Fix variables and assumptionsL1–7

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 s
  6. L6
    intro hdivision
  7. L7
    intro hscaled
02Separate the logical casesL8–8

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

  1. L8
    cases hdivision
03Establish hcasesL9–12

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hcases : Le(s,q) ∨ Lt(q,s)Definitions: Le(s,q)Lt(q,s)Original native command in the exact edition
  2. L10
    specialize le_or_lt s
  3. L11
    specialize le_or_lt q
  4. L12
    exact le_or_lt
04Separate the logical casesL13–13

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

  1. L13
    cases hcases
05Use earlier factsL14–14

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

  1. L14
    exact hcases_left
06Establish hupperL15–21

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

  1. L15
    have hupper : Lt(N,d · S q)Definitions: Lt(N,d · S q)Original native command in the exact edition
  2. L16
    rewrite hdivision_left
  3. L17
    specialize division_block_upper d
  4. L18
    specialize division_block_upper q
  5. L19
    specialize division_block_upper r
  6. L20
    apply division_block_upper
  7. L21
    exact hdivision_right
07Establish hreverseL22–23

Establish this local claim before using it. It is not an additional assumption.

  1. L22
    have hreverse : Lt(q,s)Definitions: Lt(q,s)Original native command in the exact edition
  2. L23
    exact hcases_right
08Establish hproductL24–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.

  1. L24
    have hproduct : Le(d · S q,d · s)Definitions: Le(d · S q,d · s)Original native command in the exact edition
  2. L25
    specialize mul_le_mul_left (S q)
  3. L26
    specialize mul_le_mul_left s
  4. L27
    specialize mul_le_mul_left d
  5. L28
    apply mul_le_mul_left
  6. L29
    exact hreverse
09Establish hstrictL30–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L30
    have hstrict : Lt(N,d · s)Definitions: Lt(N,d · s)Original native command in the exact edition
  2. L31
    specialize lt_of_lt_of_le N
  3. L32
    specialize lt_of_lt_of_le (d * S q)
  4. L33
    specialize lt_of_lt_of_le (d * s)
  5. L34
    apply lt_of_lt_of_le
  6. L35
    exact hupper
  7. L36
    exact hproduct
10Separate the logical casesL37–37

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

  1. L37
    exfalso
11Use earlier factsL38–42

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

  1. L38
    specialize lt_not_le N
  2. L39
    specialize lt_not_le (d * s)
  3. L40
    apply lt_not_le
  4. L41
    exact hstrict
  5. L42
    exact hscaled

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro d
  2. 0002intro N
  3. 0003intro q
  4. 0004intro r
  5. 0005intro s
  6. 0006intro hdivision
  7. 0007intro hscaled
  8. 0008cases hdivision
  9. 0009have hcases : Le(s,q) ∨ Lt(q,s)
    Exact native replay linehave hcases : (exists bcf_le_gap_b5rbdqlosl_result. bcf_le_gap_b5rbdqlosl_result + (s) = q) \/ (exists bcf_lt_gap_b5rbdqlosl_reverse. bcf_lt_gap_b5rbdqlosl_reverse + S (q) = s)
  10. 0010specialize le_or_lt s
  11. 0011specialize le_or_lt q
  12. 0012exact le_or_lt
  13. 0013cases hcases
  14. 0014exact hcases_left
  15. 0015have hupper : Lt(N,d · S q)
    Exact native replay linehave hupper : exists bcf_lt_gap_b5rbdqlosl_upper. bcf_lt_gap_b5rbdqlosl_upper + S (N) = d * S q
  16. 0016rewrite hdivision_left
  17. 0017specialize division_block_upper d
  18. 0018specialize division_block_upper q
  19. 0019specialize division_block_upper r
  20. 0020apply division_block_upper
  21. 0021exact hdivision_right
  22. 0022have hreverse : Lt(q,s)
    Exact native replay linehave hreverse : exists bcf_le_gap_b5rbdqlosl_reverse_le. bcf_le_gap_b5rbdqlosl_reverse_le + (S q) = s
  23. 0023exact hcases_right
  24. 0024have hproduct : Le(d · S q,d · s)
    Exact native replay linehave hproduct : exists bcf_le_gap_b5rbdqlosl_product_le. bcf_le_gap_b5rbdqlosl_product_le + (d * S q) = d * s
  25. 0025specialize mul_le_mul_left (S q)
  26. 0026specialize mul_le_mul_left s
  27. 0027specialize mul_le_mul_left d
  28. 0028apply mul_le_mul_left
  29. 0029exact hreverse
  30. 0030have hstrict : Lt(N,d · s)
    Exact native replay linehave hstrict : exists bcf_lt_gap_b5rbdqlosl_contradiction. bcf_lt_gap_b5rbdqlosl_contradiction + S (N) = d * s
  31. 0031specialize lt_of_lt_of_le N
  32. 0032specialize lt_of_lt_of_le (d * S q)
  33. 0033specialize lt_of_lt_of_le (d * s)
  34. 0034apply lt_of_lt_of_le
  35. 0035exact hupper
  36. 0036exact hproduct
  37. 0037exfalso
  38. 0038specialize lt_not_le N
  39. 0039specialize lt_not_le (d * s)
  40. 0040apply lt_not_le
  41. 0041exact hstrict
  42. 0042exact hscaled