BT001U · Bertrand theorem

division_remainder_unique

Stable checked-use theorem · independently kernel verified

Bounded quotient-remainder decompositions have unique quotients and remainders.

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. ∀ n. ∀ q. ∀ r. ∀ q2. ∀ r2. n = m · q + r → Lt(r,m) → n = m · q2 + r2 → Lt(r2,m) → q = q2 ∧ r = r2

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

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall m n q r q2 r2. n = m * q + r -> (exists k. k + S r = m) -> n = m * q2 + r2 -> (exists k. k + S r2 = m) -> q = q2 /\ r = r2

Proof neighborhood

Direct theorem prerequisites

BT0000 zero_add BT000K le_total BT000Q zero_or_succ BT000V add_left_cancel BT001S positive_quotient_gap_impossible

Direct theorem dependents

BT003B multiple_decidable_nonzero BT003W mod_eq_bounded_unique BT0042 beta_at_unique BT00S1 power_quotient_prefix_transport BT00SG division_remainder_successor_cases BT00SH division_successor_quotient_by_bit BT00SS prime_power_quotient_prefix_last_zero BT00XF division_zero_quotient_of_lt BT00XG division_double_quotient_bit 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

74 script commands · 33 reading checkpoints · 1 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)
zero addle totalzero or succadd left cancelpositive quotient gap impossible
01Fix variables and assumptionsL1–10

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro q2
  6. L6
    intro r2
  7. L7
    intro h1
  8. L8
    intro hr
  9. L9
    intro h2
  10. L10
    intro hr2
02Establish hsumL11–17

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

  1. L11
    have hsum : m * q + r = m * q2 + r2
  2. L12
    trans n
  3. L13
    symm
  4. L14
    exact h1
  5. L15
    exact h2
  6. L16
    specialize le_total q
  7. L17
    specialize le_total q2
03Separate the logical casesL18–19

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

  1. L18
    cases le_total
  2. L19
    cases le_total_left
04Use earlier factsL20–20

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

  1. L20
    specialize zero_or_succ x
05Separate the logical casesL21–21

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

  1. L21
    cases zero_or_succ
06Calculate and transport equalitiesL22–22

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

  1. L22
    rewrite zero_or_succ_left at le_total_left_witness
07Use earlier factsL23–23

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

  1. L23
    specialize zero_add q
08Calculate and transport equalitiesL24–24

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

  1. L24
    rewrite zero_add at le_total_left_witness
09Separate the logical casesL25–25

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

  1. L25
    split
10Use earlier factsL26–30

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

  1. L26
    exact le_total_left_witness
  2. L27
    specialize add_left_cancel (m * q)
  3. L28
    specialize add_left_cancel r
  4. L29
    specialize add_left_cancel r2
  5. L30
    apply add_left_cancel
11Calculate and transport equalitiesL31–31

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

  1. L31
    rewrite <- le_total_left_witness at hsum
12Use earlier factsL32–32

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

  1. L32
    exact hsum
13Separate the logical casesL33–34

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

  1. L33
    cases zero_or_succ_right
  2. L34
    exfalso
14Use earlier factsL35–42

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

  1. L35
    specialize positive_quotient_gap_impossible m
  2. L36
    specialize positive_quotient_gap_impossible q
  3. L37
    specialize positive_quotient_gap_impossible q2
  4. L38
    specialize positive_quotient_gap_impossible r
  5. L39
    specialize positive_quotient_gap_impossible r2
  6. L40
    specialize positive_quotient_gap_impossible x1
  7. L41
    apply positive_quotient_gap_impossible
  8. L42
    exact hr
15Calculate and transport equalitiesL43–43

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

  1. L43
    rewrite zero_or_succ_right_witness at le_total_left_witness
16Use earlier factsL44–45

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

  1. L44
    exact le_total_left_witness
  2. L45
    exact hsum
17Separate the logical casesL46–46

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

  1. L46
    cases le_total_right
18Use earlier factsL47–47

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

  1. L47
    specialize zero_or_succ x
19Separate the logical casesL48–48

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

  1. L48
    cases zero_or_succ
20Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite zero_or_succ_left at le_total_right_witness
21Use earlier factsL50–50

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

  1. L50
    specialize zero_add q2
22Calculate and transport equalitiesL51–51

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

  1. L51
    rewrite zero_add at le_total_right_witness
23Separate the logical casesL52–52

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

  1. L52
    split
24Calculate and transport equalitiesL53–53

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

  1. L53
    symm
