PD0028 — AllPrime

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.

Readable signature

AllPrime(b, c, l)

Exact expansion

forall dp_i. (exists dp_gap. dp_gap + S dp_i = l) -> exists dp_p. ((((exists ff_h_defined_all_prime_entry. ff_h_defined_all_prime_entry + S (dp_p) = S ((S (dp_i)) * c)) /\ exists ff_q_defined_all_prime_entry. b = ff_q_defined_all_prime_entry * S ((S (dp_i)) * c) + (dp_p))) /\ (~(dp_p = 1) /\ forall dp_a dp_d. dp_p = dp_a * dp_d -> dp_a = 1 \/ dp_d = 1))

This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

PD0002 Lt PD0004 Prime PD0013 BetaAt

Used by conservative definitions

none

All transitive conservative prerequisites

PD0002 Lt PD0004 Prime PD0013 BetaAt

Used by theorem statements or local proof propositions

TS002P beta_all_prime_entry_is_prime TS002V positive_number_with_admissible_prime_divisors_is_two_square TS0031 beta_sorted_prime_prefix_divisor_equals_bounded_last TS0032 even_valuation_sorted_terminal_prime_has_equal_predecessor

Grand-campaign planning vocabulary

Locate AllPrime in the global campaign vocabulary →

Reviewed AllPrime corresponds to blueprint AllPrime with checked argument positions [0, 1, 2].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.