BT003L

prime_divisor_exists

Stable · empty-context checked

Every nonzero nonunit natural has a prime divisor.

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 this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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