---

Step * 2 1 1 1 2 1 of Lemma qexp-minus-one


1. n : ℤ
2. 0 < n
3. -1 ↑ n - 1 = if (n - 1 rem 2 =z 0) then 1 else -1 fi  ∈ ℚ
4. ((n - 1 rem 2) + 1 rem 2) = ((n - 1) + 1 rem 2) ∈ ℤ
5. 0 ≤ (n rem 2)
6. n rem 2 < 2
7. 0 ≤ (n - 1 rem 2)
8. n - 1 rem 2 < 2
9. ¬((n - 1 rem 2) = 0 ∈ ℤ)
10. (n - 1 rem 2) = 1 ∈ ℤ
⊢ (n rem 2) = 0 ∈ ℤ
BY
{ xxxOnMaybeHyp 5 (\h. (Assert ⌜(n - 1 rem 2) = 1 ∈ ℤ⌝⋅
                        THEN Auto
                        THEN HypSubst' (-1) h⋅
                        THEN Reduce h
                        THEN Complete (Auto))⋅)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  -1  \muparrow{}  n  -  1  =  if  (n  -  1  rem  2  =\msubz{}  0)  then  1  else  -1  fi 
4.  ((n  -  1  rem  2)  +  1  rem  2)  =  ((n  -  1)  +  1  rem  2)
5.  0  \mleq{}  (n  rem  2)
6.  n  rem  2  <  2
7.  0  \mleq{}  (n  -  1  rem  2)
8.  n  -  1  rem  2  <  2
9.  \mneg{}((n  -  1  rem  2)  =  0)
10.  (n  -  1  rem  2)  =  1
\mvdash{}  (n  rem  2)  =  0


By

---

Latex:
xxxOnMaybeHyp  5  (\mbackslash{}h.  (Assert  \mkleeneopen{}(n  -  1  rem  2)  =  1\mkleeneclose{}\mcdot{}
                                            THEN  Auto
                                            THEN  HypSubst'  (-1)  h\mcdot{}
                                            THEN  Reduce  h
                                            THEN  Complete  (Auto))\mcdot{})xxx

---

Home Index