BT003Q · Bertrand theorem

mod_eq_trans

Stable checked-use theorem · independently kernel verified

Balanced natural congruence is transitive.

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. ∀ a. ∀ b. ∀ c. ModEq(m,a,b) → ModEq(m,b,c) → ModEq(m,a,c)

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

PD0008 ModEq

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall m a b c. (exists u v. a + m * u = b + m * v) -> (exists r s. b + m * r = c + m * s) -> exists x y. a + m * x = c + m * y

Proof neighborhood

Direct theorem prerequisites

BT0003 add_assoc BT0002 add_comm BT0007 mul_add

Direct theorem dependents

BT003X mod_eq_to_remainder_decomposition BT004F binary_crt BT004U binary_crt_fold_step

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 · 21 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 (3)
add assocadd commmul add
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hab
  6. L6
    intro hbc
02Separate the logical casesL7–10

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

  1. L7
    cases hab
  2. L8
    cases hab_witness
  3. L9
    cases hbc
  4. L10
    cases hbc_witness
03Construct an explicit witnessL11–12

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

  1. L11
    exists x + x2
  2. L12
    exists x3 + x1
04Calculate and transport equalitiesL13–15

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

  1. L13
    trans a + (m * x + m * x2)
  2. L14
    congr
  3. L15
    refl
05Use earlier factsL16–16

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

  1. L16
    apply mul_add
06Calculate and transport equalitiesL17–18

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

  1. L17
    trans (a + m * x) + m * x2
  2. L18
    symm
07Use earlier factsL19–19

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

  1. L19
    apply add_assoc
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 + m * x1) + m * x2
  2. L21
    congr
09Use earlier factsL22–22

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

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

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

  1. L23
    refl
  2. L24
    trans b + (m * x1 + m * x2)
11Use earlier factsL25–25

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

  1. L25
    apply add_assoc
12Calculate and transport equalitiesL26–28

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

  1. L26
    trans b + (m * x2 + m * x1)
  2. L27
    congr
  3. L28
    refl
13Use earlier factsL29–29

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

  1. L29
    apply add_comm
14Calculate and transport equalitiesL30–31

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

  1. L30
    trans (b + m * x2) + m * x1
  2. L31
    symm
15Use earlier factsL32–32

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

  1. L32
    apply add_assoc
16Calculate and transport equalitiesL33–34

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

  1. L33
    trans (c + m * x3) + m * x1
  2. L34
    congr
17Use earlier factsL35–35

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

  1. L35
    exact hbc_witness_witness
18Calculate and transport equalitiesL36–37

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

  1. L36
    refl
  2. L37
    trans c + (m * x3 + m * x1)
19Use earlier factsL38–38

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

  1. L38
    apply add_assoc
20Calculate and transport equalitiesL39–41

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

  1. L39
    congr
  2. L40
    refl
  3. L41
    symm
21Use earlier factsL42–42

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

  1. L42
    apply mul_add

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hab
  6. 0006intro hbc
  7. 0007cases hab
  8. 0008cases hab_witness
  9. 0009cases hbc
  10. 0010cases hbc_witness
  11. 0011exists x + x2
  12. 0012exists x3 + x1
  13. 0013trans a + (m * x + m * x2)
  14. 0014congr
  15. 0015refl
  16. 0016apply mul_add
  17. 0017trans (a + m * x) + m * x2
  18. 0018symm
  19. 0019apply add_assoc
  20. 0020trans (b + m * x1) + m * x2
  21. 0021congr
  22. 0022exact hab_witness_witness
  23. 0023refl
  24. 0024trans b + (m * x1 + m * x2)
  25. 0025apply add_assoc
  26. 0026trans b + (m * x2 + m * x1)
  27. 0027congr
  28. 0028refl
  29. 0029apply add_comm
  30. 0030trans (b + m * x2) + m * x1
  31. 0031symm
  32. 0032apply add_assoc
  33. 0033trans (c + m * x3) + m * x1
  34. 0034congr
  35. 0035exact hbc_witness_witness
  36. 0036refl
  37. 0037trans c + (m * x3 + m * x1)
  38. 0038apply add_assoc
  39. 0039congr
  40. 0040refl
  41. 0041symm
  42. 0042apply mul_add