---

Step * of Lemma qabs-zero

∀[r:ℚ]. uiff(r = 0 ∈ ℚ;|r| = 0 ∈ ℚ)
BY
{ Auto }

1
1. r : ℚ
2. r = 0 ∈ ℚ
⊢ |r| = 0 ∈ ℚ

2
1. r : ℚ
2. |r| = 0 ∈ ℚ
⊢ r = 0 ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  uiff(r  =  0;|r|  =  0)


By

---

Latex:
Auto

---

Home Index