---

Step * of Lemma rpower-nonzero

∀x:ℝ. (x ≠ r0 ⇒ (∀n:ℕ. x^n ≠ r0))
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto) }

1
.....upcase..... 
1. x : ℝ
2. x ≠ r0
3. n : ℤ
4. [%2] : 0 < n
5. x^n - 1 ≠ r0
⊢ x^n ≠ r0

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  x\^{}n  \mneq{}  r0))


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Auto)

---

Home Index