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 ⊢ Ⅎ 𝑘 𝐹
Assertion esumfzf ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑁 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 esumfzf.1 ⊢ Ⅎ 𝑘 𝐹
2 nfv ⊢ Ⅎ 𝑘 𝑖 = 1
3 oveq2 ⊢ ( 𝑖 = 1 → ( 1 ... 𝑖 ) = ( 1 ... 1 ) )
4 2 3 esumeq1d ⊢ ( 𝑖 = 1 → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑘 ) )
5 fveq2 ⊢ ( 𝑖 = 1 → ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 1 ) )
6 4 5 eqeq12d ⊢ ( 𝑖 = 1 → ( Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ↔ Σ* 𝑘 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 1 ) ) )
7 6 imbi2d ⊢ ( 𝑖 = 1 → ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ) ↔ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 1 ) ) ) )
8 nfv ⊢ Ⅎ 𝑘 𝑖 = 𝑛
9 oveq2 ⊢ ( 𝑖 = 𝑛 → ( 1 ... 𝑖 ) = ( 1 ... 𝑛 ) )
10 8 9 esumeq1d ⊢ ( 𝑖 = 𝑛 → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) )
11 fveq2 ⊢ ( 𝑖 = 𝑛 → ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) )
12 10 11 eqeq12d ⊢ ( 𝑖 = 𝑛 → ( Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ↔ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) )
13 12 imbi2d ⊢ ( 𝑖 = 𝑛 → ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ) ↔ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) ) )
14 nfv ⊢ Ⅎ 𝑘 𝑖 = ( 𝑛 + 1 )
15 oveq2 ⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( 1 ... 𝑖 ) = ( 1 ... ( 𝑛 + 1 ) ) )
16 14 15 esumeq1d ⊢ ( 𝑖 = ( 𝑛 + 1 ) → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) )
17 fveq2 ⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
18 16 17 eqeq12d ⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ↔ Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
19 18 imbi2d ⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ) ↔ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
20 nfv ⊢ Ⅎ 𝑘 𝑖 = 𝑁
21 oveq2 ⊢ ( 𝑖 = 𝑁 → ( 1 ... 𝑖 ) = ( 1 ... 𝑁 ) )
22 20 21 esumeq1d ⊢ ( 𝑖 = 𝑁 → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) )
23 fveq2 ⊢ ( 𝑖 = 𝑁 → ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑁 ) )
24 22 23 eqeq12d ⊢ ( 𝑖 = 𝑁 → ( Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ↔ Σ* 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑁 ) ) )
25 24 imbi2d ⊢ ( 𝑖 = 𝑁 → ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑖 ) ) ↔ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑁 ) ) ) )
26 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑥 ) )
27 nfcv ⊢ Ⅎ 𝑥 { 1 }
28 nfcv ⊢ Ⅎ 𝑘 { 1 }
29 nfcv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑘 )
30 nfcv ⊢ Ⅎ 𝑘 𝑥
31 1 30 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑥 )
32 26 27 28 29 31 cbvesum ⊢ Σ* 𝑘 ∈ { 1 } ( 𝐹 ‘ 𝑘 ) = Σ* 𝑥 ∈ { 1 } ( 𝐹 ‘ 𝑥 )
33 simpr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 1 ) → 𝑥 = 1 )
34 33 fveq2d ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 1 ) )
35 1z ⊢ 1 ∈ ℤ
36 35 a1i ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → 1 ∈ ℤ )
37 1nn ⊢ 1 ∈ ℕ
38 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 1 ∈ ℕ ) → ( 𝐹 ‘ 1 ) ∈ ( 0 [,] +∞ ) )
39 37 38 mpan2 ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝐹 ‘ 1 ) ∈ ( 0 [,] +∞ ) )
40 34 36 39 esumsn ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑥 ∈ { 1 } ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 1 ) )
41 32 40 syl5eq ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ { 1 } ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 1 ) )
42 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
43 35 42 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
44 esumeq1 ⊢ ( ( 1 ... 1 ) = { 1 } → Σ* 𝑘 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ { 1 } ( 𝐹 ‘ 𝑘 ) )
45 43 44 ax-mp ⊢ Σ* 𝑘 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ { 1 } ( 𝐹 ‘ 𝑘 )
46 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( +𝑒 , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
47 35 46 ax-mp ⊢ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 )
48 41 45 47 3eqtr4g ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 1 ) )
49 simpl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → 𝑛 ∈ ℕ )
50 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
51 49 50 eleqtrdi ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
52 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
53 51 52 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
54 53 adantr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) → ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
55 simpr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) )
56 55 oveq1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
57 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ ℕ
58 57 nfci ⊢ Ⅎ 𝑘 ℕ
59 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
60 1 58 59 nff ⊢ Ⅎ 𝑘 𝐹 : ℕ ⟶ ( 0 [,] +∞ )
61 57 60 nfan ⊢ Ⅎ 𝑘 ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
62 fzsuc ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
63 51 62 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
64 61 63 esumeq1d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = Σ* 𝑘 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ( 𝐹 ‘ 𝑘 ) )
65 nfcv ⊢ Ⅎ 𝑘 ( 1 ... 𝑛 )
66 nfcv ⊢ Ⅎ 𝑘 { ( 𝑛 + 1 ) }
67 ovexd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( 1 ... 𝑛 ) ∈ V )
68 snex ⊢ { ( 𝑛 + 1 ) } ∈ V
69 68 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → { ( 𝑛 + 1 ) } ∈ V )
70 fzp1disj ⊢ ( ( 1 ... 𝑛 ) ∩ { ( 𝑛 + 1 ) } ) = ∅
71 70 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( ( 1 ... 𝑛 ) ∩ { ( 𝑛 + 1 ) } ) = ∅ )
72 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
73 fzssnn ⊢ ( 1 ∈ ℕ → ( 1 ... 𝑛 ) ⊆ ℕ )
74 37 73 ax-mp ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
75 simpr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ( 1 ... 𝑛 ) )
76 74 75 sseldi ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
77 72 76 ffvelrnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
78 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
79 simpr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → 𝑘 ∈ { ( 𝑛 + 1 ) } )
80 velsn ⊢ ( 𝑘 ∈ { ( 𝑛 + 1 ) } ↔ 𝑘 = ( 𝑛 + 1 ) )
81 79 80 sylib ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → 𝑘 = ( 𝑛 + 1 ) )
82 simpll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → 𝑛 ∈ ℕ )
83 82 peano2nnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → ( 𝑛 + 1 ) ∈ ℕ )
84 81 83 eqeltrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → 𝑘 ∈ ℕ )
85 78 84 ffvelrnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ { ( 𝑛 + 1 ) } ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
86 61 65 66 67 69 71 77 85 esumsplit ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ( 𝐹 ‘ 𝑘 ) = ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) +𝑒 Σ* 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝐹 ‘ 𝑘 ) ) )
87 nfcv ⊢ Ⅎ 𝑥 { ( 𝑛 + 1 ) }
88 26 87 66 29 31 cbvesum ⊢ Σ* 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝐹 ‘ 𝑘 ) = Σ* 𝑥 ∈ { ( 𝑛 + 1 ) } ( 𝐹 ‘ 𝑥 )
89 simpr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = ( 𝑛 + 1 ) ) → 𝑥 = ( 𝑛 + 1 ) )
90 89 fveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = ( 𝑛 + 1 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
91 49 peano2nnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( 𝑛 + 1 ) ∈ ℕ )
92 simpr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
93 92 91 ffvelrnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,] +∞ ) )
94 90 91 93 esumsn ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → Σ* 𝑥 ∈ { ( 𝑛 + 1 ) } ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
95 88 94 syl5eq ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
96 95 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) +𝑒 Σ* 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝐹 ‘ 𝑘 ) ) = ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
97 64 86 96 3eqtrrd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) )
98 97 adantr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) +𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) )
99 54 56 98 3eqtr2rd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
100 99 exp31 ⊢ ( 𝑛 ∈ ℕ → ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
101 100 a2d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ) → ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
102 7 13 19 25 48 101 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑁 ) ) )
103 102 impcom ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑁 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑁 ) )