### Nuprl Lemma : rnexp-even-nonneg

`∀n:ℕ. (((n rem 2) = 0 ∈ ℤ) `` (∀x:ℝ. (r0 ≤ x^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` remainder: `n rem m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` guard: `{T}` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` and: `P ∧ Q` uiff: `uiff(P;Q)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` prop: `ℙ` false: `False` not: `¬A` nequal: `a ≠ b ∈ T ` true: `True` int_nzero: `ℤ-o` le: `A ≤ B` less_than': `less_than'(a;b)` nat_plus: `ℕ+` rev_uimplies: `rev_uimplies(P;Q)`

Latex:
\mforall{}n:\mBbbN{}.  (((n  rem  2)  =  0)  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (r0  \mleq{}  x\^{}n)))

Date html generated: 2020_05_20-AM-10_59_13
Last ObjectModification: 2020_01_03-AM-11_17_33

Theory : reals

Home Index