Nuprl Lemma : rabs-rmul-rleq-rabs

[x,y,a,b:ℝ].  (|x y| ≤ |a b|) supposing ((|y| ≤ |b|) and (|x| ≤ |a|))


Definitions occuring in Statement :  rleq: x ≤ y rabs: |x| rmul: b real: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rleq: x ≤ y rnonneg: rnonneg(x) all: x:A. B[x] le: A ≤ B and: P ∧ Q not: ¬A implies:  Q false: False subtype_rel: A ⊆B real: prop: uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  less_than'_wf rsub_wf rabs_wf rmul_wf real_wf nat_plus_wf rleq_wf rabs-rmul-rleq rleq_functionality req_weakening rabs-rmul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality because_Cache lemma_by_obid isectElimination applyEquality hypothesis setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination independent_isectElimination

\mforall{}[x,y,a,b:\mBbbR{}].    (|x  *  y|  \mleq{}  |a  *  b|)  supposing  ((|y|  \mleq{}  |b|)  and  (|x|  \mleq{}  |a|))

Date html generated: 2016_05_18-AM-07_14_45
Last ObjectModification: 2015_12_28-AM-00_42_23

Theory : reals

Home Index