---

Step * 2 1 2 2 1 2 1 1 of Lemma div_unique3


1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n|
6. a = ((p * n) + r) ∈ ℤ
7. (0 ≤ a) ⇒ (0 ≤ r)
8. 0 < r ⇒ 0 < a
9. r < 0 ⇒ a < 0
10. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
11. |a rem n| < |n|
12. ((p - a ÷ n) * n) = ((a rem n) - r) ∈ ℤ
13. |(a rem n) - r| < |n|
14. |(p - a ÷ n) * n| = |(a rem n) - r| ∈ ℤ
15. (|p - a ÷ n| * |n|) = |(a rem n) - r| ∈ ℤ
16. ¬(|p - a ÷ n| = 0 ∈ ℤ)
⊢ 1 ≤ |p - a ÷ n|
BY
{ TACTIC:(MoveToConcl (-1) THEN (GenConclTerm ⌜|p - a ÷ n|⌝⋅ THENA Auto) THEN All Thin) }

1
1. v : ℕ
⊢ (¬(v = 0 ∈ ℤ)) ⇒ (1 ≤ v)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  p  :  \mBbbZ{}
4.  r  :  \mBbbZ{}
5.  |r|  <  |n|
6.  a  =  ((p  *  n)  +  r)
7.  (0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  r)
8.  0  <  r  {}\mRightarrow{}  0  <  a
9.  r  <  0  {}\mRightarrow{}  a  <  0
10.  a  =  (((a  \mdiv{}  n)  *  n)  +  (a  rem  n))
11.  |a  rem  n|  <  |n|
12.  ((p  -  a  \mdiv{}  n)  *  n)  =  ((a  rem  n)  -  r)
13.  |(a  rem  n)  -  r|  <  |n|
14.  |(p  -  a  \mdiv{}  n)  *  n|  =  |(a  rem  n)  -  r|
15.  (|p  -  a  \mdiv{}  n|  *  |n|)  =  |(a  rem  n)  -  r|
16.  \mneg{}(|p  -  a  \mdiv{}  n|  =  0)
\mvdash{}  1  \mleq{}  |p  -  a  \mdiv{}  n|


By

---

Latex:
TACTIC:(MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}|p  -  a  \mdiv{}  n|\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index