25Use earlier factsL54–58

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

  1. L54
    exact le_total_right_witness
  2. L55
    specialize add_left_cancel (m * q)
  3. L56
    specialize add_left_cancel r
  4. L57
    specialize add_left_cancel r2
  5. L58
    apply add_left_cancel
26Calculate and transport equalitiesL59–59

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

  1. L59
    rewrite le_total_right_witness at hsum
27Use earlier factsL60–60

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

  1. L60
    exact hsum
28Separate the logical casesL61–62

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

  1. L61
    cases zero_or_succ_right
  2. L62
    exfalso
29Use earlier factsL63–70

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

  1. L63
    specialize positive_quotient_gap_impossible m
  2. L64
    specialize positive_quotient_gap_impossible q2
  3. L65
    specialize positive_quotient_gap_impossible q
  4. L66
    specialize positive_quotient_gap_impossible r2
  5. L67
    specialize positive_quotient_gap_impossible r
  6. L68
    specialize positive_quotient_gap_impossible x1
  7. L69
    apply positive_quotient_gap_impossible
  8. L70
    exact hr2
30Calculate and transport equalitiesL71–71

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

  1. L71
    rewrite zero_or_succ_right_witness at le_total_right_witness
31Use earlier factsL72–72

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

  1. L72
    exact le_total_right_witness
32Calculate and transport equalitiesL73–73

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

  1. L73
    symm
33Use earlier factsL74–74

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

  1. L74
    exact hsum

Library-wide reading audit

Original defined command ledger · 74 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro q2
  6. 0006intro r2
  7. 0007intro h1
  8. 0008intro hr
  9. 0009intro h2
  10. 0010intro hr2
  11. 0011have hsum : m * q + r = m * q2 + r2
  12. 0012trans n
  13. 0013symm
  14. 0014exact h1
  15. 0015exact h2
  16. 0016specialize le_total q
  17. 0017specialize le_total q2
  18. 0018cases le_total
  19. 0019cases le_total_left
  20. 0020specialize zero_or_succ x
  21. 0021cases zero_or_succ
  22. 0022rewrite zero_or_succ_left at le_total_left_witness
  23. 0023specialize zero_add q
  24. 0024rewrite zero_add at le_total_left_witness
  25. 0025split
  26. 0026exact le_total_left_witness
  27. 0027specialize add_left_cancel (m * q)
  28. 0028specialize add_left_cancel r
  29. 0029specialize add_left_cancel r2
  30. 0030apply add_left_cancel
  31. 0031rewrite <- le_total_left_witness at hsum
  32. 0032exact hsum
  33. 0033cases zero_or_succ_right
  34. 0034exfalso
  35. 0035specialize positive_quotient_gap_impossible m
  36. 0036specialize positive_quotient_gap_impossible q
  37. 0037specialize positive_quotient_gap_impossible q2
  38. 0038specialize positive_quotient_gap_impossible r
  39. 0039specialize positive_quotient_gap_impossible r2
  40. 0040specialize positive_quotient_gap_impossible x1
  41. 0041apply positive_quotient_gap_impossible
  42. 0042exact hr
  43. 0043rewrite zero_or_succ_right_witness at le_total_left_witness
  44. 0044exact le_total_left_witness
  45. 0045exact hsum
  46. 0046cases le_total_right
  47. 0047specialize zero_or_succ x
  48. 0048cases zero_or_succ
  49. 0049rewrite zero_or_succ_left at le_total_right_witness
  50. 0050specialize zero_add q2
  51. 0051rewrite zero_add at le_total_right_witness
  52. 0052split
  53. 0053symm
  54. 0054exact le_total_right_witness
  55. 0055specialize add_left_cancel (m * q)
  56. 0056specialize add_left_cancel r
  57. 0057specialize add_left_cancel r2
  58. 0058apply add_left_cancel
  59. 0059rewrite le_total_right_witness at hsum
  60. 0060exact hsum
  61. 0061cases zero_or_succ_right
  62. 0062exfalso
  63. 0063specialize positive_quotient_gap_impossible m
  64. 0064specialize positive_quotient_gap_impossible q2
  65. 0065specialize positive_quotient_gap_impossible q
  66. 0066specialize positive_quotient_gap_impossible r2
  67. 0067specialize positive_quotient_gap_impossible r
  68. 0068specialize positive_quotient_gap_impossible x1
  69. 0069apply positive_quotient_gap_impossible
  70. 0070exact hr2
  71. 0071rewrite zero_or_succ_right_witness at le_total_right_witness
  72. 0072exact le_total_right_witness
  73. 0073symm
  74. 0074exact hsum