### Nuprl Lemma : rmul_preserves_rneq

`∀a,b,x:ℝ.  (x ≠ r0 `` a ≠ b `` x * a ≠ x * b)`

Proof

Definitions occuring in Statement :  rneq: `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` rneq: `x ≠ y` or: `P ∨ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` guard: `{T}` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)`
Lemmas referenced :  rneq_wf int-to-real_wf real_wf rmul_preserves_rless rless_wf rmul_wf rless-implies-rless real_term_polynomial itermSubtract_wf itermMultiply_wf itermVar_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 rless_functionality req_transitivity itermConstant_wf rmul_functionality rmul-identity1 req_weakening rmul_reverses_rless rmul_comm
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution unionElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis natural_numberEquality lemma_by_obid inrFormation sqequalRule productElimination independent_isectElimination independent_functionElimination because_Cache dependent_functionElimination inlFormation computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}a,b,x:\mBbbR{}.    (x  \mneq{}  r0  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  x  *  a  \mneq{}  x  *  b)

Date html generated: 2017_10_03-AM-08_28_32
Last ObjectModification: 2017_07_28-AM-07_25_18

Theory : reals

Home Index