### Nuprl Lemma : rmul_preserves_rless

`∀x,y,z:ℝ.  ((r0 < y) `` (x < z `⇐⇒` (x * y) < (z * y)))`

Proof

Definitions occuring in Statement :  rless: `x < y` rmul: `a * b` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` uimplies: `b supposing a`
Lemmas referenced :  rless_wf rmul_wf int-to-real_wf real_wf rmul_functionality_wrt_rless rinv_wf2 rinv-positive rless_functionality req_transitivity req_inversion rmul-assoc rmul_functionality req_weakening rmul-rinv rmul-one-both
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality dependent_functionElimination independent_functionElimination sqequalRule inrFormation because_Cache independent_isectElimination productElimination

Latex:
\mforall{}x,y,z:\mBbbR{}.    ((r0  <  y)  {}\mRightarrow{}  (x  <  z  \mLeftarrow{}{}\mRightarrow{}  (x  *  y)  <  (z  *  y)))

Date html generated: 2016_05_18-AM-07_12_23
Last ObjectModification: 2015_12_28-AM-00_40_30

Theory : reals

Home Index