---

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


1. p : ℤ
2. v : ℤ
⊢ (|p - v| = 0 ∈ ℤ) ⇒ (v = p ∈ ℤ)
BY
{ TACTIC:(RWO "absval_unfold2" 0 THENA Auto) }

1
1. p : ℤ
2. v : ℤ
⊢ (if (0) < (p - v)  then p - v  else (-(p - v)) = 0 ∈ ℤ) ⇒ (v = p ∈ ℤ)

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}
2.  v  :  \mBbbZ{}
\mvdash{}  (|p  -  v|  =  0)  {}\mRightarrow{}  (v  =  p)


By

---

Latex:
TACTIC:(RWO  "absval\_unfold2"  0  THENA  Auto)

---

Home Index