---

Step * 1 1 of Lemma div_unique3


1. a : ℤ
2. n : ℤ-o
3. [p] : ℤ
4. (a ÷ n) = p ∈ ℤ
⊢ |a rem n| < |n|
∧ (a = ((p * n) + (a rem n)) ∈ ℤ)
∧ ((0 ≤ a) ⇒ (0 ≤ (a rem n)))
∧ (0 < a rem n ⇒ 0 < a)
∧ (a rem n < 0 ⇒ a < 0)
BY
{ TACTIC:D 0 }

1
1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. (a ÷ n) = p ∈ ℤ
⊢ |a rem n| < |n|

2
1. a : ℤ
2. n : ℤ-o
3. [p] : ℤ
4. (a ÷ n) = p ∈ ℤ
⊢ (a = ((p * n) + (a rem n)) ∈ ℤ) ∧ ((0 ≤ a) ⇒ (0 ≤ (a rem n))) ∧ (0 < a rem n ⇒ 0 < a) ∧ (a rem n < 0 ⇒ a < 0)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  [p]  :  \mBbbZ{}
4.  (a  \mdiv{}  n)  =  p
\mvdash{}  |a  rem  n|  <  |n|
\mwedge{}  (a  =  ((p  *  n)  +  (a  rem  n)))
\mwedge{}  ((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:
TACTIC:D  0

---

Home Index