---

Step * 2 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 : ℚ
⊢ (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
{ ((InstLemma `exp_unroll_q` [⌜n⌝;⌜r⌝]⋅ THENA Auto)
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN (InstHyp [⌜r⌝] (-3)⋅ THENA Auto)
   THEN SplitAndConcl
   THEN (SplitAndHyps
         THEN ((RWW "qmul-positive2< qmul-negative< qmul-zero -3 -2 -1" 0 THENA Auto)
               THEN (RepeatFor 2 (D 0) THENA Auto)
               THEN Repeat ((SplitOrHyps THEN ExRepD))
               THEN Auto
               THEN (AllHyps (\h.FLemma `even-implies` [h])⋅ THEN AllHyps (\h.FLemma `odd-implies` [h])⋅)
               THEN Auto
               THEN Try ((RelRST THEN Auto))
               THEN Auto)⋅
         )⋅)⋅ }

1
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)

---

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{}
\mvdash{}  (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:
((InstLemma  `exp\_unroll\_q`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}r\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  SplitAndConcl
  THEN  (SplitAndHyps
              THEN  ((RWW  "qmul-positive2<  qmul-negative<  qmul-zero  -3  -2  -1"  0  THENA  Auto)
                          THEN  (RepeatFor  2  (D  0)  THENA  Auto)
                          THEN  Repeat  ((SplitOrHyps  THEN  ExRepD))
                          THEN  Auto
                          THEN  (AllHyps  (\mbackslash{}h.FLemma  `even-implies`  [h])\mcdot{}
                                      THEN  AllHyps  (\mbackslash{}h.FLemma  `odd-implies`  [h])\mcdot{}
                                      )
                          THEN  Auto
                          THEN  Try  ((RelRST  THEN  Auto))
                          THEN  Auto)\mcdot{}
              )\mcdot{})\mcdot{}

---

Home Index