Nuprl Lemma : rmul-is-positive

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

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` or: `P ∨ Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)` or: `P ∨ Q` cand: `A c∧ B` guard: `{T}` rev_uimplies: `rev_uimplies(P;Q)` true: `True` less_than': `less_than'(a;b)` squash: `↓T` less_than: `a < b` rneq: `x ≠ y`
Lemmas referenced :  rless_wf int-to-real_wf rmul_wf or_wf real_wf rmul-is-negative rless-implies-rless 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 rsub_wf rmul-one-both rdiv-zero rmul-rdiv-cancel rmul-ac rmul_comm rmul_functionality rmul-assoc req_inversion req_functionality uiff_transitivity rmul-int-rdiv rmul-rdiv-cancel2 rmul-zero-both rless_functionality req_weakening req_wf rless-int rdiv_wf rmul_preserves_rless rminus-rminus req_transitivity rminus_functionality rmul_over_rminus rmul-minus rmul-int rmul_reverses_rless_iff rminus_wf rmul_reverses_rless equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesis hypothesisEquality productEquality dependent_functionElimination minusEquality independent_functionElimination because_Cache independent_isectElimination sqequalRule computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality productElimination unionElimination inlFormation inrFormation promote_hyp addLevel multiplyEquality baseClosed imageMemberEquality equalitySymmetry equalityTransitivity

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

Date html generated: 2017_10_03-AM-08_47_17
Last ObjectModification: 2017_07_28-AM-07_32_57

Theory : reals

Home Index