---

Step * 2 1 of Lemma qexp-sign


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 : ℚ
5. r ↑ n = (r ↑ n - 1 * r) ∈ ℚ
6. 0 < r ↑ n - 1 ⇒ (((n - 1) = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n - 1))))
7. 0 < r ↑ n - 1 ⇐ ((n - 1) = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n - 1)))
8. r ↑ n - 1 < 0 ⇒ (r < 0 ∧ (↑isOdd(n - 1)))
9. r ↑ n - 1 < 0 ⇐ r < 0 ∧ (↑isOdd(n - 1))
10. (r ↑ n - 1 = 0 ∈ ℚ) ⇒ ((r = 0 ∈ ℚ) ∧ (¬((n - 1) = 0 ∈ ℤ)))
11. (r ↑ n - 1 = 0 ∈ ℚ) ⇐ (r = 0 ∈ ℚ) ∧ (¬((n - 1) = 0 ∈ ℤ))
12. (n - 1) = 0 ∈ ℤ
13. r < 0
14. r < 0
⊢ ↑isOdd(n)
BY
{ (Subst ⌜n ~ 1⌝ 0⋅ THEN Auto THEN RepUR ``isEven isOdd modulus`` 0⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  [\%1]  :  0  <  n
3.  \mforall{}r:\mBbbQ{}
          ((0  <  r  \muparrow{}  n  -  1  \mLeftarrow{}{}\mRightarrow{}  ((n  -  1)  =  0)  \mvee{}  0  <  r  \mvee{}  (r  <  0  \mwedge{}  (\muparrow{}isEven(n  -  1))))
          \mwedge{}  (r  \muparrow{}  n  -  1  <  0  \mLeftarrow{}{}\mRightarrow{}  r  <  0  \mwedge{}  (\muparrow{}isOdd(n  -  1)))
          \mwedge{}  (r  \muparrow{}  n  -  1  =  0  \mLeftarrow{}{}\mRightarrow{}  (r  =  0)  \mwedge{}  (\mneg{}((n  -  1)  =  0))))
4.  r  :  \mBbbQ{}
5.  r  \muparrow{}  n  =  (r  \muparrow{}  n  -  1  *  r)
6.  0  <  r  \muparrow{}  n  -  1  {}\mRightarrow{}  (((n  -  1)  =  0)  \mvee{}  0  <  r  \mvee{}  (r  <  0  \mwedge{}  (\muparrow{}isEven(n  -  1))))
7.  0  <  r  \muparrow{}  n  -  1  \mLeftarrow{}{}  ((n  -  1)  =  0)  \mvee{}  0  <  r  \mvee{}  (r  <  0  \mwedge{}  (\muparrow{}isEven(n  -  1)))
8.  r  \muparrow{}  n  -  1  <  0  {}\mRightarrow{}  (r  <  0  \mwedge{}  (\muparrow{}isOdd(n  -  1)))
9.  r  \muparrow{}  n  -  1  <  0  \mLeftarrow{}{}  r  <  0  \mwedge{}  (\muparrow{}isOdd(n  -  1))
10.  (r  \muparrow{}  n  -  1  =  0)  {}\mRightarrow{}  ((r  =  0)  \mwedge{}  (\mneg{}((n  -  1)  =  0)))
11.  (r  \muparrow{}  n  -  1  =  0)  \mLeftarrow{}{}  (r  =  0)  \mwedge{}  (\mneg{}((n  -  1)  =  0))
12.  (n  -  1)  =  0
13.  r  <  0
14.  r  <  0
\mvdash{}  \muparrow{}isOdd(n)


By

---

Latex:
(Subst  \mkleeneopen{}n  \msim{}  1\mkleeneclose{}  0\mcdot{}  THEN  Auto  THEN  RepUR  ``isEven  isOdd  modulus``  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index