Nuprl Lemma : rless_transitivity2

x,y,z:ℝ.  (y < z)  (x < z) supposing x ≤ y


Proof




Definitions occuring in Statement :  rleq: x ≤ y rless: x < y real: uimplies: supposing a all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T 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: iff: ⇐⇒ Q nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True rev_implies:  Q exists: x:A. B[x] int_upper: {i...} guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top uiff: uiff(P;Q)
Lemmas referenced :  false_wf int_term_value_subtract_lemma int_term_value_constant_lemma int_term_value_add_lemma int_formula_prop_less_lemma itermSubtract_wf itermConstant_wf itermAdd_wf intformless_wf subtract-is-int-iff add-is-int-iff decidable__lt int_formula_prop_wf int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_plus_properties int_upper_properties rleq_wf rless_wf all_wf int_upper_wf less_than_transitivity1 rless-iff4 rleq-iff4 less_than_wf rless-iff-large-diff nat_plus_wf real_wf rsub_wf less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality voidElimination lemma_by_obid isectElimination applyEquality hypothesis setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry independent_functionElimination dependent_set_memberEquality independent_pairFormation imageMemberEquality baseClosed dependent_pairFormation independent_isectElimination addEquality because_Cache unionElimination int_eqEquality intEquality isect_memberEquality voidEquality computeAll pointwiseFunctionality promote_hyp baseApply closedConclusion

Latex:
\mforall{}x,y,z:\mBbbR{}.    (y  <  z)  {}\mRightarrow{}  (x  <  z)  supposing  x  \mleq{}  y



Date html generated: 2016_05_18-AM-07_05_43
Last ObjectModification: 2016_01_17-AM-01_51_35

Theory : reals


Home Index