---

Step * 2 of Lemma qexp-qabs

.....upcase..... 
1. a : ℚ
2. n : ℤ
3. 0 < n
4. |a| ↑ n - 1 = |a ↑ n - 1| ∈ ℚ
⊢ |a| ↑ n = |a ↑ n| ∈ ℚ
BY
{ (RWO "exp_unroll_q" 0 THEN Auto THEN RWO "qabs-qmul" 0 THEN Auto) }

---

Latex:

---

Latex:
.....upcase..... 
1.  a  :  \mBbbQ{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  |a|  \muparrow{}  n  -  1  =  |a  \muparrow{}  n  -  1|
\mvdash{}  |a|  \muparrow{}  n  =  |a  \muparrow{}  n|


By

---

Latex:
(RWO  "exp\_unroll\_q"  0  THEN  Auto  THEN  RWO  "qabs-qmul"  0  THEN  Auto)

---

Home Index