---

Step * 1 1 of Lemma mod2-add1


1. n : ℤ
⊢ ∃k:ℤ. (((n + 1) mod 2) = ((2 * k) + (n mod 2) + 1) ∈ ℤ)
BY
{ ((InstLemma `div_floor_mod_sum` [⌜n + 1⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `div_floor_mod_sum` [⌜n⌝;⌜2⌝]⋅ THENA Auto)
   ) }

1
1. n : ℤ
2. (n + 1) = ((((n + 1) ÷↓ 2) * 2) + ((n + 1) mod 2)) ∈ ℤ
3. n = (((n ÷↓ 2) * 2) + (n mod 2)) ∈ ℤ
⊢ ∃k:ℤ. (((n + 1) mod 2) = ((2 * k) + (n mod 2) + 1) ∈ ℤ)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
\mvdash{}  \mexists{}k:\mBbbZ{}.  (((n  +  1)  mod  2)  =  ((2  *  k)  +  (n  mod  2)  +  1))


By

---

Latex:
((InstLemma  `div\_floor\_mod\_sum`  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_floor\_mod\_sum`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index