PA00FL · theorem

mod_two_preserves_parity

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

Balanced congruence modulo two preserves both parity predicates.

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

∀ n. ∀ m. ModEq(2,n,m) → (Even(n) → Even(m)) ∧ (Even(m) → Even(n)) ∧ ((Odd(n) → Odd(m)) ∧ (Odd(m) → Odd(n)))

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

9 occurrences

In local proof propositions

PD0008 ModEq

9 occurrences

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

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

PA00FN qres_same_status_from_even_half_product_mod_two PA00FT qres_opposite_status_from_odd_half_product_mod_two

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

76 script commands · 20 reading checkpoints · 9 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 (6)
even to mod two zeromod two zero to evenodd to mod two onemod two one to oddmod eq symmmod eq trans
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro m
  3. L3
    intro hmod
02Establish hbackL4–9

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

  1. L4
    have hback : ModEq(2,m,n)Definitions: ModEq(2,m,n)Original native command in the exact edition
  2. L5
    specialize mod_eq_symm 2
  3. L6
    specialize mod_eq_symm n
  4. L7
    specialize mod_eq_symm m
  5. L8
    apply mod_eq_symm
  6. L9
    exact hmod
03Separate the logical casesL10–11

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

  1. L10
    split
  2. L11
    split
04Fix variables and assumptionsL12–12

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

  1. L12
    intro hneven
05Establish hnzeroL13–16

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

  1. L13
    have hnzero : ModEq(2,n,0)Definitions: ModEq(2,n,0)Original native command in the exact edition
  2. L14
    specialize even_to_mod_two_zero n
  3. L15
    apply even_to_mod_two_zero
  4. L16
    exact hneven
06Establish hmzeroL17–26

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

  1. L17
    have hmzero : ModEq(2,m,0)Definitions: ModEq(2,m,0)Original native command in the exact edition
  2. L18
    specialize mod_eq_trans 2
  3. L19
    specialize mod_eq_trans m
  4. L20
    specialize mod_eq_trans n
  5. L21
    specialize mod_eq_trans 0
  6. L22
    apply mod_eq_trans
  7. L23
    exact hback
  8. L24
    exact hnzero
  9. L25
    specialize mod_two_zero_to_even m
  10. L26
    apply mod_two_zero_to_even
07Use earlier factsL27–27

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

  1. L27
    exact hmzero
08Fix variables and assumptionsL28–28

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

  1. L28
    intro hmeven
09Establish hmzeroL29–32

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

  1. L29
    have hmzero : ModEq(2,m,0)Definitions: ModEq(2,m,0)Original native command in the exact edition
  2. L30
    specialize even_to_mod_two_zero m
  3. L31
    apply even_to_mod_two_zero
  4. L32
    exact hmeven
10Establish hnzeroL33–42

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

  1. L33
    have hnzero : ModEq(2,n,0)Definitions: ModEq(2,n,0)Original native command in the exact edition
  2. L34
    specialize mod_eq_trans 2
  3. L35
    specialize mod_eq_trans n
  4. L36
    specialize mod_eq_trans m
  5. L37
    specialize mod_eq_trans 0
  6. L38
    apply mod_eq_trans
  7. L39
    exact hmod
  8. L40
    exact hmzero
  9. L41
    specialize mod_two_zero_to_even n
  10. L42
    apply mod_two_zero_to_even
11Use earlier factsL43–43

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

  1. L43
    exact hnzero
12Separate the logical casesL44–44

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

  1. L44
    split
13Fix variables and assumptionsL45–45

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

  1. L45
    intro hnodd
14Establish hnoneL46–49

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

  1. L46
    have hnone : ModEq(2,n,1)Definitions: ModEq(2,n,1)Original native command in the exact edition
  2. L47
    specialize odd_to_mod_two_one n
  3. L48
    apply odd_to_mod_two_one
  4. L49
    exact hnodd
15Establish hmoneL50–59

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

  1. L50
    have hmone : ModEq(2,m,1)Definitions: ModEq(2,m,1)Original native command in the exact edition
  2. L51
    specialize mod_eq_trans 2
  3. L52
    specialize mod_eq_trans m
  4. L53
    specialize mod_eq_trans n
  5. L54
    specialize mod_eq_trans 1
  6. L55
    apply mod_eq_trans
  7. L56
    exact hback
  8. L57
    exact hnone
  9. L58
    specialize mod_two_one_to_odd m
  10. L59
    apply mod_two_one_to_odd
16Use earlier factsL60–60

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

  1. L60
    exact hmone
17Fix variables and assumptionsL61–61

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

  1. L61
    intro hmodd
18Establish hmoneL62–65

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

  1. L62
    have hmone : ModEq(2,m,1)Definitions: ModEq(2,m,1)Original native command in the exact edition
  2. L63
    specialize odd_to_mod_two_one m
  3. L64
    apply odd_to_mod_two_one
  4. L65
    exact hmodd
19Establish hnoneL66–75

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

  1. L66
    have hnone : ModEq(2,n,1)Definitions: ModEq(2,n,1)Original native command in the exact edition
  2. L67
    specialize mod_eq_trans 2
  3. L68
    specialize mod_eq_trans n
  4. L69
    specialize mod_eq_trans m
  5. L70
    specialize mod_eq_trans 1
  6. L71
    apply mod_eq_trans
  7. L72
    exact hmod
  8. L73
    exact hmone
  9. L74
    specialize mod_two_one_to_odd n
  10. L75
    apply mod_two_one_to_odd
20Use earlier factsL76–76

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

  1. L76
    exact hnone

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro n
  2. 0002intro m
  3. 0003intro hmod
  4. 0004have hback : ModEq(2,m,n)
    Exact native replay linehave 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 : ModEq(2,n,0)
    Exact native replay linehave 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 : ModEq(2,m,0)
    Exact native replay linehave 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 : ModEq(2,m,0)
    Exact native replay linehave 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 : ModEq(2,n,0)
    Exact native replay linehave 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 : ModEq(2,n,1)
    Exact native replay linehave 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 : ModEq(2,m,1)
    Exact native replay linehave 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 : ModEq(2,m,1)
    Exact native replay linehave 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 : ModEq(2,n,1)
    Exact native replay linehave 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