PA00CJ

matching_parity_mod_two

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

Naturals with the same constructive parity are congruent modulo two.

Exact expanded PA statement

forall x y. ((((exists sdp_even_matching_x. x = 2 * sdp_even_matching_x) /\ (exists sdp_even_matching_y. y = 2 * sdp_even_matching_y)) \/ ((exists sdp_odd_matching_x. x = 2 * sdp_odd_matching_x + 1) /\ (exists sdp_odd_matching_y. y = 2 * sdp_odd_matching_y + 1)))) -> (exists sdp_u_matching_result sdp_v_matching_result. (x) + 2 * sdp_u_matching_result = (y) + 2 * sdp_v_matching_result)

Structural proof guide

Generated structural guide

Naturals with the same constructive parity are congruent modulo two.

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

The proof proceeds by case analysis (3), intermediate claims (6).

Referenced ingredients

PA00CH even_to_mod_two_zero PA00CI odd_to_mod_two_one PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00CH even_to_mod_two_zero PA00CI odd_to_mod_two_one PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00CK odd_product_division_mod_two PA00D5 mod_two_zero_sum_to_congruent

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 x
  2. 0002intro y
  3. 0003intro hmatching
  4. 0004cases hmatching
  5. 0005cases hmatching_left
  6. 0006have hxzero : exists sdp_u_proof_x_zero sdp_v_proof_x_zero. (x) + 2 * sdp_u_proof_x_zero = (0) + 2 * sdp_v_proof_x_zero
  7. 0007specialize even_to_mod_two_zero x
  8. 0008apply even_to_mod_two_zero
  9. 0009exact hmatching_left_left
  10. 0010have hyzero : exists sdp_u_proof_y_zero sdp_v_proof_y_zero. (y) + 2 * sdp_u_proof_y_zero = (0) + 2 * sdp_v_proof_y_zero
  11. 0011specialize even_to_mod_two_zero y
  12. 0012apply even_to_mod_two_zero
  13. 0013exact hmatching_left_right
  14. 0014have hzeroy : exists sdp_u_proof_zero_y sdp_v_proof_zero_y. (0) + 2 * sdp_u_proof_zero_y = (y) + 2 * sdp_v_proof_zero_y
  15. 0015specialize mod_eq_symm 2
  16. 0016specialize mod_eq_symm y
  17. 0017specialize mod_eq_symm 0
  18. 0018apply mod_eq_symm
  19. 0019exact hyzero
  20. 0020specialize mod_eq_trans 2
  21. 0021specialize mod_eq_trans x
  22. 0022specialize mod_eq_trans 0
  23. 0023specialize mod_eq_trans y
  24. 0024apply mod_eq_trans
  25. 0025exact hxzero
  26. 0026exact hzeroy
  27. 0027cases hmatching_right
  28. 0028have hxone : exists sdp_u_proof_x_one sdp_v_proof_x_one. (x) + 2 * sdp_u_proof_x_one = (1) + 2 * sdp_v_proof_x_one
  29. 0029specialize odd_to_mod_two_one x
  30. 0030apply odd_to_mod_two_one
  31. 0031exact hmatching_right_left
  32. 0032have hyone : exists sdp_u_proof_y_one sdp_v_proof_y_one. (y) + 2 * sdp_u_proof_y_one = (1) + 2 * sdp_v_proof_y_one
  33. 0033specialize odd_to_mod_two_one y
  34. 0034apply odd_to_mod_two_one
  35. 0035exact hmatching_right_right
  36. 0036have honey : exists sdp_u_proof_one_y sdp_v_proof_one_y. (1) + 2 * sdp_u_proof_one_y = (y) + 2 * sdp_v_proof_one_y
  37. 0037specialize mod_eq_symm 2
  38. 0038specialize mod_eq_symm y
  39. 0039specialize mod_eq_symm 1
  40. 0040apply mod_eq_symm
  41. 0041exact hyone
  42. 0042specialize mod_eq_trans 2
  43. 0043specialize mod_eq_trans x
  44. 0044specialize mod_eq_trans 1
  45. 0045specialize mod_eq_trans y
  46. 0046apply mod_eq_trans
  47. 0047exact hxone
  48. 0048exact honey