Step * of Lemma sum_aux_wf

[v,i,k:ℤ]. ∀[f:{i..k-} ⟶ ℤ].  sum_aux(k;v;i;x.f[x]) ∈ ℤ supposing i ≤ k
BY
Assert ⌜∀d:ℕ. ∀[v,i:ℤ]. ∀[f:{i..i d-} ⟶ ℤ].  (sum_aux(i d;v;i;x.f[x]) ∈ ℤ)⌝⋅ }

1
.....assertion..... 
d:ℕ. ∀[v,i:ℤ]. ∀[f:{i..i d-} ⟶ ℤ].  (sum_aux(i d;v;i;x.f[x]) ∈ ℤ)

2
1. ∀d:ℕ. ∀[v,i:ℤ]. ∀[f:{i..i d-} ⟶ ℤ].  (sum_aux(i d;v;i;x.f[x]) ∈ ℤ)
⊢ ∀[v,i,k:ℤ]. ∀[f:{i..k-} ⟶ ℤ].  sum_aux(k;v;i;x.f[x]) ∈ ℤ supposing i ≤ k


Latex:


Latex:
\mforall{}[v,i,k:\mBbbZ{}].  \mforall{}[f:\{i..k\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].    sum\_aux(k;v;i;x.f[x])  \mmember{}  \mBbbZ{}  supposing  i  \mleq{}  k


By


Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}[v,i:\mBbbZ{}].  \mforall{}[f:\{i..i  +  d\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].    (sum\_aux(i  +  d;v;i;x.f[x])  \mmember{}  \mBbbZ{})\mkleeneclose{}\mcdot{}




Home Index