---

Step * 1 1 1 1 of Lemma mod2-add1


1. n : ℤ
2. (n + 1) = ((((n + 1) ÷↓ 2) * 2) + ((n + 1) mod 2)) ∈ ℤ
3. n = (((n ÷↓ 2) * 2) + (n mod 2)) ∈ ℤ
⊢ ((n + 1) mod 2) = ((2 * ((n ÷↓ 2) - (n + 1) ÷↓ 2)) + (n mod 2) + 1) ∈ ℤ
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜((n + 1) ÷↓ 2) = a ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(n ÷↓ 2) = b ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜((n + 1) mod 2) = c ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(n mod 2) = d ∈ ℤ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. n : ℤ
2. a : ℤ
3. b : ℤ
4. c : ℤ
5. d : ℤ
6. (n + 1) = ((a * 2) + c) ∈ ℤ
7. n = ((b * 2) + d) ∈ ℤ
⊢ c = ((2 * (b - a)) + d + 1) ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  (n  +  1)  =  ((((n  +  1)  \mdiv{}\mdownarrow{}  2)  *  2)  +  ((n  +  1)  mod  2))
3.  n  =  (((n  \mdiv{}\mdownarrow{}  2)  *  2)  +  (n  mod  2))
\mvdash{}  ((n  +  1)  mod  2)  =  ((2  *  ((n  \mdiv{}\mdownarrow{}  2)  -  (n  +  1)  \mdiv{}\mdownarrow{}  2))  +  (n  mod  2)  +  1)


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}((n  +  1)  \mdiv{}\mdownarrow{}  2)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(n  \mdiv{}\mdownarrow{}  2)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((n  +  1)  mod  2)  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(n  mod  2)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index