PA00CB

even_sum_iff_same_parity

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

A sum is even exactly when its summands have the same parity.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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

PA00CA even_sum_parity_cases PA006H even_add_even PA006I odd_add_odd

Proof neighborhood

Direct dependencies

PA00CA even_sum_parity_cases PA006H even_add_even PA006I odd_add_odd

Direct dependents

PA00CC odd_division_even_iff

Formal native tactic body

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

Read the argument

Proof checkpoints

22 script commands · 9 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
even sum parity caseseven add evenodd add odd
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro m
  2. L2
    intro n
02Separate the logical casesL3–3

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L3
    split
03Fix variables and assumptionsL4–4

Work with arbitrary variables or the premises of the current implication.

  1. L4
    intro hsum
04Use earlier factsL5–8

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L5
    specialize even_sum_parity_cases m
  2. L6
    specialize even_sum_parity_cases n
  3. L7
    apply even_sum_parity_cases
  4. L8
    exact hsum
05Fix variables and assumptionsL9–9

Work with arbitrary variables or the premises of the current implication.

  1. L9
    intro hsame
06Separate the logical casesL10–11

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    cases hsame
  2. L11
    cases hsame_left
07Use earlier factsL12–16

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L12
    specialize even_add_even m
  2. L13
    specialize even_add_even n
  3. L14
    apply even_add_even
  4. L15
    exact hsame_left_left
  5. L16
    exact hsame_left_right
08Separate the logical casesL17–17

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L17
    cases hsame_right
09Use earlier factsL18–22

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L18
    specialize odd_add_odd m
  2. L19
    specialize odd_add_odd n
  3. L20
    apply odd_add_odd
  4. L21
    exact hsame_right_left
  5. L22
    exact hsame_right_right

Library-wide reading audit

Original exact command ledger · 22 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003split
  4. 0004intro hsum
  5. 0005specialize even_sum_parity_cases m
  6. 0006specialize even_sum_parity_cases n
  7. 0007apply even_sum_parity_cases
  8. 0008exact hsum
  9. 0009intro hsame
  10. 0010cases hsame
  11. 0011cases hsame_left
  12. 0012specialize even_add_even m
  13. 0013specialize even_add_even n
  14. 0014apply even_add_even
  15. 0015exact hsame_left_left
  16. 0016exact hsame_left_right
  17. 0017cases hsame_right
  18. 0018specialize odd_add_odd m
  19. 0019specialize odd_add_odd n
  20. 0020apply odd_add_odd
  21. 0021exact hsame_right_left
  22. 0022exact hsame_right_right