PA00D5 · theorem

mod_two_zero_sum_to_congruent

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

If q+e is zero modulo two, q and e have the same parity and are congruent.

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

∀ q. ∀ e. ModEq(2,0,q + e) → ModEq(2,q,e)

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

2 occurrences

In local proof propositions

PD0008 ModEq PD0009 Even PD0010 Odd

6 occurrences

Exact expanded native-PA statement
forall q e. (exists fspm_u_zero_sum_input fspm_v_zero_sum_input. (0) + 2 * fspm_u_zero_sum_input = (q + e) + 2 * fspm_v_zero_sum_input) -> (exists fspm_u_zero_sum_result fspm_v_zero_sum_result. (q) + 2 * fspm_u_zero_sum_result = (e) + 2 * fspm_v_zero_sum_result)

Proof neighborhood

Direct theorem prerequisites

PA003L mod_eq_symm PA00D4 mod_two_zero_to_even PA00CA even_sum_parity_cases PA00CJ matching_parity_mod_two

Direct theorem dependents

PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum

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

22 script commands · 4 reading checkpoints · 3 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)
mod eq symmmod two zero to eveneven sum parity casesmatching parity mod two
01Fix variables and assumptionsL1–3

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

  1. L1
    intro q
  2. L2
    intro e
  3. L3
    intro hzero
02Establish hsum_zeroL4–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 hsum_zero : ModEq(2,q + e,0)Definitions: ModEq(2,q + e,0)Original native command in the exact edition
  2. L5
    specialize mod_eq_symm 2
  3. L6
    specialize mod_eq_symm 0
  4. L7
    specialize mod_eq_symm (q + e)
  5. L8
    apply mod_eq_symm
  6. L9
    exact hzero
03Establish hevenL10–13

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

  1. L10
    have heven : Even(q + e)Definitions: Even(q + e)Original native command in the exact edition
  2. L11
    specialize mod_two_zero_to_even (q + e)
  3. L12
    apply mod_two_zero_to_even
  4. L13
    exact hsum_zero
04Establish hsameL14–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even sum parity cases.

  1. L14
    have hsame : Even(q) ∧ Even(e) ∨ Odd(q) ∧ Odd(e)Definitions: Even(q)Even(e)Odd(q)Odd(e)Original native command in the exact edition
  2. L15
    specialize even_sum_parity_cases q
  3. L16
    specialize even_sum_parity_cases e
  4. L17
    apply even_sum_parity_cases
  5. L18
    exact heven
  6. L19
    specialize matching_parity_mod_two q
  7. L20
    specialize matching_parity_mod_two e
  8. L21
    apply matching_parity_mod_two
  9. L22
    exact hsame

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro q
  2. 0002intro e
  3. 0003intro hzero
  4. 0004have hsum_zero : ModEq(2,q + e,0)
    Exact native replay linehave hsum_zero : exists fspm_u_sum_zero fspm_v_sum_zero. (q + e) + 2 * fspm_u_sum_zero = (0) + 2 * fspm_v_sum_zero
  5. 0005specialize mod_eq_symm 2
  6. 0006specialize mod_eq_symm 0
  7. 0007specialize mod_eq_symm (q + e)
  8. 0008apply mod_eq_symm
  9. 0009exact hzero
  10. 0010have heven : Even(q + e)
    Exact native replay linehave heven : exists fspm_even_sum. q + e = 2 * fspm_even_sum
  11. 0011specialize mod_two_zero_to_even (q + e)
  12. 0012apply mod_two_zero_to_even
  13. 0013exact hsum_zero
  14. 0014have hsame : Even(q) ∧ Even(e) ∨ Odd(q) ∧ Odd(e)
    Exact native replay linehave hsame : (((exists fspm_even_q. q = 2 * fspm_even_q) /\ (exists fspm_even_e. e = 2 * fspm_even_e)) \/ ((exists fspm_odd_q. q = 2 * fspm_odd_q + 1) /\ (exists fspm_odd_e. e = 2 * fspm_odd_e + 1)))
  15. 0015specialize even_sum_parity_cases q
  16. 0016specialize even_sum_parity_cases e
  17. 0017apply even_sum_parity_cases
  18. 0018exact heven
  19. 0019specialize matching_parity_mod_two q
  20. 0020specialize matching_parity_mod_two e
  21. 0021apply matching_parity_mod_two
  22. 0022exact hsame