PA00CD

odd_sum_parity_cases

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

An odd sum has summands of opposite parity.

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

Structural proof guide

Generated structural guide

An odd sum has summands of opposite parity.

Use the direct prerequisites parity_cases, even_add_even, odd_add_odd, odd_not_even as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (4).

Referenced ingredients

PA0057 parity_cases PA006H even_add_even PA006I odd_add_odd PA0056 odd_not_even

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA006H even_add_even PA006I odd_add_odd PA0056 odd_not_even

Direct dependents

PA00CE odd_sum_iff_opposite_parity PA00FS qres_opposite_status_from_odd_count_sum

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.

  1. 0001intro m
  2. 0002intro n
  3. 0003intro hsum
  4. 0004have hm : exists a. m = 2 * a \/ m = 2 * a + 1
  5. 0005specialize parity_cases m
  6. 0006exact parity_cases
  7. 0007have hn : exists b. n = 2 * b \/ n = 2 * b + 1
  8. 0008specialize parity_cases n
  9. 0009exact parity_cases
  10. 0010cases hm
  11. 0011cases hn
  12. 0012cases hm_witness
  13. 0013cases hn_witness
  14. 0014exfalso
  15. 0015have heven : exists c. m + n = 2 * c
  16. 0016specialize even_add_even m
  17. 0017specialize even_add_even n
  18. 0018apply even_add_even
  19. 0019exists x
  20. 0020exact hm_witness_left
  21. 0021exists x1
  22. 0022exact hn_witness_left
  23. 0023specialize odd_not_even (m + n)
  24. 0024apply odd_not_even
  25. 0025exact hsum
  26. 0026exact heven
  27. 0027left
  28. 0028split
  29. 0029exists x
  30. 0030exact hm_witness_left
  31. 0031exists x1
  32. 0032exact hn_witness_right
  33. 0033cases hn_witness
  34. 0034right
  35. 0035split
  36. 0036exists x
  37. 0037exact hm_witness_right
  38. 0038exists x1
  39. 0039exact hn_witness_left
  40. 0040exfalso
  41. 0041have heven : exists c. m + n = 2 * c
  42. 0042specialize odd_add_odd m
  43. 0043specialize odd_add_odd n
  44. 0044apply odd_add_odd
  45. 0045exists x
  46. 0046exact hm_witness_right
  47. 0047exists x1
  48. 0048exact hn_witness_right
  49. 0049specialize odd_not_even (m + n)
  50. 0050apply odd_not_even
  51. 0051exact hsum
  52. 0052exact heven