Step | Hyp | Ref
| Expression |
1 | | isumadd.1 |
. 2
β’ π =
(β€β₯βπ) |
2 | | isumadd.2 |
. 2
β’ (π β π β β€) |
3 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
4 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (πΊβπ) = (πΊβπ)) |
5 | 3, 4 | oveq12d 7376 |
. . . . 5
β’ (π = π β ((πΉβπ) + (πΊβπ)) = ((πΉβπ) + (πΊβπ))) |
6 | | eqid 2733 |
. . . . 5
β’ (π β π β¦ ((πΉβπ) + (πΊβπ))) = (π β π β¦ ((πΉβπ) + (πΊβπ))) |
7 | | ovex 7391 |
. . . . 5
β’ ((πΉβπ) + (πΊβπ)) β V |
8 | 5, 6, 7 | fvmpt 6949 |
. . . 4
β’ (π β π β ((π β π β¦ ((πΉβπ) + (πΊβπ)))βπ) = ((πΉβπ) + (πΊβπ))) |
9 | 8 | adantl 483 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) + (πΊβπ)))βπ) = ((πΉβπ) + (πΊβπ))) |
10 | | isumadd.3 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
11 | | isumadd.5 |
. . . 4
β’ ((π β§ π β π) β (πΊβπ) = π΅) |
12 | 10, 11 | oveq12d 7376 |
. . 3
β’ ((π β§ π β π) β ((πΉβπ) + (πΊβπ)) = (π΄ + π΅)) |
13 | 9, 12 | eqtrd 2773 |
. 2
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) + (πΊβπ)))βπ) = (π΄ + π΅)) |
14 | | isumadd.4 |
. . 3
β’ ((π β§ π β π) β π΄ β β) |
15 | | isumadd.6 |
. . 3
β’ ((π β§ π β π) β π΅ β β) |
16 | 14, 15 | addcld 11179 |
. 2
β’ ((π β§ π β π) β (π΄ + π΅) β β) |
17 | | isumadd.7 |
. . . 4
β’ (π β seqπ( + , πΉ) β dom β ) |
18 | 1, 2, 10, 14, 17 | isumclim2 15648 |
. . 3
β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) |
19 | | seqex 13914 |
. . . 4
β’ seqπ( + , (π β π β¦ ((πΉβπ) + (πΊβπ)))) β V |
20 | 19 | a1i 11 |
. . 3
β’ (π β seqπ( + , (π β π β¦ ((πΉβπ) + (πΊβπ)))) β V) |
21 | | isumadd.8 |
. . . 4
β’ (π β seqπ( + , πΊ) β dom β ) |
22 | 1, 2, 11, 15, 21 | isumclim2 15648 |
. . 3
β’ (π β seqπ( + , πΊ) β Ξ£π β π π΅) |
23 | 10, 14 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
24 | 1, 2, 23 | serf 13942 |
. . . 4
β’ (π β seqπ( + , πΉ):πβΆβ) |
25 | 24 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
26 | 11, 15 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) β β) |
27 | 1, 2, 26 | serf 13942 |
. . . 4
β’ (π β seqπ( + , πΊ):πβΆβ) |
28 | 27 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΊ)βπ) β β) |
29 | | simpr 486 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
30 | 29, 1 | eleqtrdi 2844 |
. . . 4
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
31 | | simpll 766 |
. . . . 5
β’ (((π β§ π β π) β§ π β (π...π)) β π) |
32 | | elfzuz 13443 |
. . . . . . 7
β’ (π β (π...π) β π β (β€β₯βπ)) |
33 | 32, 1 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β (π...π) β π β π) |
34 | 33 | adantl 483 |
. . . . 5
β’ (((π β§ π β π) β§ π β (π...π)) β π β π) |
35 | 31, 34, 23 | syl2anc 585 |
. . . 4
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) β β) |
36 | 31, 34, 26 | syl2anc 585 |
. . . 4
β’ (((π β§ π β π) β§ π β (π...π)) β (πΊβπ) β β) |
37 | 34, 8 | syl 17 |
. . . 4
β’ (((π β§ π β π) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ) + (πΊβπ)))βπ) = ((πΉβπ) + (πΊβπ))) |
38 | 30, 35, 36, 37 | seradd 13956 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , (π β π β¦ ((πΉβπ) + (πΊβπ))))βπ) = ((seqπ( + , πΉ)βπ) + (seqπ( + , πΊ)βπ))) |
39 | 1, 2, 18, 20, 22, 25, 28, 38 | climadd 15520 |
. 2
β’ (π β seqπ( + , (π β π β¦ ((πΉβπ) + (πΊβπ)))) β (Ξ£π β π π΄ + Ξ£π β π π΅)) |
40 | 1, 2, 13, 16, 39 | isumclim 15647 |
1
β’ (π β Ξ£π β π (π΄ + π΅) = (Ξ£π β π π΄ + Ξ£π β π π΅)) |