---

Step * 2 1 2 of Lemma sum-has-value

.....upcase..... 
1. f : Base
2. d : ℤ
3. 0 < d
4. ∀n,m:ℕ.  (((n - m) ≤ (d - 1)) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))
⊢ ∀n,m:ℕ.  (((n - m) ≤ d) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))
BY
{ TACTIC:Auto }

1
1. f : Base
2. d : ℤ
3. 0 < d
4. ∀n,m:ℕ.  (((n - m) ≤ (d - 1)) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))
5. n : ℕ@i
6. m : ℕ@i
7. (n - m) ≤ d
8. v : ℤ@i
9. (sum_aux(n;v;m;x.f[x]))↓
⊢ f ∈ {m..n-} ⟶ ℤ

---

Latex:

---

Latex:
.....upcase..... 
1.  f  :  Base
2.  d  :  \mBbbZ{}
3.  0  <  d
4.  \mforall{}n,m:\mBbbN{}.    (((n  -  m)  \mleq{}  (d  -  1))  {}\mRightarrow{}  (\mforall{}v:\mBbbZ{}.  ((sum\_aux(n;v;m;x.f[x]))\mdownarrow{}  {}\mRightarrow{}  (f  \mmember{}  \{m..n\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}))))
\mvdash{}  \mforall{}n,m:\mBbbN{}.    (((n  -  m)  \mleq{}  d)  {}\mRightarrow{}  (\mforall{}v:\mBbbZ{}.  ((sum\_aux(n;v;m;x.f[x]))\mdownarrow{}  {}\mRightarrow{}  (f  \mmember{}  \{m..n\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}))))


By

---

Latex:
TACTIC:Auto

---

Home Index