PA00D2 · theorem

mod_two_cancel_middle

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

From x == q+x+s modulo two, cancel x and obtain 0 == q+s.

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. ∀ q. ∀ s. ModEq(2,x,q + x + s) → ModEq(2,0,q + s)

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

none

0 occurrences

Exact expanded native-PA statement
forall x q s. (exists fspm_u_cancel_middle_input fspm_v_cancel_middle_input. (x) + 2 * fspm_u_cancel_middle_input = (q + x + s) + 2 * fspm_v_cancel_middle_input) -> (exists fspm_u_cancel_middle_result fspm_v_cancel_middle_result. (0) + 2 * fspm_u_cancel_middle_result = (q + s) + 2 * fspm_v_cancel_middle_result)

Proof neighborhood

Direct theorem prerequisites

PA00D1 mod_eq_add_cancel_left PA0009 add_assoc PA000F add_comm

Direct theorem dependents

PA00D3 gauss_eisenstein_terminal_cancel_magnitude_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

16 script commands · 3 reading checkpoints · 2 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 (1)
mod eq add cancel left
01Fix variables and assumptionsL1–4

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

  1. L1
    intro x
  2. L2
    intro q
  3. L3
    intro s
  4. L4
    intro hmod
02Establish hreorderL5–12

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

  1. L5
    have hreorder : q + x + s = x + (q + s)
  2. L6
    simp [add_assoc, add_comm]
  3. L7
    rewrite hreorder at hmod
  4. L8
    specialize mod_eq_add_cancel_left 2
  5. L9
    specialize mod_eq_add_cancel_left x
  6. L10
    specialize mod_eq_add_cancel_left 0
  7. L11
    specialize mod_eq_add_cancel_left (q + s)
  8. L12
    apply mod_eq_add_cancel_left
03Establish hxzeroL13–16

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

  1. L13
    have hxzero : x + 0 = x
  2. L14
    apply PA3
  3. L15
    rewrite hxzero
  4. L16
    exact hmod

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro x
  2. 0002intro q
  3. 0003intro s
  4. 0004intro hmod
  5. 0005have hreorder : q + x + s = x + (q + s)
  6. 0006simp [add_assoc, add_comm]
  7. 0007rewrite hreorder at hmod
  8. 0008specialize mod_eq_add_cancel_left 2
  9. 0009specialize mod_eq_add_cancel_left x
  10. 0010specialize mod_eq_add_cancel_left 0
  11. 0011specialize mod_eq_add_cancel_left (q + s)
  12. 0012apply mod_eq_add_cancel_left
  13. 0013have hxzero : x + 0 = x
  14. 0014apply PA3
  15. 0015rewrite hxzero
  16. 0016exact hmod