PA00CA

even_sum_parity_cases

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

An even sum has summands of the same parity.

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

Structural proof guide

Generated structural guide

An even sum has summands of the same parity.

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

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

Referenced ingredients

PA0057 parity_cases PA006F even_add_odd PA006G odd_add_even PA0059 even_not_odd

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA006F even_add_odd PA006G odd_add_even PA0059 even_not_odd

Direct dependents

PA00CB even_sum_iff_same_parity PA00D5 mod_two_zero_sum_to_congruent PA00FM qres_same_status_from_even_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. 0014left
  15. 0015split
  16. 0016exists x
  17. 0017exact hm_witness_left
  18. 0018exists x1
  19. 0019exact hn_witness_left
  20. 0020exfalso
  21. 0021have hodd : exists c. m + n = 2 * c + 1
  22. 0022specialize even_add_odd m
  23. 0023specialize even_add_odd n
  24. 0024apply even_add_odd
  25. 0025exists x
  26. 0026exact hm_witness_left
  27. 0027exists x1
  28. 0028exact hn_witness_right
  29. 0029specialize even_not_odd (m + n)
  30. 0030apply even_not_odd
  31. 0031exact hsum
  32. 0032exact hodd
  33. 0033cases hn_witness
  34. 0034exfalso
  35. 0035have hodd : exists c. m + n = 2 * c + 1
  36. 0036specialize odd_add_even m
  37. 0037specialize odd_add_even n
  38. 0038apply odd_add_even
  39. 0039exists x
  40. 0040exact hm_witness_right
  41. 0041exists x1
  42. 0042exact hn_witness_left
  43. 0043specialize even_not_odd (m + n)
  44. 0044apply even_not_odd
  45. 0045exact hsum
  46. 0046exact hodd
  47. 0047right
  48. 0048split
  49. 0049exists x
  50. 0050exact hm_witness_right
  51. 0051exists x1
  52. 0052exact hn_witness_right