Step | Hyp | Ref
| Expression |
1 | | climfsum.8 |
. . . 4
β’ ((π β§ π β π) β (π»βπ) = Ξ£π β π΄ (πΉβπ)) |
2 | 1 | mpteq2dva 5210 |
. . 3
β’ (π β (π β π β¦ (π»βπ)) = (π β π β¦ Ξ£π β π΄ (πΉβπ))) |
3 | | climfsum.1 |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
4 | | uzssz 12791 |
. . . . . . . 8
β’
(β€β₯βπ) β β€ |
5 | 3, 4 | eqsstri 3983 |
. . . . . . 7
β’ π β
β€ |
6 | | zssre 12513 |
. . . . . . 7
β’ β€
β β |
7 | 5, 6 | sstri 3958 |
. . . . . 6
β’ π β
β |
8 | 7 | a1i 11 |
. . . . 5
β’ (π β π β β) |
9 | | climfsum.3 |
. . . . 5
β’ (π β π΄ β Fin) |
10 | | fvexd 6862 |
. . . . 5
β’ ((π β§ (π β π β§ π β π΄)) β (πΉβπ) β V) |
11 | | climfsum.5 |
. . . . . . 7
β’ ((π β§ π β π΄) β πΉ β π΅) |
12 | | climfsum.2 |
. . . . . . . . 9
β’ (π β π β β€) |
13 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π β β€) |
14 | | climrel 15381 |
. . . . . . . . . 10
β’ Rel
β |
15 | 14 | brrelex1i 5693 |
. . . . . . . . 9
β’ (πΉ β π΅ β πΉ β V) |
16 | 11, 15 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π΄) β πΉ β V) |
17 | | eqid 2737 |
. . . . . . . . 9
β’ (π β π β¦ (πΉβπ)) = (π β π β¦ (πΉβπ)) |
18 | 3, 17 | climmpt 15460 |
. . . . . . . 8
β’ ((π β β€ β§ πΉ β V) β (πΉ β π΅ β (π β π β¦ (πΉβπ)) β π΅)) |
19 | 13, 16, 18 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π΄) β (πΉ β π΅ β (π β π β¦ (πΉβπ)) β π΅)) |
20 | 11, 19 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β π΄) β (π β π β¦ (πΉβπ)) β π΅) |
21 | | climfsum.7 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π β π)) β (πΉβπ) β β) |
22 | 21 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π) β (πΉβπ) β β) |
23 | 22 | fmpttd 7068 |
. . . . . . 7
β’ ((π β§ π β π΄) β (π β π β¦ (πΉβπ)):πβΆβ) |
24 | 3, 13, 23 | rlimclim 15435 |
. . . . . 6
β’ ((π β§ π β π΄) β ((π β π β¦ (πΉβπ)) βπ π΅ β (π β π β¦ (πΉβπ)) β π΅)) |
25 | 20, 24 | mpbird 257 |
. . . . 5
β’ ((π β§ π β π΄) β (π β π β¦ (πΉβπ)) βπ π΅) |
26 | 8, 9, 10, 25 | fsumrlim 15703 |
. . . 4
β’ (π β (π β π β¦ Ξ£π β π΄ (πΉβπ)) βπ Ξ£π β π΄ π΅) |
27 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π΄ β Fin) |
28 | 21 | anass1rs 654 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π΄) β (πΉβπ) β β) |
29 | 27, 28 | fsumcl 15625 |
. . . . . 6
β’ ((π β§ π β π) β Ξ£π β π΄ (πΉβπ) β β) |
30 | 29 | fmpttd 7068 |
. . . . 5
β’ (π β (π β π β¦ Ξ£π β π΄ (πΉβπ)):πβΆβ) |
31 | 3, 12, 30 | rlimclim 15435 |
. . . 4
β’ (π β ((π β π β¦ Ξ£π β π΄ (πΉβπ)) βπ Ξ£π β π΄ π΅ β (π β π β¦ Ξ£π β π΄ (πΉβπ)) β Ξ£π β π΄ π΅)) |
32 | 26, 31 | mpbid 231 |
. . 3
β’ (π β (π β π β¦ Ξ£π β π΄ (πΉβπ)) β Ξ£π β π΄ π΅) |
33 | 2, 32 | eqbrtrd 5132 |
. 2
β’ (π β (π β π β¦ (π»βπ)) β Ξ£π β π΄ π΅) |
34 | | climfsum.6 |
. . 3
β’ (π β π» β π) |
35 | | eqid 2737 |
. . . 4
β’ (π β π β¦ (π»βπ)) = (π β π β¦ (π»βπ)) |
36 | 3, 35 | climmpt 15460 |
. . 3
β’ ((π β β€ β§ π» β π) β (π» β Ξ£π β π΄ π΅ β (π β π β¦ (π»βπ)) β Ξ£π β π΄ π΅)) |
37 | 12, 34, 36 | syl2anc 585 |
. 2
β’ (π β (π» β Ξ£π β π΄ π΅ β (π β π β¦ (π»βπ)) β Ξ£π β π΄ π΅)) |
38 | 33, 37 | mpbird 257 |
1
β’ (π β π» β Ξ£π β π΄ π΅) |