Nuprl Lemma : exp-convex2

[a,b:ℤ]. ∀[c:ℕ]. ∀[n:ℕ+].  |a b| ≤ supposing (|a^n b^n| ≤ c^n) ∧ (0 ≤ ⇐⇒ 0 ≤ b)


Proof




Definitions occuring in Statement :  exp: i^n absval: |i| nat_plus: + nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B iff: ⇐⇒ Q and: P ∧ Q subtract: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q iff: ⇐⇒ Q le: A ≤ B not: ¬A implies:  Q false: False nat: subtype_rel: A ⊆B prop: rev_implies:  Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q nat_plus: + ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top squash: T true: True less_than: a < b less_than': less_than'(a;b) so_lambda: λ2x.t[x] so_apply: x[s] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b subtract: m
Lemmas referenced :  less_than'_wf absval_wf subtract_wf le_wf exp_wf2 nat_plus_subtype_nat iff_wf nat_plus_wf nat_wf decidable__le exp-convex nat_plus_properties nat_properties satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermMinus_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_minus_lemma int_term_value_var_lemma int_formula_prop_wf intformimplies_wf int_formual_prop_imp_lemma squash_wf true_wf eq_int_wf modulus_wf_int_mod less_than_wf subtype_rel_set int_mod_wf int-subtype-int_mod bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int exp-minus iff_weakening_equal absval_sym minus-minus minus-add minus-one-mul minus-one-mul-top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache extract_by_obid isectElimination setElimination rename hypothesis applyEquality axiomEquality equalityTransitivity equalitySymmetry productEquality natural_numberEquality isect_memberEquality intEquality voidElimination unionElimination independent_functionElimination dependent_set_memberEquality independent_isectElimination minusEquality dependent_pairFormation int_eqEquality voidEquality independent_pairFormation computeAll hyp_replacement imageElimination imageMemberEquality baseClosed lambdaFormation equalityElimination promote_hyp instantiate cumulativity equalityEquality addEquality

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[c:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    |a  -  b|  \mleq{}  c  supposing  (|a\^{}n  -  b\^{}n|  \mleq{}  c\^{}n)  \mwedge{}  (0  \mleq{}  a  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  b)



Date html generated: 2016_10_25-AM-10_59_36
Last ObjectModification: 2016_07_12-AM-07_06_49

Theory : general


Home Index