---

Step * of Lemma qexp-minus-one

∀[n:ℕ]. (-1 ↑ n = if (n rem 2 =z 0) then 1 else -1 fi  ∈ ℚ)
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ -1 ↑ 0 = if (0 rem 2 =z 0) then 1 else -1 fi  ∈ ℚ

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. -1 ↑ n - 1 = if (n - 1 rem 2 =z 0) then 1 else -1 fi  ∈ ℚ
⊢ -1 ↑ n = if (n rem 2 =z 0) then 1 else -1 fi  ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (-1  \muparrow{}  n  =  if  (n  rem  2  =\msubz{}  0)  then  1  else  -1  fi  )


By

---

Latex:
InductionOnNat

---

Home Index