Nuprl Lemma : rnexp-convex2

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


Proof




Definitions occuring in Statement :  rleq: x ≤ y rabs: |x| rnexp: x^k1 rsub: y int-to-real: r(n) real: nat_plus: + all: x:A. B[x] implies:  Q natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q prop: subtype_rel: A ⊆B uimplies: supposing a uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y guard: {T}
Lemmas referenced :  rnexp-convex rmax_wf rmin_wf rmin_ub int-to-real_wf rmin-rleq-rmax nat_plus_wf rleq_wf real_wf rnexp_wf nat_plus_subtype_nat rsub_wf rabs_wf rleq_weakening_equal rleq_functionality rnexp_functionality req_inversion rmax-minus-rmin req_weakening rleq_functionality_wrt_implies rsub_functionality rmax-rnexp rmin-rnexp
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality hypothesis independent_functionElimination natural_numberEquality productElimination independent_pairFormation applyEquality sqequalRule because_Cache independent_isectElimination equalityTransitivity equalitySymmetry

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



Date html generated: 2016_05_18-AM-09_30_09
Last ObjectModification: 2015_12_27-PM-11_20_29

Theory : reals


Home Index