### Nuprl Lemma : rmul_reverses_rless_iff

`∀x,y,z:ℝ.  ((y < r0) `` (x < z `⇐⇒` (z * y) < (x * 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` uimplies: `b supposing a` rneq: `x ≠ y` or: `P ∨ Q` rdiv: `(x/y)` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  rless_wf rmul_wf int-to-real_wf real_wf rmul_reverses_rless rdiv_wf rinv-negative rless-implies-rless rinv_wf2 real_term_polynomial itermSubtract_wf itermConstant_wf itermVar_wf itermMultiply_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma real_term_value_mul_lemma req-iff-rsub-is-0 rsub_wf req_wf req_weakening rless_functionality uiff_transitivity req_functionality req_inversion rmul-assoc rmul_functionality rmul_comm req_transitivity rmul-ac rmul-rdiv-cancel rmul-one-both
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality independent_functionElimination dependent_functionElimination lemma_by_obid independent_isectElimination inlFormation because_Cache sqequalRule computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality productElimination promote_hyp

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

Date html generated: 2017_10_03-AM-08_35_08
Last ObjectModification: 2017_07_28-AM-07_28_50

Theory : reals

Home Index