Nuprl Lemma : rsub_functionality_wrt_rleq

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


Definitions occuring in Statement :  rge: x ≥ y rleq: x ≤ y rsub: y real: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rsub: y 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) rge: x ≥ y guard: {T}
Lemmas referenced :  less_than'_wf rsub_wf real_wf nat_plus_wf rge_wf rleq_wf radd_wf rminus_wf uiff_transitivity radd-preserves-rleq rmul_wf int-to-real_wf rleq_functionality req_transitivity radd_functionality rminus-as-rmul req_weakening radd-assoc req_inversion rmul-identity1 rmul-distrib2 rmul_functionality radd-int rmul-zero-both radd-zero-both rminus-reverses-rleq rleq_functionality_wrt_implies radd_functionality_wrt_rleq rleq_weakening_equal
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_functionElimination independent_isectElimination addEquality

\mforall{}[x,y,z,t:\mBbbR{}].    ((x  -  y)  \mleq{}  (z  -  t))  supposing  ((y  \mgeq{}  t)  and  (x  \mleq{}  z))

Date html generated: 2016_05_18-AM-07_08_47
Last ObjectModification: 2015_12_28-AM-00_39_43

Theory : reals

Home Index