Step
*
1
of Lemma
rinv-negative
1. x : ℝ
2. x < r0
3. r0 < -(x)
⊢ rinv(x) < r0
BY
{ ((FLemma `rinv-positive` [-1] THENA Auto) THEN (RWO "rinv-rminus<" (-1) THENA Auto)) }
1
1. x : ℝ
2. x < r0
3. r0 < -(x)
4. r0 < -(rinv(x))
⊢ rinv(x) < r0
Latex:
Latex:
1. x : \mBbbR{}
2. x < r0
3. r0 < -(x)
\mvdash{} rinv(x) < r0
By
Latex:
((FLemma `rinv-positive` [-1] THENA Auto) THEN (RWO "rinv-rminus<" (-1) THENA Auto))
Home
Index