BT003A · Bertrand theorem

eq_decidable

Stable checked-use theorem · independently kernel verified

Equality of natural numbers is constructively decidable.

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

forall a b. a = b \/ ~(a = b)

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

none

0 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b. a = b \/ ~(a = b)

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

BT003B multiple_decidable_nonzero BT003C multiple_decidable BT003E factor_search_up_to BT003H prime_decidable BT00YM no_bertrand_central_prime_contribution_ranges BT0103 prime_contribution_cofactor_eq_one

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

27 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.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro a
02Induction on aL2–3

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction a
  2. L3
    intro b
03Induction on bL4–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction b
04Separate the logical casesL5–5

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

  1. L5
    left
05Calculate and transport equalitiesL6–6

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

  1. L6
    refl
06Separate the logical casesL7–7

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

  1. L7
    right
07Fix variables and assumptionsL8–8

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

  1. L8
    intro h
08Use earlier factsL9–9

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

  1. L9
    apply PA1
09Calculate and transport equalitiesL10–10

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

  1. L10
    symm
10Use earlier factsL11–11

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

  1. L11
    exact h
11Fix variables and assumptionsL12–12

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

  1. L12
    intro b
12Induction on bL13–13

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L13
    induction b
13Separate the logical casesL14–14

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

  1. L14
    right
14Fix variables and assumptionsL15–15

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

  1. L15
    intro h
15Use earlier factsL16–18

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

  1. L16
    apply PA1
  2. L17
    exact h
  3. L18
    specialize IH b
16Separate the logical casesL19–20

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

  1. L19
    cases IH
  2. L20
    left
17Calculate and transport equalitiesL21–21

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

  1. L21
    congr
18Use earlier factsL22–22

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

  1. L22
    exact IH_left
19Separate the logical casesL23–23

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

  1. L23
    right
20Fix variables and assumptionsL24–24

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

  1. L24
    intro h
21Use earlier factsL25–27

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

  1. L25
    apply IH_right
  2. L26
    apply PA2
  3. L27
    exact h

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro a
  2. 0002induction a
  3. 0003intro b
  4. 0004induction b
  5. 0005left
  6. 0006refl
  7. 0007right
  8. 0008intro h
  9. 0009apply PA1
  10. 0010symm
  11. 0011exact h
  12. 0012intro b
  13. 0013induction b
  14. 0014right
  15. 0015intro h
  16. 0016apply PA1
  17. 0017exact h
  18. 0018specialize IH b
  19. 0019cases IH
  20. 0020left
  21. 0021congr
  22. 0022exact IH_left
  23. 0023right
  24. 0024intro h
  25. 0025apply IH_right
  26. 0026apply PA2
  27. 0027exact h