PA000U

beta_modulus_nonzero

Stable checked-use theorem · independently closed

Every Gödel-beta decoding modulus is nonzero.

Exact expanded PA statement

forall c i. ~(S ((S i) * c) = 0)

Structural proof guide

Generated structural guide

Every Gödel-beta decoding modulus is nonzero.

Use the direct prerequisites succ_ne_zero as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0005 succ_ne_zero

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA0029 beta_at_exists PA002G beta_exclusive_recode_congruence_step PA002W beta_at_of_mod_eq_bound PA002X beta_prefix_extend

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.

  1. 0001intro c
  2. 0002intro i
  3. 0003specialize succ_ne_zero ((S i) * c)
  4. 0004exact succ_ne_zero