PA00CE — odd_sum_iff_opposite

Exact expanded PA statement

forall m n. (((exists psc_odd_odd_sum. m + n = 2 * psc_odd_odd_sum + 1) -> ((((exists psc_even_even_m. m = 2 * psc_even_even_m) /\ (exists psc_odd_odd_n. n = 2 * psc_odd_odd_n + 1)) \/ ((exists psc_odd_odd_m. m = 2 * psc_odd_odd_m + 1) /\ (exists psc_even_even_n. n = 2 * psc_even_even_n))))) /\ (((((exists psc_even_even_m. m = 2 * psc_even_even_m) /\ (exists psc_odd_odd_n. n = 2 * psc_odd_odd_n + 1)) \/ ((exists psc_odd_odd_m. m = 2 * psc_odd_odd_m + 1) /\ (exists psc_even_even_n. n = 2 * psc_even_even_n)))) -> (exists psc_odd_odd_sum. m + n = 2 * psc_odd_odd_sum + 1)))

Structural proof guide

Generated structural guide

A sum is odd exactly when its summands have opposite parity.

Use the direct prerequisites odd_sum_parity_cases, even_add_odd, odd_add_even as previously established PA formulas.

The proof proceeds by case analysis (3).

Referenced ingredients

PA00CD odd_sum_parity_cases PA006F even_add_odd PA006G odd_add_even

Proof neighborhood

Direct dependencies

PA00CD odd_sum_parity_cases PA006F even_add_odd PA006G odd_add_even

Direct dependents

PA00CF odd_division_odd_iff

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.