Metamath Proof Explorer

Theorem esumfzf

Description: Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017)

Ref Expression
Hypothesis esumfzf.1 ⊢Ⅎ_kF
Assertion esumfzf ⊢F:ℕ⟶0+∞∧N∈ℕ→∑*k=1NF⁡k=seq1+𝑒F⁡N

Proof

Step Hyp Ref Expression
1 esumfzf.1 ⊢Ⅎ_kF
2 nfv ⊢Ⅎki=1
3 oveq2 ⊢i=1→1…i=1…1
4 2 3 esumeq1d ⊢i=1→∑*k=1iF⁡k=∑*k=11F⁡k
5 fveq2 ⊢i=1→seq1+𝑒F⁡i=seq1+𝑒F⁡1
6 4 5 eqeq12d ⊢i=1→∑*k=1iF⁡k=seq1+𝑒F⁡i↔∑*k=11F⁡k=seq1+𝑒F⁡1
7 6 imbi2d ⊢i=1→F:ℕ⟶0+∞→∑*k=1iF⁡k=seq1+𝑒F⁡i↔F:ℕ⟶0+∞→∑*k=11F⁡k=seq1+𝑒F⁡1
8 nfv ⊢Ⅎki=n
9 oveq2 ⊢i=n→1…i=1…n
10 8 9 esumeq1d ⊢i=n→∑*k=1iF⁡k=∑*k=1nF⁡k
11 fveq2 ⊢i=n→seq1+𝑒F⁡i=seq1+𝑒F⁡n
12 10 11 eqeq12d ⊢i=n→∑*k=1iF⁡k=seq1+𝑒F⁡i↔∑*k=1nF⁡k=seq1+𝑒F⁡n
13 12 imbi2d ⊢i=n→F:ℕ⟶0+∞→∑*k=1iF⁡k=seq1+𝑒F⁡i↔F:ℕ⟶0+∞→∑*k=1nF⁡k=seq1+𝑒F⁡n
14 nfv ⊢Ⅎki=n+1
15 oveq2 ⊢i=n+1→1…i=1…n+1
16 14 15 esumeq1d ⊢i=n+1→∑*k=1iF⁡k=∑*k=1n+1F⁡k
17 fveq2 ⊢i=n+1→seq1+𝑒F⁡i=seq1+𝑒F⁡n+1
18 16 17 eqeq12d ⊢i=n+1→∑*k=1iF⁡k=seq1+𝑒F⁡i↔∑*k=1n+1F⁡k=seq1+𝑒F⁡n+1
19 18 imbi2d ⊢i=n+1→F:ℕ⟶0+∞→∑*k=1iF⁡k=seq1+𝑒F⁡i↔F:ℕ⟶0+∞→∑*k=1n+1F⁡k=seq1+𝑒F⁡n+1
20 nfv ⊢Ⅎki=N
21 oveq2 ⊢i=N→1…i=1…N
22 20 21 esumeq1d ⊢i=N→∑*k=1iF⁡k=∑*k=1NF⁡k
23 fveq2 ⊢i=N→seq1+𝑒F⁡i=seq1+𝑒F⁡N
24 22 23 eqeq12d ⊢i=N→∑*k=1iF⁡k=seq1+𝑒F⁡i↔∑*k=1NF⁡k=seq1+𝑒F⁡N
25 24 imbi2d ⊢i=N→F:ℕ⟶0+∞→∑*k=1iF⁡k=seq1+𝑒F⁡i↔F:ℕ⟶0+∞→∑*k=1NF⁡k=seq1+𝑒F⁡N
26 fveq2 ⊢k=x→F⁡k=F⁡x
27 nfcv ⊢Ⅎ_x1
28 nfcv ⊢Ⅎ_k1
29 nfcv ⊢Ⅎ_xF⁡k
30 nfcv ⊢Ⅎ_kx
31 1 30 nffv ⊢Ⅎ_kF⁡x
32 26 27 28 29 31 cbvesum ⊢∑*k∈1F⁡k=∑*x∈1F⁡x
33 simpr ⊢F:ℕ⟶0+∞∧x=1→x=1
34 33 fveq2d ⊢F:ℕ⟶0+∞∧x=1→F⁡x=F⁡1
35 1z ⊢1∈ℤ
36 35 a1i ⊢F:ℕ⟶0+∞→1∈ℤ
37 1nn ⊢1∈ℕ
38 ffvelcdm ⊢F:ℕ⟶0+∞∧1∈ℕ→F⁡1∈0+∞
39 37 38 mpan2 ⊢F:ℕ⟶0+∞→F⁡1∈0+∞
40 34 36 39 esumsn ⊢F:ℕ⟶0+∞→∑*x∈1F⁡x=F⁡1
41 32 40 eqtrid ⊢F:ℕ⟶0+∞→∑*k∈1F⁡k=F⁡1
42 fzsn ⊢1∈ℤ→1…1=1
43 35 42 ax-mp ⊢1…1=1
44 esumeq1 ⊢1…1=1→∑*k=11F⁡k=∑*k∈1F⁡k
45 43 44 ax-mp ⊢∑*k=11F⁡k=∑*k∈1F⁡k
46 seq1 ⊢1∈ℤ→seq1+𝑒F⁡1=F⁡1
47 35 46 ax-mp ⊢seq1+𝑒F⁡1=F⁡1
48 41 45 47 3eqtr4g ⊢F:ℕ⟶0+∞→∑*k=11F⁡k=seq1+𝑒F⁡1
49 simpl ⊢n∈ℕ∧F:ℕ⟶0+∞→n∈ℕ
50 nnuz ⊢ℕ=ℤ≥1
51 49 50 eleqtrdi ⊢n∈ℕ∧F:ℕ⟶0+∞→n∈ℤ≥1
52 seqp1 ⊢n∈ℤ≥1→seq1+𝑒F⁡n+1=seq1+𝑒F⁡n+𝑒F⁡n+1
53 51 52 syl ⊢n∈ℕ∧F:ℕ⟶0+∞→seq1+𝑒F⁡n+1=seq1+𝑒F⁡n+𝑒F⁡n+1
54 53 adantr ⊢n∈ℕ∧F:ℕ⟶0+∞∧∑*k=1nF⁡k=seq1+𝑒F⁡n→seq1+𝑒F⁡n+1=seq1+𝑒F⁡n+𝑒F⁡n+1
55 simpr ⊢n∈ℕ∧F:ℕ⟶0+∞∧∑*k=1nF⁡k=seq1+𝑒F⁡n→∑*k=1nF⁡k=seq1+𝑒F⁡n
56 55 oveq1d ⊢n∈ℕ∧F:ℕ⟶0+∞∧∑*k=1nF⁡k=seq1+𝑒F⁡n→∑*k=1nF⁡k+𝑒F⁡n+1=seq1+𝑒F⁡n+𝑒F⁡n+1
57 nfv ⊢Ⅎkn∈ℕ
58 57 nfci ⊢Ⅎ_kℕ
59 nfcv ⊢Ⅎ_k0+∞
60 1 58 59 nff ⊢ℲkF:ℕ⟶0+∞
61 57 60 nfan ⊢Ⅎkn∈ℕ∧F:ℕ⟶0+∞
62 fzsuc ⊢n∈ℤ≥1→1…n+1=1…n∪n+1
63 51 62 syl ⊢n∈ℕ∧F:ℕ⟶0+∞→1…n+1=1…n∪n+1
64 61 63 esumeq1d ⊢n∈ℕ∧F:ℕ⟶0+∞→∑*k=1n+1F⁡k=∑*k∈1…n∪n+1F⁡k
65 nfcv ⊢Ⅎ_k1…n
66 nfcv ⊢Ⅎ_kn+1
67 ovexd ⊢n∈ℕ∧F:ℕ⟶0+∞→1…n∈V
68 snex ⊢n+1∈V
69 68 a1i ⊢n∈ℕ∧F:ℕ⟶0+∞→n+1∈V
70 fzp1disj ⊢1…n∩n+1=∅
71 70 a1i ⊢n∈ℕ∧F:ℕ⟶0+∞→1…n∩n+1=∅
72 simplr ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈1…n→F:ℕ⟶0+∞
73 fzssnn ⊢1∈ℕ→1…n⊆ℕ
74 37 73 ax-mp ⊢1…n⊆ℕ
75 simpr ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈1…n→k∈1…n
76 74 75 sselid ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈1…n→k∈ℕ
77 72 76 ffvelcdmd ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈1…n→F⁡k∈0+∞
78 simplr ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→F:ℕ⟶0+∞
79 simpr ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→k∈n+1
80 velsn ⊢k∈n+1↔k=n+1
81 79 80 sylib ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→k=n+1
82 simpll ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→n∈ℕ
83 82 peano2nnd ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→n+1∈ℕ
84 81 83 eqeltrd ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→k∈ℕ
85 78 84 ffvelcdmd ⊢n∈ℕ∧F:ℕ⟶0+∞∧k∈n+1→F⁡k∈0+∞
86 61 65 66 67 69 71 77 85 esumsplit ⊢n∈ℕ∧F:ℕ⟶0+∞→∑*k∈1…n∪n+1F⁡k=∑*k=1nF⁡k+𝑒∑*k∈n+1F⁡k
87 nfcv ⊢Ⅎ_xn+1
88 26 87 66 29 31 cbvesum ⊢∑*k∈n+1F⁡k=∑*x∈n+1F⁡x
89 simpr ⊢n∈ℕ∧F:ℕ⟶0+∞∧x=n+1→x=n+1
90 89 fveq2d ⊢n∈ℕ∧F:ℕ⟶0+∞∧x=n+1→F⁡x=F⁡n+1
91 49 peano2nnd ⊢n∈ℕ∧F:ℕ⟶0+∞→n+1∈ℕ
92 simpr ⊢n∈ℕ∧F:ℕ⟶0+∞→F:ℕ⟶0+∞
93 92 91 ffvelcdmd ⊢n∈ℕ∧F:ℕ⟶0+∞→F⁡n+1∈0+∞
94 90 91 93 esumsn ⊢n∈ℕ∧F:ℕ⟶0+∞→∑*x∈n+1F⁡x=F⁡n+1
95 88 94 eqtrid ⊢n∈ℕ∧F:ℕ⟶0+∞→∑*k∈n+1F⁡k=F⁡n+1
96 95 oveq2d ⊢n∈ℕ∧F:ℕ⟶0+∞→∑*k=1nF⁡k+𝑒∑*k∈n+1F⁡k=∑*k=1nF⁡k+𝑒F⁡n+1
97 64 86 96 3eqtrrd ⊢n∈ℕ∧F:ℕ⟶0+∞→∑*k=1nF⁡k+𝑒F⁡n+1=∑*k=1n+1F⁡k
98 97 adantr ⊢n∈ℕ∧F:ℕ⟶0+∞∧∑*k=1nF⁡k=seq1+𝑒F⁡n→∑*k=1nF⁡k+𝑒F⁡n+1=∑*k=1n+1F⁡k
99 54 56 98 3eqtr2rd ⊢n∈ℕ∧F:ℕ⟶0+∞∧∑*k=1nF⁡k=seq1+𝑒F⁡n→∑*k=1n+1F⁡k=seq1+𝑒F⁡n+1
100 99 exp31 ⊢n∈ℕ→F:ℕ⟶0+∞→∑*k=1nF⁡k=seq1+𝑒F⁡n→∑*k=1n+1F⁡k=seq1+𝑒F⁡n+1
101 100 a2d ⊢n∈ℕ→F:ℕ⟶0+∞→∑*k=1nF⁡k=seq1+𝑒F⁡n→F:ℕ⟶0+∞→∑*k=1n+1F⁡k=seq1+𝑒F⁡n+1
102 7 13 19 25 48 101 nnind ⊢N∈ℕ→F:ℕ⟶0+∞→∑*k=1NF⁡k=seq1+𝑒F⁡N
103 102 impcom ⊢F:ℕ⟶0+∞∧N∈ℕ→∑*k=1NF⁡k=seq1+𝑒F⁡N