### Nuprl Lemma : rinv-positive

`∀x:ℝ. ((r0 < x) `` (r0 < rinv(x)))`

Proof

Definitions occuring in Statement :  rless: `x < y` rinv: `rinv(x)` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` rneq: `x ≠ y` or: `P ∨ Q` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` rpositive: `rpositive(x)` sq_exists: `∃x:A [B[x]]` rinv: `rinv(x)` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` rless: `x < y` real: `ℝ` sq_stable: `SqStable(P)` squash: `↓T` decidable: `Dec(P)` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` has-value: `(a)↓` nat: `ℕ` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` less_than: `a < b` true: `True` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` less_than': `less_than'(a;b)` reg-seq-inv: `reg-seq-inv(x)` rpositive2: `rpositive2(x)` nequal: `a ≠ b ∈ T ` cand: `A c∧ B` int_nzero: `ℤ-o` ge: `i ≥ j ` absval: `|i|` reg-seq-adjust: `reg-seq-adjust(n;x)`

Latex:
\mforall{}x:\mBbbR{}.  ((r0  <  x)  {}\mRightarrow{}  (r0  <  rinv(x)))

Date html generated: 2020_05_20-AM-10_57_21
Last ObjectModification: 2020_01_06-PM-00_27_50

Theory : reals

Home Index