PA00FL

mod_two_preserves_parity

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

Balanced congruence modulo two preserves both parity predicates.

Exact expanded PA statement

forall n m. (exists pmt_u_n_m pmt_v_n_m. n + 2 * pmt_u_n_m = m + 2 * pmt_v_n_m) -> (((((exists pmt_even_n. n = 2 * pmt_even_n) -> (exists pmt_even_m. m = 2 * pmt_even_m)) /\ ((exists pmt_even_m. m = 2 * pmt_even_m) -> (exists pmt_even_n. n = 2 * pmt_even_n)))) /\ ((((exists pmt_odd_n. n = 2 * pmt_odd_n + 1) -> (exists pmt_odd_m. m = 2 * pmt_odd_m + 1)) /\ ((exists pmt_odd_m. m = 2 * pmt_odd_m + 1) -> (exists pmt_odd_n. n = 2 * pmt_odd_n + 1)))))

Structural proof guide

Generated structural guide

Balanced congruence modulo two preserves both parity predicates.

Use the direct prerequisites even_to_mod_two_zero, mod_two_zero_to_even, odd_to_mod_two_one, mod_two_one_to_odd, mod_eq_symm, mod_eq_trans as previously established PA formulas.

The proof proceeds by intermediate claims (9).

Referenced ingredients

PA00CH even_to_mod_two_zero PA00D4 mod_two_zero_to_even PA00CI odd_to_mod_two_one PA00FK mod_two_one_to_odd PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00CH even_to_mod_two_zero PA00D4 mod_two_zero_to_even PA00CI odd_to_mod_two_one PA00FK mod_two_one_to_odd PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00FN qres_same_status_from_even_half_product_mod_two PA00FT qres_opposite_status_from_odd_half_product_mod_two

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 n
  2. 0002intro m
  3. 0003intro hmod
  4. 0004have hback : exists pmt_u_m_n pmt_v_m_n. m + 2 * pmt_u_m_n = n + 2 * pmt_v_m_n
  5. 0005specialize mod_eq_symm 2
  6. 0006specialize mod_eq_symm n
  7. 0007specialize mod_eq_symm m
  8. 0008apply mod_eq_symm
  9. 0009exact hmod
  10. 0010split
  11. 0011split
  12. 0012intro hneven
  13. 0013have hnzero : exists pmt_u_n_zero pmt_v_n_zero. n + 2 * pmt_u_n_zero = 0 + 2 * pmt_v_n_zero
  14. 0014specialize even_to_mod_two_zero n
  15. 0015apply even_to_mod_two_zero
  16. 0016exact hneven
  17. 0017have hmzero : exists pmt_u_m_zero pmt_v_m_zero. m + 2 * pmt_u_m_zero = 0 + 2 * pmt_v_m_zero
  18. 0018specialize mod_eq_trans 2
  19. 0019specialize mod_eq_trans m
  20. 0020specialize mod_eq_trans n
  21. 0021specialize mod_eq_trans 0
  22. 0022apply mod_eq_trans
  23. 0023exact hback
  24. 0024exact hnzero
  25. 0025specialize mod_two_zero_to_even m
  26. 0026apply mod_two_zero_to_even
  27. 0027exact hmzero
  28. 0028intro hmeven
  29. 0029have hmzero : exists pmt_u_m_zero pmt_v_m_zero. m + 2 * pmt_u_m_zero = 0 + 2 * pmt_v_m_zero
  30. 0030specialize even_to_mod_two_zero m
  31. 0031apply even_to_mod_two_zero
  32. 0032exact hmeven
  33. 0033have hnzero : exists pmt_u_n_zero pmt_v_n_zero. n + 2 * pmt_u_n_zero = 0 + 2 * pmt_v_n_zero
  34. 0034specialize mod_eq_trans 2
  35. 0035specialize mod_eq_trans n
  36. 0036specialize mod_eq_trans m
  37. 0037specialize mod_eq_trans 0
  38. 0038apply mod_eq_trans
  39. 0039exact hmod
  40. 0040exact hmzero
  41. 0041specialize mod_two_zero_to_even n
  42. 0042apply mod_two_zero_to_even
  43. 0043exact hnzero
  44. 0044split
  45. 0045intro hnodd
  46. 0046have hnone : exists pmt_u_n_one pmt_v_n_one. n + 2 * pmt_u_n_one = 1 + 2 * pmt_v_n_one
  47. 0047specialize odd_to_mod_two_one n
  48. 0048apply odd_to_mod_two_one
  49. 0049exact hnodd
  50. 0050have hmone : exists pmt_u_m_one pmt_v_m_one. m + 2 * pmt_u_m_one = 1 + 2 * pmt_v_m_one
  51. 0051specialize mod_eq_trans 2
  52. 0052specialize mod_eq_trans m
  53. 0053specialize mod_eq_trans n
  54. 0054specialize mod_eq_trans 1
  55. 0055apply mod_eq_trans
  56. 0056exact hback
  57. 0057exact hnone
  58. 0058specialize mod_two_one_to_odd m
  59. 0059apply mod_two_one_to_odd
  60. 0060exact hmone
  61. 0061intro hmodd
  62. 0062have hmone : exists pmt_u_m_one pmt_v_m_one. m + 2 * pmt_u_m_one = 1 + 2 * pmt_v_m_one
  63. 0063specialize odd_to_mod_two_one m
  64. 0064apply odd_to_mod_two_one
  65. 0065exact hmodd
  66. 0066have hnone : exists pmt_u_n_one pmt_v_n_one. n + 2 * pmt_u_n_one = 1 + 2 * pmt_v_n_one
  67. 0067specialize mod_eq_trans 2
  68. 0068specialize mod_eq_trans n
  69. 0069specialize mod_eq_trans m
  70. 0070specialize mod_eq_trans 1
  71. 0071apply mod_eq_trans
  72. 0072exact hmod
  73. 0073exact hmone
  74. 0074specialize mod_two_one_to_odd n
  75. 0075apply mod_two_one_to_odd
  76. 0076exact hnone