BT003L

prime_divisor_exists

Stable checked-use theorem · independently kernel verified

Every nonzero nonunit natural has a prime divisor.

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.

Exact expanded PA statement

forall n. ~(n = 0) -> ~(n = 1) -> exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists k. n = p * k)

Structural proof guide

Every nonzero nonunit natural has a prime divisor.

Direct prerequisites: le_refl, prime_divisor_exists_up_to. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT000E le_refl BT003K prime_divisor_exists_up_to

Direct dependents

BT0103 prime_contribution_cofactor_eq_one BT0118 nonprime_has_small_prime_divisor_below_square

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

9 script commands · 2 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.

Named ingredients (2)
le reflprime divisor exists up to
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro hn0
  3. L3
    intro hn1
02Use earlier factsL4–9

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

  1. L4
    specialize prime_divisor_exists_up_to n
  2. L5
    specialize prime_divisor_exists_up_to n
  3. L6
    apply prime_divisor_exists_up_to
  4. L7
    apply le_refl
  5. L8
    exact hn0
  6. L9
    exact hn1

Library-wide reading audit

Original exact command ledger · 9 lines
  1. 0001intro n
  2. 0002intro hn0
  3. 0003intro hn1
  4. 0004specialize prime_divisor_exists_up_to n
  5. 0005specialize prime_divisor_exists_up_to n
  6. 0006apply prime_divisor_exists_up_to
  7. 0007apply le_refl
  8. 0008exact hn0
  9. 0009exact hn1