Nuprl Lemma : rless-implies-rless

a,b:ℝ.  ∀[c,d:ℝ].  (a < b) supposing ((c < d) and ((d c) (b a)))


Definitions occuring in Statement :  rless: x < y rsub: y req: y real: uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T implies:  Q sq_stable: SqStable(P) iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q squash: T prop: rsub: y guard: {T}
Lemmas referenced :  req_witness rsub_wf sq_stable__rless radd-preserves-rless rminus_wf radd-rminus-both rless_wf req_wf real_wf radd_wf int-to-real_wf rless_functionality req_weakening radd_comm req_inversion rless_transitivity1 rleq_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination rename dependent_functionElimination because_Cache productElimination sqequalRule imageMemberEquality baseClosed imageElimination natural_numberEquality independent_isectElimination

\mforall{}a,b:\mBbbR{}.    \mforall{}[c,d:\mBbbR{}].    (a  <  b)  supposing  ((c  <  d)  and  ((d  -  c)  =  (b  -  a)))

Date html generated: 2017_10_03-AM-08_25_32
Last ObjectModification: 2017_04_04-PM-02_18_41

Theory : reals

Home Index