Nuprl Lemma : rnexp_functionality_wrt_rleq
∀x,y:ℝ. ((r0 ≤ x) ⇒ (x ≤ y) ⇒ (∀n:ℕ. (x^n ≤ y^n)))
Proof
Definitions occuring in Statement :
rleq: x ≤ y,
rnexp: x^k1,
int-to-real: r(n),
real: ℝ,
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Lemmas referenced :
rnexp-rleq
Rules used in proof :
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}x,y:\mBbbR{}. ((r0 \mleq{} x) {}\mRightarrow{} (x \mleq{} y) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (x\^{}n \mleq{} y\^{}n)))
Date html generated:
2016_10_26-AM-09_08_44
Last ObjectModification:
2016_10_13-PM-06_43_08
Theory : reals
Home
Index