Step | Hyp | Ref
| Expression |
1 | | eqid 2725 |
. 2
β’
(β€β₯β(π + 1)) =
(β€β₯β(π + 1)) |
2 | | clim2ser.2 |
. . . . 5
β’ (π β π β π) |
3 | | clim2ser.1 |
. . . . 5
β’ π =
(β€β₯βπ) |
4 | 2, 3 | eleqtrdi 2835 |
. . . 4
β’ (π β π β (β€β₯βπ)) |
5 | | peano2uz 12915 |
. . . 4
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β (π + 1) β
(β€β₯βπ)) |
7 | | eluzelz 12862 |
. . 3
β’ ((π + 1) β
(β€β₯βπ) β (π + 1) β β€) |
8 | 6, 7 | syl 17 |
. 2
β’ (π β (π + 1) β β€) |
9 | | clim2ser2.5 |
. 2
β’ (π β seq(π + 1)( + , πΉ) β π΄) |
10 | | eluzel2 12857 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
11 | 4, 10 | syl 17 |
. . . 4
β’ (π β π β β€) |
12 | | clim2ser.4 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
13 | 3, 11, 12 | serf 14027 |
. . 3
β’ (π β seqπ( + , πΉ):πβΆβ) |
14 | 13, 2 | ffvelcdmd 7090 |
. 2
β’ (π β (seqπ( + , πΉ)βπ) β β) |
15 | | seqex 14000 |
. . 3
β’ seqπ( + , πΉ) β V |
16 | 15 | a1i 11 |
. 2
β’ (π β seqπ( + , πΉ) β V) |
17 | 6, 3 | eleqtrrdi 2836 |
. . . . . 6
β’ (π β (π + 1) β π) |
18 | 3 | uztrn2 12871 |
. . . . . 6
β’ (((π + 1) β π β§ π β (β€β₯β(π + 1))) β π β π) |
19 | 17, 18 | sylan 578 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π + 1))) β π β π) |
20 | 19, 12 | syldan 589 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β (πΉβπ) β β) |
21 | 1, 8, 20 | serf 14027 |
. . 3
β’ (π β seq(π + 1)( + , πΉ):(β€β₯β(π +
1))βΆβ) |
22 | 21 | ffvelcdmda 7089 |
. 2
β’ ((π β§ π β (β€β₯β(π + 1))) β (seq(π + 1)( + , πΉ)βπ) β β) |
23 | 14 | adantr 479 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) β β) |
24 | | addcl 11220 |
. . . . 5
β’ ((π β β β§ π₯ β β) β (π + π₯) β β) |
25 | 24 | adantl 480 |
. . . 4
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β)) β (π + π₯) β β) |
26 | | addass 11225 |
. . . . 5
β’ ((π β β β§ π₯ β β β§ π¦ β β) β ((π + π₯) + π¦) = (π + (π₯ + π¦))) |
27 | 26 | adantl 480 |
. . . 4
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β β§ π¦ β β)) β ((π + π₯) + π¦) = (π + (π₯ + π¦))) |
28 | | simpr 483 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
29 | 4 | adantr 479 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β π β (β€β₯βπ)) |
30 | | elfzuz 13529 |
. . . . . . 7
β’ (π β (π...π) β π β (β€β₯βπ)) |
31 | 30, 3 | eleqtrrdi 2836 |
. . . . . 6
β’ (π β (π...π) β π β π) |
32 | 31, 12 | sylan2 591 |
. . . . 5
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
33 | 32 | adantlr 713 |
. . . 4
β’ (((π β§ π β (β€β₯β(π + 1))) β§ π β (π...π)) β (πΉβπ) β β) |
34 | 25, 27, 28, 29, 33 | seqsplit 14032 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ))) |
35 | 23, 22, 34 | comraddd 11458 |
. 2
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seq(π + 1)( + , πΉ)βπ) + (seqπ( + , πΉ)βπ))) |
36 | 1, 8, 9, 14, 16, 22, 35 | climaddc1 15611 |
1
β’ (π β seqπ( + , πΉ) β (π΄ + (seqπ( + , πΉ)βπ))) |