Nuprl Lemma : i-member-convex3

I:Interval. ∀a,b:ℝ.  ((a ∈ I)  (b ∈ I)  (∀n:ℕ+. ∀i:ℕ.  (((i 1) n ∈ ℤ ((i b)/n ∈ I))))


Proof




Definitions occuring in Statement :  i-member: r ∈ I interval: Interval int-rdiv: (a)/k1 int-rmul: k1 a radd: b real: nat_plus: + nat: all: x:A. B[x] implies:  Q add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T implies:  Q nat: uall: [x:A]. B[x] nat_plus: + ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: false: False subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q and: P ∧ Q
Lemmas referenced :  i-member-convex2 nat_properties nat_plus_properties decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le int-rmul-one set_subtype_base le_wf int_subtype_base less_than_wf istype-nat nat_plus_wf i-member_wf real_wf interval_wf int-rdiv_wf nat_plus_inc_int_nzero radd_wf int-rmul_wf i-member_functionality int-rdiv_functionality radd_functionality req_weakening
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination dependent_set_memberEquality_alt natural_numberEquality isectElimination setElimination rename unionElimination independent_isectElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt isect_memberEquality_alt voidElimination sqequalRule universeIsType equalityIstype baseApply closedConclusion baseClosed applyEquality intEquality sqequalBase equalitySymmetry inhabitedIsType because_Cache equalityTransitivity productElimination

Latex:
\mforall{}I:Interval.  \mforall{}a,b:\mBbbR{}.    ((a  \mmember{}  I)  {}\mRightarrow{}  (b  \mmember{}  I)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}i:\mBbbN{}.    (((i  +  1)  =  n)  {}\mRightarrow{}  ((i  *  a  +  b)/n  \mmember{}  I))))



Date html generated: 2019_10_29-AM-10_47_28
Last ObjectModification: 2019_01_08-PM-10_02_52

Theory : reals


Home Index