---

Step * of Lemma all-even-implies-sum-even

No Annotations
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  ↑isEven(Σ(f[x] | x < n)) supposing ∀x:ℕn. (↑isEven(f[x]))
BY
{ (Auto
   THEN (RWO "isEven-sum" 0 THEN Auto)
   THEN RWO "filter_is_nil" 0
   THEN Auto
   THEN Reduce 0
   THEN RWO "l_all_iff" 0
   THEN Auto
   THEN D -3 With ⌜x⌝ 
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    \muparrow{}isEven(\mSigma{}(f[x]  |  x  <  n))  supposing  \mforall{}x:\mBbbN{}n.  (\muparrow{}isEven(f[x]))


By

---

Latex:
(Auto
  THEN  (RWO  "isEven-sum"  0  THEN  Auto)
  THEN  RWO  "filter\_is\_nil"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  RWO  "l\_all\_iff"  0
  THEN  Auto
  THEN  D  -3  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  EAuto  1)

---

Home Index