---

Step * of Lemma rnexp-even-nonneg

No Annotations
∀n:ℕ. (((n rem 2) = 0 ∈ ℤ) ⇒ (∀x:ℝ. (r0 ≤ x^n)))
BY
{ (Auto THEN Subst' n ~ 2 * (n ÷ 2) 0 THEN Auto) }

1
1. n : ℕ
2. (n rem 2) = 0 ∈ ℤ
3. x : ℝ
⊢ n = (2 * (n ÷ 2)) ∈ ℕ

2
1. n : ℕ
2. (n rem 2) = 0 ∈ ℤ
3. x : ℝ
⊢ r0 ≤ x^2 * (n ÷ 2)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Subst'  n  \msim{}  2  *  (n  \mdiv{}  2)  0  THEN  Auto)

---

Home Index