---

Step * of Lemma qabs-qinv

No Annotations
∀[s:{s:ℚ| ¬(s = 0 ∈ ℚ)} ]. (|1/s| = 1/|s| ∈ ℚ)
BY
{ (Auto THEN Assert ⌜(¬(s = 0 ∈ ℚ)) ∧ (¬(|s| = 0 ∈ ℚ))⌝⋅) }

1
.....assertion..... 
1. s : {s:ℚ| ¬(s = 0 ∈ ℚ)} 
⊢ (¬(s = 0 ∈ ℚ)) ∧ (¬(|s| = 0 ∈ ℚ))

2
1. s : {s:ℚ| ¬(s = 0 ∈ ℚ)} 
2. (¬(s = 0 ∈ ℚ)) ∧ (¬(|s| = 0 ∈ ℚ))
⊢ |1/s| = 1/|s| ∈ ℚ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[s:\{s:\mBbbQ{}|  \mneg{}(s  =  0)\}  ].  (|1/s|  =  1/|s|)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}(\mneg{}(s  =  0))  \mwedge{}  (\mneg{}(|s|  =  0))\mkleeneclose{}\mcdot{})

---

Home Index