PA00CE

odd_sum_iff_opposite_parity

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

A sum is odd exactly when its summands have opposite 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_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-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)
odd sum parity caseseven add oddodd add even
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 odd_sum_parity_cases m
  2. L6
    specialize odd_sum_parity_cases n
  3. L7
    apply odd_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 hopposite
06Separate the logical casesL10–11

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

  1. L10
    cases hopposite
  2. L11
    cases hopposite_left
07Use earlier factsL12–16

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

  1. L12
    specialize even_add_odd m
  2. L13
    specialize even_add_odd n
  3. L14
    apply even_add_odd
  4. L15
    exact hopposite_left_left
  5. L16
    exact hopposite_left_right
08Separate the logical casesL17–17

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

  1. L17
    cases hopposite_right
09Use earlier factsL18–22

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

  1. L18
    specialize odd_add_even m
  2. L19
    specialize odd_add_even n
  3. L20
    apply odd_add_even
  4. L21
    exact hopposite_right_left
  5. L22
    exact hopposite_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 odd_sum_parity_cases m
  6. 0006specialize odd_sum_parity_cases n
  7. 0007apply odd_sum_parity_cases
  8. 0008exact hsum
  9. 0009intro hopposite
  10. 0010cases hopposite
  11. 0011cases hopposite_left
  12. 0012specialize even_add_odd m
  13. 0013specialize even_add_odd n
  14. 0014apply even_add_odd
  15. 0015exact hopposite_left_left
  16. 0016exact hopposite_left_right
  17. 0017cases hopposite_right
  18. 0018specialize odd_add_even m
  19. 0019specialize odd_add_even n
  20. 0020apply odd_add_even
  21. 0021exact hopposite_right_left
  22. 0022exact hopposite_right_right