---

Step * 1 of Lemma lsum-of-even


1. T : Type
2. u : T
3. v : T List
4. ∀[f:{x:T| (x ∈ v)}  ⟶ ℤ]. ↑isEven(Σ(f[x] | x ∈ v)) supposing (∀x∈v.↑isEven(f[x]))
5. f : {x:T| (x ∈ [u / v])}  ⟶ ℤ
6. ↑isEven(f[u])
7. (∀x∈v.↑isEven(f[x]))
8. ↑isEven(Σ(f[x] | x ∈ v))
9. ∀[P:{x:T| (x ∈ [u / v])}  ⟶ ℙ]
     ∀x:{x:T| (x ∈ [u / v])} . ∀L:{x:T| (x ∈ [u / v])}  List.  ((∀y∈[x / L].P[y]) ⇐⇒ P[x] ∧ (∀y∈L.P[y]))
⊢ ↑isEven(f[u] + Σ(f[x] | x ∈ v))
BY
{ ((RWO "isEven-add" 0 THEN Auto) THEN Unfold `same-parity` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[f:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbZ{}].  \muparrow{}isEven(\mSigma{}(f[x]  |  x  \mmember{}  v))  supposing  (\mforall{}x\mmember{}v.\muparrow{}isEven(f[x]))
5.  f  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbZ{}
6.  \muparrow{}isEven(f[u])
7.  (\mforall{}x\mmember{}v.\muparrow{}isEven(f[x]))
8.  \muparrow{}isEven(\mSigma{}(f[x]  |  x  \mmember{}  v))
9.  \mforall{}[P:\{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbP{}]
          \mforall{}x:\{x:T|  (x  \mmember{}  [u  /  v])\}  .  \mforall{}L:\{x:T|  (x  \mmember{}  [u  /  v])\}    List.
              ((\mforall{}y\mmember{}[x  /  L].P[y])  \mLeftarrow{}{}\mRightarrow{}  P[x]  \mwedge{}  (\mforall{}y\mmember{}L.P[y]))
\mvdash{}  \muparrow{}isEven(f[u]  +  \mSigma{}(f[x]  |  x  \mmember{}  v))


By

---

Latex:
((RWO  "isEven-add"  0  THEN  Auto)  THEN  Unfold  `same-parity`  0  THEN  AutoSplit)

---

Home Index