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