---

Step * of Lemma rem-sign

∀[a:ℤ]. ∀[n:ℤ-o].  (((0 ≤ a) ⇒ (0 ≤ (a rem n))) ∧ (0 < a rem n ⇒ 0 < a) ∧ (a rem n < 0 ⇒ a < 0))
BY
{ ((UnivCD THENA Auto) THEN (Decide ⌜0 ≤ n⌝⋅ THEN Auto) THEN SupposeNot THEN Auto) }

1
1. a : ℤ
2. n : ℤ-o
3. 0 ≤ n
4. (0 ≤ a) ⇒ (0 ≤ (a rem n))
5. 0 < a rem n@i
6. ¬0 < a
⊢ 0 < a

2
1. a : ℤ
2. n : ℤ-o
3. 0 ≤ n
4. (0 ≤ a) ⇒ (0 ≤ (a rem n))
5. 0 < a rem n ⇒ 0 < a
6. a rem n < 0@i
7. ¬a < 0
⊢ a < 0

3
1. a : ℤ
2. n : ℤ-o
3. ¬(0 ≤ n)
4. (0 ≤ a) ⇒ (0 ≤ (a rem n))
5. 0 < a rem n@i
6. ¬0 < a
⊢ 0 < a

4
1. a : ℤ
2. n : ℤ-o
3. ¬(0 ≤ n)
4. (0 ≤ a) ⇒ (0 ≤ (a rem n))
5. 0 < a rem n ⇒ 0 < a
6. a rem n < 0@i
7. ¬a < 0
⊢ a < 0

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (((0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  (a  rem  n)))  \mwedge{}  (0  <  a  rem  n  {}\mRightarrow{}  0  <  a)  \mwedge{}  (a  rem  n  <  0  {}\mRightarrow{}  a  <  0))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Decide  \mkleeneopen{}0  \mleq{}  n\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  SupposeNot  THEN  Auto)

---

Home Index