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)Squarefree(n)AllPrime(b,c,l)

Checked theorems using this definition

MC0002 · prime_toggle_fresh_divisor_productMC0007 · prime_factor_toggle_preserves_divisorMC0008 · divisor_prime_toggle_existsMC0009 · divisor_prime_toggle_functionalMC000A · divisor_prime_toggle_symmetricMC000B · divisor_prime_toggle_boundedMC000C · divisor_prime_toggle_prefix_existsMC000E · divisor_prime_toggle_prefix_permutationMC000F · divisor_prime_toggle_permutation_existsMC0010 · mobius_prime_factor_toggle_negatesMC0012 · mobius_divisor_mask_prime_toggle_negatesMC0016 · mobius_divisor_mask_prime_factor_sum_zeroMC0017 · mobius_divisor_sum_nonunit_value_zero