Nuprl Lemma : rmul_preserves_rleq2

[x,y,z:ℝ].  ((x y) ≤ (z y)) supposing ((x ≤ z) and (r0 ≤ y))


Definitions occuring in Statement :  rleq: x ≤ y rmul: b int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
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:
Lemmas referenced :  less_than'_wf rsub_wf rmul_wf real_wf nat_plus_wf rleq_wf int-to-real_wf rmul_functionality_wrt_rleq
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,z:\mBbbR{}].    ((x  *  y)  \mleq{}  (z  *  y))  supposing  ((x  \mleq{}  z)  and  (r0  \mleq{}  y))

Date html generated: 2016_05_18-AM-07_12_35
Last ObjectModification: 2015_12_28-AM-00_41_24

Theory : reals

Home Index