Exact expanded PA statement
forall m n. (((exists psc_even_even_sum. m + n = 2 * psc_even_even_sum) -> ((((exists psc_even_even_m. m = 2 * psc_even_even_m) /\ (exists psc_even_even_n. n = 2 * psc_even_even_n)) \/ ((exists psc_odd_odd_m. m = 2 * psc_odd_odd_m + 1) /\ (exists psc_odd_odd_n. n = 2 * psc_odd_odd_n + 1))))) /\ (((((exists psc_even_even_m. m = 2 * psc_even_even_m) /\ (exists psc_even_even_n. n = 2 * psc_even_even_n)) \/ ((exists psc_odd_odd_m. m = 2 * psc_odd_odd_m + 1) /\ (exists psc_odd_odd_n. n = 2 * psc_odd_odd_n + 1)))) -> (exists psc_even_even_sum. m + n = 2 * psc_even_even_sum)))Structural proof guide
Generated structural guide
A sum is even exactly when its summands have the same parity.
Use the direct prerequisites even_sum_parity_cases, even_add_even, odd_add_odd as previously established PA formulas.
The proof proceeds by case analysis (3).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
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.
- 0001
intro m - 0002
intro n - 0003
split - 0004
intro hsum - 0005
specialize even_sum_parity_cases m - 0006
specialize even_sum_parity_cases n - 0007
apply even_sum_parity_cases - 0008
exact hsum - 0009
intro hsame - 0010
cases hsame - 0011
cases hsame_left - 0012
specialize even_add_even m - 0013
specialize even_add_even n - 0014
apply even_add_even - 0015
exact hsame_left_left - 0016
exact hsame_left_right - 0017
cases hsame_right - 0018
specialize odd_add_odd m - 0019
specialize odd_add_odd n - 0020
apply odd_add_odd - 0021
exact hsame_right_left - 0022
exact hsame_right_right