### Nuprl Lemma : rmul_functionality_wrt_rless

`∀x,y,z:ℝ.  ((x < z) `` (r0 < y) `` ((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]` 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]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)` uimplies: `b supposing a`
Lemmas referenced :  rlessw_wf rmul_wf rless-iff-rpositive int-to-real_wf rless_wf real_wf rpositive-rmul rsub_wf real_term_polynomial itermSubtract_wf itermMultiply_wf itermVar_wf itermConstant_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma req-iff-rsub-is-0 rpositive_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality hypothesis dependent_set_memberEquality natural_numberEquality productElimination independent_functionElimination sqequalRule computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_isectElimination

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

Date html generated: 2017_10_03-AM-08_26_38
Last ObjectModification: 2017_07_28-AM-07_24_27

Theory : reals

Home Index