Nuprl Lemma : rless_functionality_wrt_implies

a,b,c,d:ℝ.  ({(b < c)  (a < d)}) supposing ((c ≤ d) and (b ≥ a))


Definitions occuring in Statement :  rge: x ≥ y rleq: x ≤ y rless: x < y real: uimplies: supposing a guard: {T} all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  guard: {T} all: x:A. B[x] uimplies: supposing a member: t ∈ T rge: x ≥ y rleq: x ≤ y rnonneg: rnonneg(x) le: A ≤ B and: P ∧ Q not: ¬A implies:  Q false: False uall: [x:A]. B[x] subtype_rel: A ⊆B real: prop:
Lemmas referenced :  less_than'_wf rsub_wf real_wf nat_plus_wf rless_transitivity2 rless_transitivity1 rless_wf rleq_wf rge_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation isect_memberFormation cut introduction sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality voidElimination lemma_by_obid isectElimination applyEquality hypothesis setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry because_Cache independent_isectElimination independent_functionElimination

\mforall{}a,b,c,d:\mBbbR{}.    (\{(b  <  c)  {}\mRightarrow{}  (a  <  d)\})  supposing  ((c  \mleq{}  d)  and  (b  \mgeq{}  a))

Date html generated: 2016_05_18-AM-07_06_10
Last ObjectModification: 2015_12_28-AM-00_37_13

Theory : reals

Home Index