Nuprl Lemma : regular-less

[x,y:ℝ].  ∀n:ℕ+((x n) 4 <  (∀m:ℕ+((x m) ≤ ((y m) 4))))


Proof




Definitions occuring in Statement :  real: nat_plus: + less_than: a < b uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] implies:  Q apply: a add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q real: uimplies: supposing a and: P ∧ Q cand: c∧ B nat_plus: + sq_stable: SqStable(P) regular-int-seq: k-regular-seq(f) squash: T le: A ≤ B prop: decidable: Dec(P) or: P ∨ Q less_than: a < b false: False uiff: uiff(P;Q) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A top: Top subtype_rel: A ⊆B sq_type: SQType(T) guard: {T} ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q rev_implies:  Q bfalse: ff
Lemmas referenced :  assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_lt_int eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases int_term_value_minus_lemma itermMinus_wf minus-is-int-iff not_wf bnot_wf assert_wf subtract-is-int-iff int_subtype_base lt_int_wf real_wf less_than'_wf nat_plus_wf false_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_mul_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermSubtract_wf itermConstant_wf itermAdd_wf itermVar_wf itermMultiply_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt multiply-is-int-iff add-is-int-iff less_than_wf decidable__le nat_plus_properties absval_ifthenelse subtract_wf sq_stable__le mul_cancel_in_le mul_preserves_lt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin addEquality applyEquality setElimination rename hypothesisEquality natural_numberEquality independent_isectElimination hypothesis multiplyEquality independent_functionElimination dependent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination independent_pairFormation because_Cache productElimination dependent_set_memberEquality unionElimination pointwiseFunctionality equalityTransitivity equalitySymmetry promote_hyp baseApply closedConclusion dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll independent_pairEquality axiomEquality instantiate cumulativity impliesFunctionality

Latex:
\mforall{}[x,y:\mBbbR{}].    \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  +  4  <  y  n  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}.  ((x  m)  \mleq{}  ((y  m)  +  4))))



Date html generated: 2016_05_18-AM-06_47_40
Last ObjectModification: 2016_01_17-AM-01_46_47

Theory : reals


Home Index