PA0031 — prime

Exact expanded PA statement

forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 0)

Structural proof guide

Generated structural guide

Every prime natural is nonzero.

Use the direct prerequisites mul_zero_left, succ_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (1), equality transport (1).

Referenced ingredients

PA000D mul_zero_left PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA000D mul_zero_left PA0005 succ_ne_zero

Direct dependents

PA003S prime_mod_cancel PA0061 prime_is_succ_succ PA0062 prime_mod_inverse PA0063 prime_bounded_nonzero_mod_inverse PA0072 gauss_half_range_signed_choices PA007B gauss_mixed_sign_scaled_source_impossible PA0084 gauss_signed_products_cancel_mod PA008B prime_mul_index_map_exists_up_to PA008L fermat_predecessor_exponent_mod_one PA008M quadratic_residue_half_power_mod_one PA008Q prime_scaled_inverse_exists PA00BN bounded_euler_criterion_dichotomy PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00C0 prime_scaled_half_division_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.