BT003G · Bertrand theorem

prime_nonzero

Stable checked-use theorem · independently kernel verified

Every prime natural is nonzero.

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

∀ p. Prime(p) → ¬p = 0

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

PD0004 Prime

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 0)

Proof neighborhood

Direct theorem prerequisites

BT0004 mul_zero_left BT000C succ_ne_zero

Direct theorem dependents

BT003H prime_decidable BT00AW prime_is_succ_succ BT00PS bounded_prime_interval_search BT00QF prime_power_exponent_le BT00QN prime_power_successor_cancel_cofactor BT00S0 prime_power_quotient_prefix_exists BT00Y5 central_binom_prime_power_contribution_le_double BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00YE central_binom_prime_valuation_zero_two_thirds_range

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

20 script commands · 10 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 (2)
mul zero leftsucc ne zero
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro hp
  3. L3
    intro hp0
02Separate the logical casesL4–4

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

  1. L4
    cases hp
03Use earlier factsL5–6

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

  1. L5
    specialize hp_right 0
  2. L6
    specialize hp_right 0
04Establish hunitL7–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hp right.

  1. L7
    have hunit : 0 = 1 \/ 0 = 1
  2. L8
    apply hp_right
  3. L9
    rewrite hp0
  4. L10
    symm
  5. L11
    apply mul_zero_left
05Separate the logical casesL12–12

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

  1. L12
    cases hunit
06Use earlier factsL13–14

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

  1. L13
    specialize succ_ne_zero 0
  2. L14
    apply succ_ne_zero
07Calculate and transport equalitiesL15–15

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

  1. L15
    symm
08Use earlier factsL16–18

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

  1. L16
    exact hunit_left
  2. L17
    specialize succ_ne_zero 0
  3. L18
    apply succ_ne_zero
09Calculate and transport equalitiesL19–19

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

  1. L19
    symm
10Use earlier factsL20–20

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

  1. L20
    exact hunit_right

Library-wide reading audit

Original defined command ledger · 20 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003intro hp0
  4. 0004cases hp
  5. 0005specialize hp_right 0
  6. 0006specialize hp_right 0
  7. 0007have hunit : 0 = 1 \/ 0 = 1
  8. 0008apply hp_right
  9. 0009rewrite hp0
  10. 0010symm
  11. 0011apply mul_zero_left
  12. 0012cases hunit
  13. 0013specialize succ_ne_zero 0
  14. 0014apply succ_ne_zero
  15. 0015symm
  16. 0016exact hunit_left
  17. 0017specialize succ_ne_zero 0
  18. 0018apply succ_ne_zero
  19. 0019symm
  20. 0020exact hunit_right