Nuprl Lemma : rmul-is-negative

`∀x,y:ℝ.  (((x * y) < r0) `` ((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]` implies: `P `` Q` or: `P ∨ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` or: `P ∨ Q` rneq: `x ≠ y` prop: `ℙ` uall: `∀[x:A]. B[x]` guard: `{T}` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  req_transitivity rmul-one-both rdiv-zero rmul-int-rdiv rmul-rdiv-cancel rmul-ac rmul_comm rmul_functionality rmul-assoc req_inversion req_functionality uiff_transitivity rmul-rdiv-cancel2 rmul-zero-both rless_functionality req_weakening req_wf rless-int rdiv_wf rmul_preserves_rless real_wf rmul_wf int-to-real_wf rless_wf rmul-is-negative1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis unionElimination inlFormation isectElimination natural_numberEquality sqequalRule inrFormation independent_isectElimination because_Cache productElimination independent_pairFormation introduction imageMemberEquality baseClosed multiplyEquality addLevel promote_hyp

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

Date html generated: 2016_05_18-AM-07_32_56
Last ObjectModification: 2016_01_17-AM-02_01_28

Theory : reals

Home Index