---

Step * 2 1 2 1 of Lemma div_unique3

.....assertion..... 
1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n| ∧ (a = ((p * n) + r) ∈ ℤ) ∧ ((0 ≤ a) ⇒ (0 ≤ r)) ∧ (0 < r ⇒ 0 < a) ∧ (r < 0 ⇒ a < 0)
6. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
7. |a rem n| < |n|
8. ((p - a ÷ n) * n) = ((a rem n) - r) ∈ ℤ
⊢ |(a rem n) - r| < |n|
BY
{ TACTIC:Assert ⌜∀x,y,z:ℤ.  (((0 < x ⇒ (0 ≤ y)) ∧ (0 < y ⇒ (0 ≤ x))) ⇒ |x| < z ⇒ |y| < z ⇒ |x - y| < z)⌝⋅ }

1
.....assertion..... 
1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n| ∧ (a = ((p * n) + r) ∈ ℤ) ∧ ((0 ≤ a) ⇒ (0 ≤ r)) ∧ (0 < r ⇒ 0 < a) ∧ (r < 0 ⇒ a < 0)
6. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
7. |a rem n| < |n|
8. ((p - a ÷ n) * n) = ((a rem n) - r) ∈ ℤ
⊢ ∀x,y,z:ℤ.  (((0 < x ⇒ (0 ≤ y)) ∧ (0 < y ⇒ (0 ≤ x))) ⇒ |x| < z ⇒ |y| < z ⇒ |x - y| < z)

2
1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n| ∧ (a = ((p * n) + r) ∈ ℤ) ∧ ((0 ≤ a) ⇒ (0 ≤ r)) ∧ (0 < r ⇒ 0 < a) ∧ (r < 0 ⇒ a < 0)
6. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
7. |a rem n| < |n|
8. ((p - a ÷ n) * n) = ((a rem n) - r) ∈ ℤ
9. ∀x,y,z:ℤ.  (((0 < x ⇒ (0 ≤ y)) ∧ (0 < y ⇒ (0 ≤ x))) ⇒ |x| < z ⇒ |y| < z ⇒ |x - y| < z)
⊢ |(a rem n) - r| < |n|

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  p  :  \mBbbZ{}
4.  r  :  \mBbbZ{}
5.  |r|  <  |n|  \mwedge{}  (a  =  ((p  *  n)  +  r))  \mwedge{}  ((0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  r))  \mwedge{}  (0  <  r  {}\mRightarrow{}  0  <  a)  \mwedge{}  (r  <  0  {}\mRightarrow{}  a  <  0)
6.  a  =  (((a  \mdiv{}  n)  *  n)  +  (a  rem  n))
7.  |a  rem  n|  <  |n|
8.  ((p  -  a  \mdiv{}  n)  *  n)  =  ((a  rem  n)  -  r)
\mvdash{}  |(a  rem  n)  -  r|  <  |n|


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y,z:\mBbbZ{}.
                                  (((0  <  x  {}\mRightarrow{}  (0  \mleq{}  y))  \mwedge{}  (0  <  y  {}\mRightarrow{}  (0  \mleq{}  x)))  {}\mRightarrow{}  |x|  <  z  {}\mRightarrow{}  |y|  <  z  {}\mRightarrow{}  |x  -  y|  <  z)\mkleeneclose{}\mcdot{}

---

Home Index