PA00D4

mod_two_zero_to_even

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

Congruence to zero modulo two supplies an even witness.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Congruence to zero modulo two supplies an even witness.

Use the direct prerequisites mod_eq_zero_to_dvd_nonzero as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA008A mod_eq_zero_to_dvd_nonzero

Proof neighborhood

Direct dependencies

PA008A mod_eq_zero_to_dvd_nonzero

Direct dependents

PA00D5 mod_two_zero_sum_to_congruent 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 hzero
  3. 0003specialize mod_eq_zero_to_dvd_nonzero 2
  4. 0004specialize mod_eq_zero_to_dvd_nonzero n
  5. 0005apply mod_eq_zero_to_dvd_nonzero
  6. 0006intro htwo
  7. 0007apply PA1
  8. 0008exact htwo
  9. 0009exact hzero