PA00CH

even_to_mod_two_zero

Alpha v16 checked-use theorem · independently closed; not Stable

Every even natural is congruent to zero modulo two.

Exact expanded PA statement

forall n. (exists pmt_even_n. n = 2 * pmt_even_n) -> (exists pmt_u_n_zero pmt_v_n_zero. n + 2 * pmt_u_n_zero = 0 + 2 * pmt_v_n_zero)

Structural proof guide

Generated structural guide

Every even natural is congruent to zero modulo two.

Use the direct prerequisites dvd_to_mod_zero as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0021 dvd_to_mod_zero

Proof neighborhood

Direct dependencies

PA0021 dvd_to_mod_zero

Direct dependents

PA00CJ matching_parity_mod_two PA00FL mod_two_preserves_parity

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro heven
  3. 0003specialize dvd_to_mod_zero 2
  4. 0004specialize dvd_to_mod_zero n
  5. 0005apply dvd_to_mod_zero
  6. 0006exact heven