PD0004

Prime(p)

p is nonunit and every factorization of p has a unit factor.

Conservative notation; not a theorem, primitive, or axiom.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Definition in prerequisite notation

¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

HasPrimeSquareDivisor(n)AllPrime(b,c,l)Squarefree(n)

Checked theorems using this definition

MV0007 · mobius_from_prime_squareMV000F · mobius_prime_squarefreeMV0010 · mobius_squarefree_fresh_prime_productMV0011 · mobius_prime_factor_list_appendMV0014 · mobius_prime_square_value_zeroMV0015 · mobius_fresh_prime_negates