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 | | clim2ser.5 |
. 2
β’ (π β seqπ( + , πΉ) β π΄) |
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(π + 1)( + , πΉ) β V |
16 | 15 | a1i 11 |
. 2
β’ (π β seq(π + 1)( + , πΉ) β V) |
17 | 13 | adantr 482 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β seqπ( + , πΉ):πβΆβ) |
18 | 6, 3 | eleqtrrdi 2845 |
. . . 4
β’ (π β (π + 1) β π) |
19 | 3 | uztrn2 12787 |
. . . 4
β’ (((π + 1) β π β§ π β (β€β₯β(π + 1))) β π β π) |
20 | 18, 19 | sylan 581 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β π β π) |
21 | 17, 20 | ffvelcdmd 7037 |
. 2
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) β β) |
22 | | addcl 11138 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β (π + π₯) β β) |
23 | 22 | adantl 483 |
. . . . 5
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β)) β (π + π₯) β β) |
24 | | addass 11143 |
. . . . . 6
β’ ((π β β β§ π₯ β β β§ π¦ β β) β ((π + π₯) + π¦) = (π + (π₯ + π¦))) |
25 | 24 | adantl 483 |
. . . . 5
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β β§ π¦ β β)) β ((π + π₯) + π¦) = (π + (π₯ + π¦))) |
26 | | simpr 486 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
27 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π + 1))) β π β (β€β₯βπ)) |
28 | | elfzuz 13443 |
. . . . . . . 8
β’ (π β (π...π) β π β (β€β₯βπ)) |
29 | 28, 3 | eleqtrrdi 2845 |
. . . . . . 7
β’ (π β (π...π) β π β π) |
30 | 29, 12 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
31 | 30 | adantlr 714 |
. . . . 5
β’ (((π β§ π β (β€β₯β(π + 1))) β§ π β (π...π)) β (πΉβπ) β β) |
32 | 23, 25, 26, 27, 31 | seqsplit 13947 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ))) |
33 | 32 | oveq1d 7373 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) = (((seqπ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ)) β (seqπ( + , πΉ)βπ))) |
34 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) β β) |
35 | 3 | uztrn2 12787 |
. . . . . . . 8
β’ (((π + 1) β π β§ π β (β€β₯β(π + 1))) β π β π) |
36 | 18, 35 | sylan 581 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(π + 1))) β π β π) |
37 | 36, 12 | syldan 592 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (πΉβπ) β β) |
38 | 1, 8, 37 | serf 13942 |
. . . . 5
β’ (π β seq(π + 1)( + , πΉ):(β€β₯β(π +
1))βΆβ) |
39 | 38 | ffvelcdmda 7036 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β (seq(π + 1)( + , πΉ)βπ) β β) |
40 | 34, 39 | pncan2d 11519 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (((seqπ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ)) β (seqπ( + , πΉ)βπ)) = (seq(π + 1)( + , πΉ)βπ)) |
41 | 33, 40 | eqtr2d 2774 |
. 2
β’ ((π β§ π β (β€β₯β(π + 1))) β (seq(π + 1)( + , πΉ)βπ) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) |
42 | 1, 8, 9, 14, 16, 21, 41 | climsubc1 15526 |
1
β’ (π β seq(π + 1)( + , πΉ) β (π΄ β (seqπ( + , πΉ)βπ))) |