### Nuprl Lemma : rabs-rless-iff

`∀x,z:ℝ.  (|x| < z `⇐⇒` (-(z) < x) ∧ (x < z))`

Proof

Definitions occuring in Statement :  rless: `x < y` rabs: `|x|` rminus: `-(x)` real: `ℝ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` and: `P ∧ Q` rsub: `x - y` iff: `P `⇐⇒` Q` implies: `P `` Q` uimplies: `b supposing a` rev_implies: `P `` Q`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination natural_numberEquality hypothesis because_Cache productEquality sqequalRule productElimination independent_pairFormation independent_functionElimination independent_isectElimination promote_hyp

Latex:
\mforall{}x,z:\mBbbR{}.    (|x|  <  z  \mLeftarrow{}{}\mRightarrow{}  (-(z)  <  x)  \mwedge{}  (x  <  z))

Date html generated: 2016_10_26-AM-09_10_23
Last ObjectModification: 2016_09_01-PM-01_37_12

Theory : reals

Home Index