---

Step * 1 of Lemma qexp-sign


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 ∈ ℤ)))
BY
{ ((Subst ⌜r ↑ 0 = 1 ∈ ℚ⌝ 0⋅ THENA (Auto THEN BLemma `qexp-zero` THEN Auto))
   THEN RepUR ``isEven isOdd modulus`` 0⋅
   THEN Auto
   THEN OnMaybeHyp 5 (\h. ((RWO "int-equal-in-rationals" h THENA Auto) THEN Complete (Auto')))) }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
\mvdash{}  (0  <  r  \muparrow{}  0  \mLeftarrow{}{}\mRightarrow{}  (0  =  0)  \mvee{}  0  <  r  \mvee{}  (r  <  0  \mwedge{}  (\muparrow{}isEven(0))))
\mwedge{}  (r  \muparrow{}  0  <  0  \mLeftarrow{}{}\mRightarrow{}  r  <  0  \mwedge{}  (\muparrow{}isOdd(0)))
\mwedge{}  (r  \muparrow{}  0  =  0  \mLeftarrow{}{}\mRightarrow{}  (r  =  0)  \mwedge{}  (\mneg{}(0  =  0)))


By

---

Latex:
((Subst  \mkleeneopen{}r  \muparrow{}  0  =  1\mkleeneclose{}  0\mcdot{}  THENA  (Auto  THEN  BLemma  `qexp-zero`  THEN  Auto))
  THEN  RepUR  ``isEven  isOdd  modulus``  0\mcdot{}
  THEN  Auto
  THEN  OnMaybeHyp  5  (\mbackslash{}h.  ((RWO  "int-equal-in-rationals"  h  THENA  Auto)  THEN  Complete  (Auto'))))

---

Home Index