---

Step * of Lemma qexp-positive-iff

∀n:ℕ. ∀r:ℚ.  (0 < r ↑ n ⇐⇒ (n = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n))))
BY
{ (InstLemma `qexp-sign` [] THEN RepeatFor 2 (ParallelLast') THEN SplitAndHyps THEN (RWO "-3" 0 THENA Auto) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}r:\mBbbQ{}.    (0  <  r  \muparrow{}  n  \mLeftarrow{}{}\mRightarrow{}  (n  =  0)  \mvee{}  0  <  r  \mvee{}  (r  <  0  \mwedge{}  (\muparrow{}isEven(n))))


By

---

Latex:
(InstLemma  `qexp-sign`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  SplitAndHyps
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  Auto)

---

Home Index