---

Step * of Lemma qexp-sign

∀n:ℕ. ∀r:ℚ.
  ((0 < r ↑ n ⇐⇒ (n = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n))))
  ∧ (r ↑ n < 0 ⇐⇒ r < 0 ∧ (↑isOdd(n)))
  ∧ (r ↑ n = 0 ∈ ℚ ⇐⇒ (r = 0 ∈ ℚ) ∧ (¬(n = 0 ∈ ℤ))))
BY
{ (InductionOnNat THEN (D 0 THENA Auto)) }

1
1. r : ℚ
⊢ (0 < r ↑ 0 ⇐⇒ (0 = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(0))))
∧ (r ↑ 0 < 0 ⇐⇒ r < 0 ∧ (↑isOdd(0)))
∧ (r ↑ 0 = 0 ∈ ℚ ⇐⇒ (r = 0 ∈ ℚ) ∧ (¬(0 = 0 ∈ ℤ)))

2
1. n : ℤ
2. [%1] : 0 < n
3. ∀r:ℚ
     ((0 < r ↑ n - 1 ⇐⇒ ((n - 1) = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n - 1))))
     ∧ (r ↑ n - 1 < 0 ⇐⇒ r < 0 ∧ (↑isOdd(n - 1)))
     ∧ (r ↑ n - 1 = 0 ∈ ℚ ⇐⇒ (r = 0 ∈ ℚ) ∧ (¬((n - 1) = 0 ∈ ℤ))))
4. r : ℚ
⊢ (0 < r ↑ n ⇐⇒ (n = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n))))
∧ (r ↑ n < 0 ⇐⇒ r < 0 ∧ (↑isOdd(n)))
∧ (r ↑ n = 0 ∈ ℚ ⇐⇒ (r = 0 ∈ ℚ) ∧ (¬(n = 0 ∈ ℤ)))

---

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))))
    \mwedge{}  (r  \muparrow{}  n  <  0  \mLeftarrow{}{}\mRightarrow{}  r  <  0  \mwedge{}  (\muparrow{}isOdd(n)))
    \mwedge{}  (r  \muparrow{}  n  =  0  \mLeftarrow{}{}\mRightarrow{}  (r  =  0)  \mwedge{}  (\mneg{}(n  =  0))))


By

---

Latex:
(InductionOnNat  THEN  (D  0  THENA  Auto))

---

Home Index