---

Step * of Lemma absval_cases

∀x:ℤ. ∀[y:ℕ]. uiff(|x| = y ∈ ℤ;(x = y ∈ ℤ) ∨ (x = (-y) ∈ ℤ))
BY
{ Auto }

1
1. x : ℤ
2. [y] : ℕ
3. |x| = y ∈ ℤ
⊢ (x = y ∈ ℤ) ∨ (x = (-y) ∈ ℤ)

2
1. x : ℤ
2. y : ℕ
3. (x = y ∈ ℤ) ∨ (x = (-y) ∈ ℤ)
⊢ |x| = y ∈ ℤ

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  \mforall{}[y:\mBbbN{}].  uiff(|x|  =  y;(x  =  y)  \mvee{}  (x  =  (-y)))


By

---

Latex:
Auto

---

Home Index