BT0024 · Bertrand theorem

two_large_factors_impossible

Stable checked-use theorem · independently kernel verified

Two naturals at least two cannot multiply to two.

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. ~(2 = S (S a) * S (S 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. ~(2 = S (S a) * S (S b))

Proof neighborhood

Direct theorem prerequisites

BT0005 mul_succ_left BT001X add_eq_zero_left BT000M mul_eq_zero

Direct theorem dependents

BT0025 prime_two

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

28 script commands · 9 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 (3)
mul succ leftadd eq zero leftmul eq zero
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
02Use earlier factsL4–5

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

  1. L4
    specialize mul_succ_left (S a)
  2. L5
    specialize mul_succ_left (S (S b))
03Calculate and transport equalitiesL6–8

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

  1. L6
    rewrite mul_succ_left at h
  2. L7
    rewrite PA4 at h
  3. L8
    rewrite PA4 at h
04Establish hzeroL9–12

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

  1. L9
    have hzero : 0 = S a * S (S b) + b
  2. L10
    apply PA2
  3. L11
    apply PA2
  4. L12
    exact h
05Establish hzero'L13–15

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

  1. L13
    have hzero' : S a * S (S b) + b = 0
  2. L14
    symm
  3. L15
    exact hzero
06Establish hprodL16–20

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

  1. L16
    have hprod : S a * S (S b) = 0
  2. L17
    apply add_eq_zero_left
  3. L18
    exact hzero'
  4. L19
    specialize mul_eq_zero (S a)
  5. L20
    specialize mul_eq_zero (S (S b))
07Establish hzL21–23

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

  1. L21
    have hz : S a = 0 \/ S (S b) = 0
  2. L22
    apply mul_eq_zero
  3. L23
    exact hprod
08Separate the logical casesL24–24

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

  1. L24
    cases hz
09Use earlier factsL25–28

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

  1. L25
    apply PA1
  2. L26
    exact hz_left
  3. L27
    apply PA1
  4. L28
    exact hz_right

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004specialize mul_succ_left (S a)
  5. 0005specialize mul_succ_left (S (S b))
  6. 0006rewrite mul_succ_left at h
  7. 0007rewrite PA4 at h
  8. 0008rewrite PA4 at h
  9. 0009have hzero : 0 = S a * S (S b) + b
  10. 0010apply PA2
  11. 0011apply PA2
  12. 0012exact h
  13. 0013have hzero' : S a * S (S b) + b = 0
  14. 0014symm
  15. 0015exact hzero
  16. 0016have hprod : S a * S (S b) = 0
  17. 0017apply add_eq_zero_left
  18. 0018exact hzero'
  19. 0019specialize mul_eq_zero (S a)
  20. 0020specialize mul_eq_zero (S (S b))
  21. 0021have hz : S a = 0 \/ S (S b) = 0
  22. 0022apply mul_eq_zero
  23. 0023exact hprod
  24. 0024cases hz
  25. 0025apply PA1
  26. 0026exact hz_left
  27. 0027apply PA1
  28. 0028exact hz_right