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

PrimeExponentEntries(n,pb,pc,eb,ec,vb,vc,l)PrimeDivisorSupport(n,pb,pc,l)AllPrime(b,c,l)

Checked theorems using this definition

PV0002 · prime_valuation_zero_of_nondivisorPV0003 · prime_valuation_nondivisor_of_zeroPV0004 · prime_power_valuation_pow_valuePV0005 · prime_power_valuation_powPV0007 · prime_valuation_distinct_prime_power_zeroPV0008 · prime_divisor_of_prime_powerPV0009 · prime_valuation_product_zero_leftPV000A · prime_valuation_strip_other_primePV000B · prime_exponent_entries_prime_dividesPV000C · prime_exponent_entries_restore_prime_powerPV000D · prime_exponent_entries_recodePV000E · prime_exponent_entries_appendPV0011 · prime_valuation_strict_cofactor_existsPV0012 · prime_valuation_support_append_full_powerPV0013 · prime_valuation_support_bounded_exists