Step * of Lemma rem_sym

No Annotations
[a:ℤ]. ∀[b:ℤ-o].  ((a rem -b) (a rem b) ∈ ℤ)
BY
(Auto THEN (Decide ⌜0 ≤ b⌝ THENA Auto)) }

1
1. : ℤ
2. : ℤ-o
3. 0 ≤ b
⊢ (a rem -b) (a rem b) ∈ ℤ

2
1. : ℤ
2. : ℤ-o
3. ¬(0 ≤ b)
⊢ (a rem -b) (a rem b) ∈ ℤ


Latex:


Latex:
No  Annotations
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    ((a  rem  -b)  =  (a  rem  b))


By


Latex:
(Auto  THEN  (Decide  \mkleeneopen{}0  \mleq{}  b\mkleeneclose{}  THENA  Auto))




Home Index