BT003X · Bertrand theorem

mod_eq_to_remainder_decomposition

Stable checked-use theorem · independently kernel verified

A bounded balanced residue has a directed quotient/remainder witness.

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. ∀ b. ∀ x. ¬m = 0 → Lt(x,m) → ModEq(m,b,x) → ∃ y. b = y · m + x

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 PD0008 ModEq

2 occurrences

In local proof propositions

PD0007 DivRem PD0008 ModEq

3 occurrences

Exact expanded native-PA statement
forall m b x. ~(m = 0) -> (exists h. h + S x = m) -> (exists u v. b + m * u = x + m * v) -> exists q. b = q * m + x

Proof neighborhood

Direct theorem prerequisites

BT001P division_remainder_exists BT0002 add_comm BT0006 mul_comm BT003Q mod_eq_trans BT003W mod_eq_bounded_unique

Direct theorem dependents

BT0045 beta_at_of_mod_eq_bound

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

51 script commands · 20 reading checkpoints · 4 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 remainder existsadd commmul commmod eq transmod eq bounded unique
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro b
  3. L3
    intro x
  4. L4
    intro hm
  5. L5
    intro hx
  6. L6
    intro hbx
02Establish hdivL7–11

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

  1. L7
    have hdiv : ∃ q. ∃ r. DivRem(b,m,q,r)Definitions: DivRem(b,m,q,r)Original native command in the exact edition
  2. L8
    specialize division_remainder_exists m
  3. L9
    specialize division_remainder_exists b
  4. L10
    apply division_remainder_exists
  5. L11
    exact hm
03Separate the logical casesL12–14

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

  1. L12
    cases hdiv
  2. L13
    cases hdiv_witness
  3. L14
    cases hdiv_witness_witness
04Establish hrembL15–15

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

  1. L15
    have hremb : ModEq(m,x2,b)Definitions: ModEq(m,x2,b)Original native command in the exact edition
05Construct an explicit witnessL16–17

Supply the displayed value, then prove that it has the required property.

  1. L16
    exists x1
  2. L17
    exists 0
06Calculate and transport equalitiesL18–18

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

  1. L18
    trans m * x1 + x2
07Use earlier factsL19–19

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

  1. L19
    apply add_comm
08Calculate and transport equalitiesL20–21

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

  1. L20
    trans b
  2. L21
    symm
09Use earlier factsL22–22

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

  1. L22
    exact hdiv_witness_witness_left
10Calculate and transport equalitiesL23–24

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

  1. L23
    symm
  2. L24
    rewrite PA5
11Use earlier factsL25–25

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

  1. L25
    apply PA3
12Establish hremxL26–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L26
    have hremx : ModEq(m,x2,x)Definitions: ModEq(m,x2,x)Original native command in the exact edition
  2. L27
    specialize mod_eq_trans m
  3. L28
    specialize mod_eq_trans x2
  4. L29
    specialize mod_eq_trans b
  5. L30
    specialize mod_eq_trans x
  6. L31
    apply mod_eq_trans
  7. L32
    exact hremb
  8. L33
    exact hbx
13Establish hrxL34–41

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

  1. L34
    have hrx : x2 = x
  2. L35
    specialize mod_eq_bounded_unique m
  3. L36
    specialize mod_eq_bounded_unique x2
  4. L37
    specialize mod_eq_bounded_unique x
  5. L38
    apply mod_eq_bounded_unique
  6. L39
    exact hdiv_witness_witness_right
  7. L40
    exact hx
  8. L41
    exact hremx
14Construct an explicit witnessL42–42

Supply the displayed value, then prove that it has the required property.

  1. L42
    exists x1
15Calculate and transport equalitiesL43–43

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

  1. L43
    trans m * x1 + x2
16Use earlier factsL44–44

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

  1. L44
    exact hdiv_witness_witness_left
17Calculate and transport equalitiesL45–46

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

  1. L45
    trans x1 * m + x2
  2. L46
    congr
18Use earlier factsL47–47

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

  1. L47
    apply mul_comm
19Calculate and transport equalitiesL48–50

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

  1. L48
    refl
  2. L49
    congr
  3. L50
    refl
20Use earlier factsL51–51

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

  1. L51
    exact hrx

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro m
  2. 0002intro b
  3. 0003intro x
  4. 0004intro hm
  5. 0005intro hx
  6. 0006intro hbx
  7. 0007have hdiv : ∃ q. ∃ r. DivRem(b,m,q,r)
    Exact native replay linehave hdiv : exists q r. b = m * q + r /\ exists h. h + S r = m
  8. 0008specialize division_remainder_exists m
  9. 0009specialize division_remainder_exists b
  10. 0010apply division_remainder_exists
  11. 0011exact hm
  12. 0012cases hdiv
  13. 0013cases hdiv_witness
  14. 0014cases hdiv_witness_witness
  15. 0015have hremb : ModEq(m,x2,b)
    Exact native replay linehave hremb : exists u v. x2 + m * u = b + m * v
  16. 0016exists x1
  17. 0017exists 0
  18. 0018trans m * x1 + x2
  19. 0019apply add_comm
  20. 0020trans b
  21. 0021symm
  22. 0022exact hdiv_witness_witness_left
  23. 0023symm
  24. 0024rewrite PA5
  25. 0025apply PA3
  26. 0026have hremx : ModEq(m,x2,x)
    Exact native replay linehave hremx : exists u v. x2 + m * u = x + m * v
  27. 0027specialize mod_eq_trans m
  28. 0028specialize mod_eq_trans x2
  29. 0029specialize mod_eq_trans b
  30. 0030specialize mod_eq_trans x
  31. 0031apply mod_eq_trans
  32. 0032exact hremb
  33. 0033exact hbx
  34. 0034have hrx : x2 = x
  35. 0035specialize mod_eq_bounded_unique m
  36. 0036specialize mod_eq_bounded_unique x2
  37. 0037specialize mod_eq_bounded_unique x
  38. 0038apply mod_eq_bounded_unique
  39. 0039exact hdiv_witness_witness_right
  40. 0040exact hx
  41. 0041exact hremx
  42. 0042exists x1
  43. 0043trans m * x1 + x2
  44. 0044exact hdiv_witness_witness_left
  45. 0045trans x1 * m + x2
  46. 0046congr
  47. 0047apply mul_comm
  48. 0048refl
  49. 0049congr
  50. 0050refl
  51. 0051exact hrx