Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . 3
β’
(β€β₯β(π + 1)) =
(β€β₯β(π + 1)) |
2 | | clim2div.2 |
. . . . 5
β’ (π β π β π) |
3 | | eluzelz 12836 |
. . . . . 6
β’ (π β
(β€β₯βπ) β π β β€) |
4 | | clim2div.1 |
. . . . . 6
β’ π =
(β€β₯βπ) |
5 | 3, 4 | eleq2s 2845 |
. . . . 5
β’ (π β π β π β β€) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (π β π β β€) |
7 | 6 | peano2zd 12673 |
. . 3
β’ (π β (π + 1) β β€) |
8 | | clim2div.4 |
. . 3
β’ (π β seqπ( Β· , πΉ) β π΄) |
9 | | eluzel2 12831 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β π β β€) |
10 | 9, 4 | eleq2s 2845 |
. . . . . . 7
β’ (π β π β π β β€) |
11 | 2, 10 | syl 17 |
. . . . . 6
β’ (π β π β β€) |
12 | | clim2div.3 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
13 | 4, 11, 12 | prodf 15839 |
. . . . 5
β’ (π β seqπ( Β· , πΉ):πβΆβ) |
14 | 13, 2 | ffvelcdmd 7081 |
. . . 4
β’ (π β (seqπ( Β· , πΉ)βπ) β β) |
15 | | clim2div.5 |
. . . 4
β’ (π β (seqπ( Β· , πΉ)βπ) β 0) |
16 | 14, 15 | reccld 11987 |
. . 3
β’ (π β (1 / (seqπ( Β· , πΉ)βπ)) β β) |
17 | | seqex 13974 |
. . . 4
β’ seq(π + 1)( Β· , πΉ) β V |
18 | 17 | a1i 11 |
. . 3
β’ (π β seq(π + 1)( Β· , πΉ) β V) |
19 | 2, 4 | eleqtrdi 2837 |
. . . . . . 7
β’ (π β π β (β€β₯βπ)) |
20 | | peano2uz 12889 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
21 | 19, 20 | syl 17 |
. . . . . 6
β’ (π β (π + 1) β
(β€β₯βπ)) |
22 | 21, 4 | eleqtrrdi 2838 |
. . . . 5
β’ (π β (π + 1) β π) |
23 | 4 | uztrn2 12845 |
. . . . 5
β’ (((π + 1) β π β§ π β (β€β₯β(π + 1))) β π β π) |
24 | 22, 23 | sylan 579 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β π β π) |
25 | 13 | ffvelcdmda 7080 |
. . . 4
β’ ((π β§ π β π) β (seqπ( Β· , πΉ)βπ) β β) |
26 | 24, 25 | syldan 590 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( Β· , πΉ)βπ) β β) |
27 | | mulcl 11196 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
28 | 27 | adantl 481 |
. . . . . . 7
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
29 | | mulass 11200 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β β§ π¦ β β) β ((π Β· π₯) Β· π¦) = (π Β· (π₯ Β· π¦))) |
30 | 29 | adantl 481 |
. . . . . . 7
β’ (((π β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π₯ β β β§ π¦ β β)) β ((π Β· π₯) Β· π¦) = (π Β· (π₯ Β· π¦))) |
31 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
32 | 19 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(π + 1))) β π β (β€β₯βπ)) |
33 | | elfzuz 13503 |
. . . . . . . . . 10
β’ (π β (π...π) β π β (β€β₯βπ)) |
34 | 33, 4 | eleqtrrdi 2838 |
. . . . . . . . 9
β’ (π β (π...π) β π β π) |
35 | 34, 12 | sylan2 592 |
. . . . . . . 8
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
36 | 35 | adantlr 712 |
. . . . . . 7
β’ (((π β§ π β (β€β₯β(π + 1))) β§ π β (π...π)) β (πΉβπ) β β) |
37 | 28, 30, 31, 32, 36 | seqsplit 14006 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( Β· , πΉ)βπ) = ((seqπ( Β· , πΉ)βπ) Β· (seq(π + 1)( Β· , πΉ)βπ))) |
38 | 37 | eqcomd 2732 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π + 1))) β ((seqπ( Β· , πΉ)βπ) Β· (seq(π + 1)( Β· , πΉ)βπ)) = (seqπ( Β· , πΉ)βπ)) |
39 | 14 | adantr 480 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( Β· , πΉ)βπ) β β) |
40 | 4 | uztrn2 12845 |
. . . . . . . . . 10
β’ (((π + 1) β π β§ π β (β€β₯β(π + 1))) β π β π) |
41 | 22, 40 | sylan 579 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯β(π + 1))) β π β π) |
42 | 41, 12 | syldan 590 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + 1))) β (πΉβπ) β β) |
43 | 1, 7, 42 | prodf 15839 |
. . . . . . 7
β’ (π β seq(π + 1)( Β· , πΉ):(β€β₯β(π +
1))βΆβ) |
44 | 43 | ffvelcdmda 7080 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (seq(π + 1)( Β· , πΉ)βπ) β β) |
45 | 15 | adantr 480 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (seqπ( Β· , πΉ)βπ) β 0) |
46 | 26, 39, 44, 45 | divmuld 12016 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π + 1))) β (((seqπ( Β· , πΉ)βπ) / (seqπ( Β· , πΉ)βπ)) = (seq(π + 1)( Β· , πΉ)βπ) β ((seqπ( Β· , πΉ)βπ) Β· (seq(π + 1)( Β· , πΉ)βπ)) = (seqπ( Β· , πΉ)βπ))) |
47 | 38, 46 | mpbird 257 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β ((seqπ( Β· , πΉ)βπ) / (seqπ( Β· , πΉ)βπ)) = (seq(π + 1)( Β· , πΉ)βπ)) |
48 | 26, 39, 45 | divrec2d 11998 |
. . . 4
β’ ((π β§ π β (β€β₯β(π + 1))) β ((seqπ( Β· , πΉ)βπ) / (seqπ( Β· , πΉ)βπ)) = ((1 / (seqπ( Β· , πΉ)βπ)) Β· (seqπ( Β· , πΉ)βπ))) |
49 | 47, 48 | eqtr3d 2768 |
. . 3
β’ ((π β§ π β (β€β₯β(π + 1))) β (seq(π + 1)( Β· , πΉ)βπ) = ((1 / (seqπ( Β· , πΉ)βπ)) Β· (seqπ( Β· , πΉ)βπ))) |
50 | 1, 7, 8, 16, 18, 26, 49 | climmulc2 15587 |
. 2
β’ (π β seq(π + 1)( Β· , πΉ) β ((1 / (seqπ( Β· , πΉ)βπ)) Β· π΄)) |
51 | | climcl 15449 |
. . . 4
β’ (seqπ( Β· , πΉ) β π΄ β π΄ β β) |
52 | 8, 51 | syl 17 |
. . 3
β’ (π β π΄ β β) |
53 | 52, 14, 15 | divrec2d 11998 |
. 2
β’ (π β (π΄ / (seqπ( Β· , πΉ)βπ)) = ((1 / (seqπ( Β· , πΉ)βπ)) Β· π΄)) |
54 | 50, 53 | breqtrrd 5169 |
1
β’ (π β seq(π + 1)( Β· , πΉ) β (π΄ / (seqπ( Β· , πΉ)βπ))) |