PA00CJ · theorem

matching_parity_mod_two

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

Naturals with the same constructive parity are congruent modulo two.

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

∀ x. ∀ y. Even(x) ∧ Even(y) ∨ Odd(x) ∧ Odd(y) → ModEq(2,x,y)

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

PD0008 ModEq PD0009 Even PD0010 Odd

5 occurrences

In local proof propositions

PD0008 ModEq

6 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA00CH even_to_mod_two_zero PA00CI odd_to_mod_two_one PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA00CK odd_product_division_mod_two PA00D5 mod_two_zero_sum_to_congruent

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

48 script commands · 11 reading checkpoints · 6 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 (4)
even to mod two zeroodd to mod two onemod eq symmmod eq trans
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro x
  2. L2
    intro y
  3. L3
    intro hmatching
02Separate the logical casesL4–5

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L4
    cases hmatching
  2. L5
    cases hmatching_left
03Establish hxzeroL6–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even to mod two zero.

  1. L6
    have hxzero : ModEq(2,x,0)Definitions: ModEq(2,x,0)Original native command in the exact edition
  2. L7
    specialize even_to_mod_two_zero x
  3. L8
    apply even_to_mod_two_zero
  4. L9
    exact hmatching_left_left
04Establish hyzeroL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even to mod two zero.

  1. L10
    have hyzero : ModEq(2,y,0)Definitions: ModEq(2,y,0)Original native command in the exact edition
  2. L11
    specialize even_to_mod_two_zero y
  3. L12
    apply even_to_mod_two_zero
  4. L13
    exact hmatching_left_right
05Establish hzeroyL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L14
    have hzeroy : ModEq(2,0,y)Definitions: ModEq(2,0,y)Original native command in the exact edition
  2. L15
    specialize mod_eq_symm 2
  3. L16
    specialize mod_eq_symm y
  4. L17
    specialize mod_eq_symm 0
  5. L18
    apply mod_eq_symm
  6. L19
    exact hyzero
  7. L20
    specialize mod_eq_trans 2
  8. L21
    specialize mod_eq_trans x
  9. L22
    specialize mod_eq_trans 0
  10. L23
    specialize mod_eq_trans y
06Use earlier factsL24–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    apply mod_eq_trans
  2. L25
    exact hxzero
  3. L26
    exact hzeroy
07Separate the logical casesL27–27

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    cases hmatching_right
08Establish hxoneL28–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd to mod two one.

  1. L28
    have hxone : ModEq(2,x,1)Definitions: ModEq(2,x,1)Original native command in the exact edition
  2. L29
    specialize odd_to_mod_two_one x
  3. L30
    apply odd_to_mod_two_one
  4. L31
    exact hmatching_right_left
09Establish hyoneL32–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd to mod two one.

  1. L32
    have hyone : ModEq(2,y,1)Definitions: ModEq(2,y,1)Original native command in the exact edition
  2. L33
    specialize odd_to_mod_two_one y
  3. L34
    apply odd_to_mod_two_one
  4. L35
    exact hmatching_right_right
10Establish honeyL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L36
    have honey : ModEq(2,1,y)Definitions: ModEq(2,1,y)Original native command in the exact edition
  2. L37
    specialize mod_eq_symm 2
  3. L38
    specialize mod_eq_symm y
  4. L39
    specialize mod_eq_symm 1
  5. L40
    apply mod_eq_symm
  6. L41
    exact hyone
  7. L42
    specialize mod_eq_trans 2
  8. L43
    specialize mod_eq_trans x
  9. L44
    specialize mod_eq_trans 1
  10. L45
    specialize mod_eq_trans y
11Use earlier factsL46–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L46
    apply mod_eq_trans
  2. L47
    exact hxone
  3. L48
    exact honey

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro x
  2. 0002intro y
  3. 0003intro hmatching
  4. 0004cases hmatching
  5. 0005cases hmatching_left
  6. 0006have hxzero : ModEq(2,x,0)
    Exact native replay linehave 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 : ModEq(2,y,0)
    Exact native replay linehave 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 : ModEq(2,0,y)
    Exact native replay linehave 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 : ModEq(2,x,1)
    Exact native replay linehave 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 : ModEq(2,y,1)
    Exact native replay linehave 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 : ModEq(2,1,y)
    Exact native replay linehave 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