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. Exact original first-admission records.

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

PrimeBitPrefix(b,c,l)Primorial(n,z)

Checked theorems using this definition

PC0001 · prime_bit_choice_existsPC0004 · prime_bit_prefix_entryPC0005 · prime_bit_prefix_extendPC0006 · prime_bit_prefix_existsPC0007 · prime_bit_prefix_all_bitsPC000B · prime_count_positive_above_onePC001A · primorial_prefix_decoded_choicePC001B · primorial_factor_choice_one_lePC001C · prime_contribution_prefix_decoded_choicePC001D · central_binom_prime_mask_weighted_upperPC001E · primorial_cutoff_weighted_lowerPC001F · central_binom_prime_count_power_boundPC0032 · prime_bit_choice_functionalPC0036 · prime_count_one