### Nuprl Lemma : rmul_reverses_rless

`∀x,y,z:ℝ.  ((x < z) `` (y < r0) `` ((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]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` top: `Top` uiff: `uiff(P;Q)` and: `P ∧ Q` false: `False` not: `¬A` iff: `P `⇐⇒` Q`
Lemmas referenced :  rless_wf int-to-real_wf real_wf rminus-reverses-rless rminus_wf rmul_wf rless_functionality real_term_polynomial itermSubtract_wf itermMinus_wf itermConstant_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_minus_lemma req-iff-rsub-is-0 req_transitivity itermVar_wf itermMultiply_wf real_term_value_var_lemma real_term_value_mul_lemma req_inversion rminus-as-rmul rmul_functionality_wrt_rless rless-implies-rless rsub_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality natural_numberEquality hypothesis dependent_functionElimination independent_functionElimination because_Cache minusEquality independent_isectElimination sqequalRule computeAll lambdaEquality intEquality isect_memberEquality voidElimination voidEquality productElimination int_eqEquality

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

Date html generated: 2017_10_03-AM-08_27_22
Last ObjectModification: 2017_07_28-AM-07_24_48

Theory : reals

Home Index