### Nuprl Lemma : small-reciprocal-rneq-zero

`∀x:ℝ. (x ≠ r0 `` (∃k:ℕ+. ((r1/r(k)) < |x|)))`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` rneq: `x ≠ y` rless: `x < y` rabs: `|x|` int-to-real: `r(n)` real: `ℝ` nat_plus: `ℕ+` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  small-reciprocal-real-ext rabs_wf rless_wf int-to-real_wf rneq_wf real_wf rpositive-rless rabs-positive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin dependent_set_memberEquality isectElimination hypothesisEquality hypothesis natural_numberEquality productElimination independent_functionElimination

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}\msupplus{}.  ((r1/r(k))  <  |x|)))

Date html generated: 2016_05_18-AM-07_34_37
Last ObjectModification: 2015_12_28-AM-00_55_49

Theory : reals

Home Index