---

Step * of Lemma qexp-qabs

∀[a:ℚ]. ∀[n:ℕ].  (|a| ↑ n = |a ↑ n| ∈ ℚ)
BY
{ xxx(InductionOnNat THEN (RWW "qexp-zero" 0 THENA Auto))xxx }

1
1. a : ℚ
2. n : ℤ
⊢ 1 = |1| ∈ ℚ

2
.....upcase..... 
1. a : ℚ
2. n : ℤ
3. 0 < n
4. |a| ↑ n - 1 = |a ↑ n - 1| ∈ ℚ
⊢ |a| ↑ n = |a ↑ n| ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (|a|  \muparrow{}  n  =  |a  \muparrow{}  n|)


By

---

Latex:
xxx(InductionOnNat  THEN  (RWW  "qexp-zero"  0  THENA  Auto))xxx

---

Home Index