Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(β€β₯β(π + 1)) =
(β€β₯β(π + 1)) |
2 | | clim2ser.2 |
. . . . 5
β’ (π β π β π) |
3 | | clim2ser.1 |
. . . . 5
β’ π =
(β€β₯βπ) |
4 | 2, 3 | eleqtrdi 2844 |
. . . 4
β’ (π β π β (β€β₯βπ)) |
5 | | peano2uz 12831 |
. . . 4
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β (π + 1) β
(β€β₯βπ)) |
7 | | eluzelz 12778 |
. . 3
β’ ((π + 1) β
(β€β₯βπ) β (π + 1) β β€) |
8 | 6, 7 | syl 17 |
. 2
β’ (π β (π + 1) β β€) |
9 | | clim2ser2.5 |
. 2
β’ (π β seq(π + 1)( + , πΉ) β π΄) |
10 | | eluzel2 12773 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
11 | 4, 10 | syl 17 |
. . . 4
β’ (π β π β β€) |
12 | | clim2ser.4 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
13 | 3, 11, 12 | serf 13942 |
. . 3
β’ (π β seqπ( + , πΉ):πβΆβ) |
14 | 13, 2 | ffvelcdmd 7037 |
. 2
β’ (π β (seqπ( + , πΉ)βπ) β β) |
15 | | seqex 13914 |
. . 3
β’ seqπ( + , πΉ) β V |
16 | 15 | a1i 11 |
. 2
β’ (π β seqπ( + , πΉ) β V) |
17 | 6, 3 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β (π + 1) β π) |
18 | 3 | uztrn2 12787 |
. . . . . 6
β’ (((π + 1) β π β§ π β (β€β₯β(π + 1))) β π β π) |
19 | 17, 18 | sylan 581 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π + 1))) β π β π) |
20 | 19, 12 | syldan 592 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β (πΉβπ) β β) |
21 | 1, 8, 20 | serf 13942 |
. . 3
β’ (π β seq(π + 1)( + , πΉ):(β€β₯β(π +
1))βΆβ) |
22 | 21 | ffvelcdmda 7036 |
. 2
β’ ((π β§ π β (β€β₯β(π + 1))) β (seq(π + 1)( + , πΉ)βπ) β β) |
23 | 14 | adantr 482 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) β β) |
24 | | addcl 11138 |
. . . . 5
β’ ((π β β β§ π₯ β β) β (π + π₯) β β) |
25 | 24 | adantl 483 |
. . . 4
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β)) β (π + π₯) β β) |
26 | | addass 11143 |
. . . . 5
β’ ((π β β β§ π₯ β β β§ π¦ β β) β ((π + π₯) + π¦) = (π + (π₯ + π¦))) |
27 | 26 | adantl 483 |
. . . 4
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β β§ π¦ β β)) β ((π + π₯) + π¦) = (π + (π₯ + π¦))) |
28 | | simpr 486 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
29 | 4 | adantr 482 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β π β (β€β₯βπ)) |
30 | | elfzuz 13443 |
. . . . . . 7
β’ (π β (π...π) β π β (β€β₯βπ)) |
31 | 30, 3 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β (π...π) β π β π) |
32 | 31, 12 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
33 | 32 | adantlr 714 |
. . . 4
β’ (((π β§ π β (β€β₯β(π + 1))) β§ π β (π...π)) β (πΉβπ) β β) |
34 | 25, 27, 28, 29, 33 | seqsplit 13947 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ))) |
35 | 23, 22, 34 | comraddd 11374 |
. 2
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seq(π + 1)( + , πΉ)βπ) + (seqπ( + , πΉ)βπ))) |
36 | 1, 8, 9, 14, 16, 22, 35 | climaddc1 15523 |
1
β’ (π β seqπ( + , πΉ) β (π΄ + (seqπ( + , πΉ)βπ))) |