Nuprl Lemma : raise-left-endpoint-rless

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

Proof

Definitions occuring in Statement :  raise-left-endpoint: `raise-left-endpoint(a;b;n)` rless: `x < y` real: `ℝ` nat_plus: `ℕ+` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ 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: `b supposing a` prop: `ℙ` implies: `P `` Q` uall: `∀[x:A]. B[x]` cand: `A c∧ B` raise-left-endpoint: `raise-left-endpoint(a;b;n)` int_nzero: `ℤ-o` nat_plus: `ℕ+` nequal: `a ≠ b ∈ T ` 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 ⊆r B` guard: `{T}` rneq: `x ≠ y` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` decidable: `Dec(P)` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` rdiv: `(x/y)`
Lemmas referenced :  real_wf req_weakening radd-int req_inversion rmul_functionality radd_functionality req_functionality equal_wf int-to-real_wf rmul_wf radd_wf rmul-distrib2 rmul-identity1 radd-assoc req_transitivity radd_comm rmul_comm rmul-one-both 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 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_var_lemma req-iff-rsub-is-0 real_term_value_add_lemma rmul-rinv3 radd-preserves-rless 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 sqequalRule independent_pairFormation dependent_set_memberEquality setElimination rename dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality computeAll baseApply closedConclusion baseClosed applyEquality inrFormation unionElimination

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

Date html generated: 2017_10_03-AM-09_32_25
Last ObjectModification: 2017_07_28-AM-07_50_46

Theory : reals

Home Index