BT0116 · Bertrand theorem

fixed_nontrivial_factor_not_prime

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A displayed nontrivial factorization refutes primality.

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

∀ n. ∀ a. ∀ b. n = a · b → ¬a = 1 → ¬b = 1 → ¬Prime(n)

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 n a b. n = a * b -> ~(a = 1) -> ~(b = 1) -> ((~(n = 1) /\ forall bpr_left_bb8fnfp_prime bpr_right_bb8fnfp_prime. n = bpr_left_bb8fnfp_prime * bpr_right_bb8fnfp_prime -> bpr_left_bb8fnfp_prime = 1 \/ bpr_right_bb8fnfp_prime = 1)) -> false

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

BT011A prime_le_twenty_two_cases BT0126 bertrand_upper_endpoint_factorization

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

18 script commands · 6 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.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro hfactor
  5. L5
    intro ha
  6. L6
    intro hb
  7. L7
    intro hprime
02Separate the logical casesL8–8

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

  1. L8
    cases hprime
03Use earlier factsL9–10

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

  1. L9
    specialize hprime_right a
  2. L10
    specialize hprime_right b
04Establish hunitL11–13

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

  1. L11
    have hunit : a = 1 \/ b = 1
  2. L12
    apply hprime_right
  3. L13
    exact hfactor
05Separate the logical casesL14–14

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

  1. L14
    cases hunit
06Use earlier factsL15–18

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

  1. L15
    apply ha
  2. L16
    exact hunit_left
  3. L17
    apply hb
  4. L18
    exact hunit_right

Library-wide reading audit

Original defined command ledger · 18 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hfactor
  5. 0005intro ha
  6. 0006intro hb
  7. 0007intro hprime
  8. 0008cases hprime
  9. 0009specialize hprime_right a
  10. 0010specialize hprime_right b
  11. 0011have hunit : a = 1 \/ b = 1
  12. 0012apply hprime_right
  13. 0013exact hfactor
  14. 0014cases hunit
  15. 0015apply ha
  16. 0016exact hunit_left
  17. 0017apply hb
  18. 0018exact hunit_right