PA00CE · theorem

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.

Statement with defined notation

∀ m. ∀ n. (Odd(m + n) → Even(m) ∧ Odd(n) ∨ Odd(m) ∧ Even(n)) ∧ (Even(m) ∧ Odd(n) ∨ Odd(m) ∧ Even(n) → Odd(m + n))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0009 Even PD0010 Odd

10 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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)))

Proof neighborhood

Direct theorem prerequisites

PA00CD odd_sum_parity_cases PA006F even_add_odd PA006G odd_add_even

Direct theorem dependents

PA00CF odd_division_odd_iff

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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