### Nuprl Lemma : rnexp-convex3

`∀a,b:ℝ.  ((((r0 ≤ a) ∧ (r0 ≤ b)) ∨ ((a ≤ r0) ∧ (b ≤ r0))) `` (∀n:ℕ+. (|a - b|^n ≤ |a^n - b^n|)))`

Proof

Definitions occuring in Statement :  rleq: `x ≤ y` rabs: `|x|` rnexp: `x^k1` rsub: `x - y` int-to-real: `r(n)` real: `ℝ` nat_plus: `ℕ+` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)` prop: `ℙ` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` absval: `|i|`
Lemmas referenced :  rnexp-convex2 rminus_wf rleq-implies-rleq int-to-real_wf real_term_polynomial itermSubtract_wf itermConstant_wf itermVar_wf itermMinus_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma real_term_value_minus_lemma req-iff-rsub-is-0 rsub_wf nat_plus_wf or_wf rleq_wf real_wf req_wf squash_wf true_wf rabs-rminus rabs_wf iff_weakening_equal radd_wf req_weakening rnexp_wf nat_plus_subtype_nat req_functionality rabs_functionality itermAdd_wf real_term_value_add_lemma rleq_functionality rnexp_functionality rleq_functionality_wrt_implies rleq_weakening_equal rmul_wf exp_wf2 absval_wf uiff_transitivity rsub_functionality rminus-as-rmul req_transitivity rnexp-rmul req_inversion rmul-rsub-distrib rabs-rmul rmul_functionality rabs-rnexp nat_wf rabs-int rnexp-int rleq_weakening itermMultiply_wf real_term_value_mul_lemma exp-one
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution unionElimination thin productElimination cut introduction extract_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis isectElimination natural_numberEquality because_Cache independent_isectElimination sqequalRule computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality productEquality applyEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed universeEquality minusEquality callbyvalueReduce sqleReflexivity

Latex:
\mforall{}a,b:\mBbbR{}.    ((((r0  \mleq{}  a)  \mwedge{}  (r0  \mleq{}  b))  \mvee{}  ((a  \mleq{}  r0)  \mwedge{}  (b  \mleq{}  r0)))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  (|a  -  b|\^{}n  \mleq{}  |a\^{}n  -  b\^{}n|)))

Date html generated: 2017_10_03-AM-10_36_39
Last ObjectModification: 2017_07_28-AM-08_14_08

Theory : reals

Home Index