Nuprl Lemma : raise-lower-endpoints-rless

a,b:ℝ. ∀n:ℕ+.  ((a < b)  (raise-left-endpoint(a;b;n) < lower-right-endpoint(a;b;n)))


Proof




Definitions occuring in Statement :  raise-left-endpoint: raise-left-endpoint(a;b;n) lower-right-endpoint: lower-right-endpoint(a;b;n) rless: x < y real: nat_plus: + all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  member: t ∈ T all: x:A. B[x] rev_uimplies: rev_uimplies(P;Q) and: P ∧ Q uiff: uiff(P;Q) uimplies: supposing a prop: implies:  Q uall: [x:A]. B[x] lower-right-endpoint: lower-right-endpoint(a;b;n) raise-left-endpoint: raise-left-endpoint(a;b;n) int_nzero: -o nat_plus: + nequal: a ≠ b ∈  rless: x < y sq_exists: x:{A| B[x]} not: ¬A false: False satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top subtype_rel: A ⊆B guard: {T} rneq: x ≠ y or: P ∨ Q iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P) rdiv: (x/y) itermConstant: "const" req_int_terms: t1 ≡ t2
Lemmas referenced :  real_wf radd-int req_inversion rmul_functionality req_weakening req_functionality equal_wf int-to-real_wf rmul_wf radd_wf radd_comm rmul_comm rmul-one-both radd_functionality rmul-distrib uiff_transitivity req_wf rless_wf nat_plus_wf int-rdiv_wf nat_plus_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermAdd_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf equal-wf-base int_subtype_base equal-wf-T-base nequal_wf int-rmul_wf rdiv_wf rless-int decidable__lt intformnot_wf int_formula_prop_not_lemma rmul_preserves_rless rinv_wf2 rless_functionality int-rdiv-req rdiv_functionality int-rmul-req req_transitivity real_term_polynomial itermSubtract_wf itermMultiply_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_add_lemma real_term_value_var_lemma req-iff-rsub-is-0 rmul-rinv3 rless-implies-rless rsub_wf
Rules used in proof :  cut hypothesis extract_by_obid introduction intEquality lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination independent_isectElimination independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity because_Cache natural_numberEquality addEquality hypothesisEquality thin isectElimination sqequalHypSubstitution dependent_set_memberEquality setElimination rename dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll baseApply closedConclusion baseClosed applyEquality inrFormation unionElimination

Latex:
\mforall{}a,b:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    ((a  <  b)  {}\mRightarrow{}  (raise-left-endpoint(a;b;n)  <  lower-right-endpoint(a;b;n)))



Date html generated: 2017_10_03-AM-09_32_38
Last ObjectModification: 2017_07_28-AM-07_50_57

Theory : reals


Home Index