---

Step * of Lemma rv-ip-nonneg

No Annotations
∀[rv:InnerProductSpace]. ∀[x:Point(rv)].  (r0 ≤ x^2)
BY
{ (Auto THEN (DoubleNegation THENA Auto) THEN ((DistinguishCases ⌜x # 0⌝⋅ THENM RemoveDoubleNegation) THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
⊢ r0 ≤ x^2

2
1. rv : InnerProductSpace
2. x : Point(rv)
3. ¬x # 0
⊢ r0 ≤ x^2

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[x:Point(rv)].    (r0  \mleq{}  x\^{}2)


By

---

Latex:
(Auto
  THEN  (DoubleNegation  THENA  Auto)
  THEN  ((DistinguishCases  \mkleeneopen{}x  \#  0\mkleeneclose{}\mcdot{}  THENM  RemoveDoubleNegation)  THENA  Auto))

---

Home Index