PA00D5

mod_two_zero_sum_to_congruent

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

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

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites mod_eq_symm, mod_two_zero_to_even, even_sum_parity_cases, matching_parity_mod_two as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA003L mod_eq_symm PA00D4 mod_two_zero_to_even PA00CA even_sum_parity_cases PA00CJ matching_parity_mod_two

Proof neighborhood

Direct dependencies

PA003L mod_eq_symm PA00D4 mod_two_zero_to_even PA00CA even_sum_parity_cases PA00CJ matching_parity_mod_two

Direct dependents

PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum

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 q
  2. 0002intro e
  3. 0003intro hzero
  4. 0004have 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 : 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 : (((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