Step | Hyp | Ref
| Expression |
1 | | nnuz 12861 |
. . . . . 6
β’ β =
(β€β₯β1) |
2 | | 1zzd 12589 |
. . . . . 6
β’ (π β 1 β
β€) |
3 | | geomcau.5 |
. . . . . . . 8
β’ (π β π΅ β
β+) |
4 | 3 | rpcnd 13014 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | 3 | rpred 13012 |
. . . . . . . . 9
β’ (π β π΅ β β) |
6 | 3 | rpge0d 13016 |
. . . . . . . . 9
β’ (π β 0 β€ π΅) |
7 | 5, 6 | absidd 15365 |
. . . . . . . 8
β’ (π β (absβπ΅) = π΅) |
8 | | geomcau.6 |
. . . . . . . 8
β’ (π β π΅ < 1) |
9 | 7, 8 | eqbrtrd 5169 |
. . . . . . 7
β’ (π β (absβπ΅) < 1) |
10 | 4, 9 | expcnv 15806 |
. . . . . 6
β’ (π β (π β β0 β¦ (π΅βπ)) β 0) |
11 | | geomcau.4 |
. . . . . . . 8
β’ (π β π΄ β β) |
12 | | 1re 11210 |
. . . . . . . . . 10
β’ 1 β
β |
13 | | resubcl 11520 |
. . . . . . . . . 10
β’ ((1
β β β§ π΅
β β) β (1 β π΅) β β) |
14 | 12, 5, 13 | sylancr 587 |
. . . . . . . . 9
β’ (π β (1 β π΅) β
β) |
15 | | posdif 11703 |
. . . . . . . . . . 11
β’ ((π΅ β β β§ 1 β
β) β (π΅ < 1
β 0 < (1 β π΅))) |
16 | 5, 12, 15 | sylancl 586 |
. . . . . . . . . 10
β’ (π β (π΅ < 1 β 0 < (1 β π΅))) |
17 | 8, 16 | mpbid 231 |
. . . . . . . . 9
β’ (π β 0 < (1 β π΅)) |
18 | 14, 17 | elrpd 13009 |
. . . . . . . 8
β’ (π β (1 β π΅) β
β+) |
19 | 11, 18 | rerpdivcld 13043 |
. . . . . . 7
β’ (π β (π΄ / (1 β π΅)) β β) |
20 | 19 | recnd 11238 |
. . . . . 6
β’ (π β (π΄ / (1 β π΅)) β β) |
21 | | nnex 12214 |
. . . . . . . 8
β’ β
β V |
22 | 21 | mptex 7221 |
. . . . . . 7
β’ (π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) β V |
23 | 22 | a1i 11 |
. . . . . 6
β’ (π β (π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) β V) |
24 | | nnnn0 12475 |
. . . . . . . . 9
β’ (π β β β π β
β0) |
25 | 24 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β0) |
26 | | oveq2 7413 |
. . . . . . . . 9
β’ (π = π β (π΅βπ) = (π΅βπ)) |
27 | | eqid 2732 |
. . . . . . . . 9
β’ (π β β0
β¦ (π΅βπ)) = (π β β0 β¦ (π΅βπ)) |
28 | | ovex 7438 |
. . . . . . . . 9
β’ (π΅βπ) β V |
29 | 26, 27, 28 | fvmpt 6995 |
. . . . . . . 8
β’ (π β β0
β ((π β
β0 β¦ (π΅βπ))βπ) = (π΅βπ)) |
30 | 25, 29 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β ((π β β0 β¦ (π΅βπ))βπ) = (π΅βπ)) |
31 | | nnz 12575 |
. . . . . . . . 9
β’ (π β β β π β
β€) |
32 | | rpexpcl 14042 |
. . . . . . . . 9
β’ ((π΅ β β+
β§ π β β€)
β (π΅βπ) β
β+) |
33 | 3, 31, 32 | syl2an 596 |
. . . . . . . 8
β’ ((π β§ π β β) β (π΅βπ) β
β+) |
34 | 33 | rpcnd 13014 |
. . . . . . 7
β’ ((π β§ π β β) β (π΅βπ) β β) |
35 | 30, 34 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β0 β¦ (π΅βπ))βπ) β β) |
36 | 20 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β) β (π΄ / (1 β π΅)) β β) |
37 | 34, 36 | mulcomd 11231 |
. . . . . . 7
β’ ((π β§ π β β) β ((π΅βπ) Β· (π΄ / (1 β π΅))) = ((π΄ / (1 β π΅)) Β· (π΅βπ))) |
38 | 26 | oveq1d 7420 |
. . . . . . . . 9
β’ (π = π β ((π΅βπ) Β· (π΄ / (1 β π΅))) = ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
39 | | eqid 2732 |
. . . . . . . . 9
β’ (π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) = (π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
40 | | ovex 7438 |
. . . . . . . . 9
β’ ((π΅βπ) Β· (π΄ / (1 β π΅))) β V |
41 | 38, 39, 40 | fvmpt 6995 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅))))βπ) = ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
42 | 41 | adantl 482 |
. . . . . . 7
β’ ((π β§ π β β) β ((π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅))))βπ) = ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
43 | 30 | oveq2d 7421 |
. . . . . . 7
β’ ((π β§ π β β) β ((π΄ / (1 β π΅)) Β· ((π β β0 β¦ (π΅βπ))βπ)) = ((π΄ / (1 β π΅)) Β· (π΅βπ))) |
44 | 37, 42, 43 | 3eqtr4d 2782 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅))))βπ) = ((π΄ / (1 β π΅)) Β· ((π β β0 β¦ (π΅βπ))βπ))) |
45 | 1, 2, 10, 20, 23, 35, 44 | climmulc2 15577 |
. . . . 5
β’ (π β (π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) β ((π΄ / (1 β π΅)) Β· 0)) |
46 | 20 | mul01d 11409 |
. . . . 5
β’ (π β ((π΄ / (1 β π΅)) Β· 0) = 0) |
47 | 45, 46 | breqtrd 5173 |
. . . 4
β’ (π β (π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) β 0) |
48 | 33 | rpred 13012 |
. . . . . . 7
β’ ((π β§ π β β) β (π΅βπ) β β) |
49 | 19 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄ / (1 β π΅)) β β) |
50 | 48, 49 | remulcld 11240 |
. . . . . 6
β’ ((π β§ π β β) β ((π΅βπ) Β· (π΄ / (1 β π΅))) β β) |
51 | 50 | recnd 11238 |
. . . . 5
β’ ((π β§ π β β) β ((π΅βπ) Β· (π΄ / (1 β π΅))) β β) |
52 | 1, 2, 23, 42, 51 | clim0c 15447 |
. . . 4
β’ (π β ((π β β β¦ ((π΅βπ) Β· (π΄ / (1 β π΅)))) β 0 β βπ₯ β β+
βπ β β
βπ β
(β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯)) |
53 | 47, 52 | mpbid 231 |
. . 3
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯) |
54 | | nnz 12575 |
. . . . . . . 8
β’ (π β β β π β
β€) |
55 | 54 | adantl 482 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β β) β π β
β€) |
56 | | uzid 12833 |
. . . . . . 7
β’ (π β β€ β π β
(β€β₯βπ)) |
57 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π = π β (π΅βπ) = (π΅βπ)) |
58 | 57 | fvoveq1d 7427 |
. . . . . . . . 9
β’ (π = π β (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) = (absβ((π΅βπ) Β· (π΄ / (1 β π΅))))) |
59 | 58 | breq1d 5157 |
. . . . . . . 8
β’ (π = π β ((absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯)) |
60 | 59 | rspcv 3608 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯)) |
61 | 55, 56, 60 | 3syl 18 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β β) β
(βπ β
(β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯)) |
62 | | lmclim2.2 |
. . . . . . . . . . . . 13
β’ (π β π· β (Metβπ)) |
63 | 62 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π· β (Metβπ)) |
64 | | lmclim2.3 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆπ) |
65 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
66 | | ffvelcdm 7080 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆπ β§ π β β) β (πΉβπ) β π) |
67 | 64, 65, 66 | syl2an 596 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (πΉβπ) β π) |
68 | | eluznn 12898 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
69 | | ffvelcdm 7080 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆπ β§ π β β) β (πΉβπ) β π) |
70 | 64, 68, 69 | syl2an 596 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (πΉβπ) β π) |
71 | | metcl 23829 |
. . . . . . . . . . . 12
β’ ((π· β (Metβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) β β) |
72 | 63, 67, 70, 71 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β β) |
73 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(β€β₯βπ) = (β€β₯βπ) |
74 | | nnnn0 12475 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β0) |
75 | 74 | ad2antrl 726 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π β β0) |
76 | 75 | nn0zd 12580 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π β β€) |
77 | | oveq2 7413 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΅βπ) = (π΅βπ)) |
78 | 77 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π΄ Β· (π΅βπ)) = (π΄ Β· (π΅βπ))) |
79 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β¦ (π΄ Β· (π΅βπ))) = (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ))) |
80 | | ovex 7438 |
. . . . . . . . . . . . . . 15
β’ (π΄ Β· (π΅βπ)) β V |
81 | 78, 79, 80 | fvmpt 6995 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))βπ) = (π΄ Β· (π΅βπ))) |
82 | 81 | adantl 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))βπ) = (π΄ Β· (π΅βπ))) |
83 | 11 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β π΄ β β) |
84 | 5 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β π΅ β β) |
85 | | eluznn0 12897 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π β
(β€β₯βπ)) β π β β0) |
86 | 75, 85 | sylan 580 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β π β β0) |
87 | 84, 86 | reexpcld 14124 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (π΅βπ) β β) |
88 | 83, 87 | remulcld 11240 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (π΄ Β· (π΅βπ)) β β) |
89 | 88 | recnd 11238 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (π΄ Β· (π΅βπ)) β β) |
90 | 11 | recnd 11238 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β β) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π΄ β β) |
92 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π΅ β β) |
93 | 9 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (absβπ΅) < 1) |
94 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯βπ) β¦ (π΅βπ)) = (π β (β€β₯βπ) β¦ (π΅βπ)) |
95 | | ovex 7438 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅βπ) β V |
96 | 77, 94, 95 | fvmpt 6995 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ (π΅βπ))βπ) = (π΅βπ)) |
97 | 96 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (π΅βπ))βπ) = (π΅βπ)) |
98 | 92, 93, 75, 97 | geolim2 15813 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β seqπ( + , (π β (β€β₯βπ) β¦ (π΅βπ))) β ((π΅βπ) / (1 β π΅))) |
99 | 87 | recnd 11238 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (π΅βπ) β β) |
100 | 97, 99 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (π΅βπ))βπ) β β) |
101 | 97 | oveq2d 7421 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (π΄ Β· ((π β (β€β₯βπ) β¦ (π΅βπ))βπ)) = (π΄ Β· (π΅βπ))) |
102 | 82, 101 | eqtr4d 2775 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))βπ) = (π΄ Β· ((π β (β€β₯βπ) β¦ (π΅βπ))βπ))) |
103 | 73, 76, 91, 98, 100, 102 | isermulc2 15600 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β seqπ( + , (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))) β (π΄ Β· ((π΅βπ) / (1 β π΅)))) |
104 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π΅ β
β+) |
105 | 104, 76 | rpexpcld 14206 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (π΅βπ) β
β+) |
106 | 105 | rpcnd 13014 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (π΅βπ) β β) |
107 | 14 | recnd 11238 |
. . . . . . . . . . . . . . . 16
β’ (π β (1 β π΅) β
β) |
108 | 107 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (1 β π΅) β
β) |
109 | 18 | rpne0d 13017 |
. . . . . . . . . . . . . . . 16
β’ (π β (1 β π΅) β 0) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (1 β π΅) β 0) |
111 | 91, 106, 108, 110 | div12d 12022 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (π΄ Β· ((π΅βπ) / (1 β π΅))) = ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
112 | 103, 111 | breqtrd 5173 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β seqπ( + , (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))) β ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
113 | 73, 76, 82, 89, 112 | isumclim 15699 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β
(β€β₯βπ)(π΄ Β· (π΅βπ)) = ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
114 | | seqex 13964 |
. . . . . . . . . . . . . . 15
β’ seqπ( + , (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))) β V |
115 | | ovex 7438 |
. . . . . . . . . . . . . . 15
β’ (π΄ Β· ((π΅βπ) / (1 β π΅))) β V |
116 | 114, 115 | breldm 5906 |
. . . . . . . . . . . . . 14
β’ (seqπ( + , (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))) β (π΄ Β· ((π΅βπ) / (1 β π΅))) β seqπ( + , (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))) β dom β ) |
117 | 103, 116 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β seqπ( + , (π β (β€β₯βπ) β¦ (π΄ Β· (π΅βπ)))) β dom β ) |
118 | 73, 76, 82, 88, 117 | isumrecl 15707 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β
(β€β₯βπ)(π΄ Β· (π΅βπ)) β β) |
119 | 113, 118 | eqeltrrd 2834 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((π΅βπ) Β· (π΄ / (1 β π΅))) β β) |
120 | 119 | recnd 11238 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((π΅βπ) Β· (π΄ / (1 β π΅))) β β) |
121 | 120 | abscld 15379 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) β β) |
122 | | fzfid 13934 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (π...(π β 1)) β Fin) |
123 | | simpll 765 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β π) |
124 | | elfzuz 13493 |
. . . . . . . . . . . . . . . 16
β’ (π β (π...(π β 1)) β π β (β€β₯βπ)) |
125 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π β β) |
126 | | eluznn 12898 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
127 | 125, 126 | sylan 580 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β π β β) |
128 | 124, 127 | sylan2 593 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β π β β) |
129 | 62 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π· β (Metβπ)) |
130 | 64 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΉβπ) β π) |
131 | | peano2nn 12220 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π + 1) β
β) |
132 | | ffvelcdm 7080 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:ββΆπ β§ (π + 1) β β) β (πΉβ(π + 1)) β π) |
133 | 64, 131, 132 | syl2an 596 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΉβ(π + 1)) β π) |
134 | | metcl 23829 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Metβπ) β§ (πΉβπ) β π β§ (πΉβ(π + 1)) β π) β ((πΉβπ)π·(πΉβ(π + 1))) β β) |
135 | 129, 130,
133, 134 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((πΉβπ)π·(πΉβ(π + 1))) β β) |
136 | 123, 128,
135 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β ((πΉβπ)π·(πΉβ(π + 1))) β β) |
137 | 122, 136 | fsumrecl 15676 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β (π...(π β 1))((πΉβπ)π·(πΉβ(π + 1))) β β) |
138 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
139 | | elfzuz 13493 |
. . . . . . . . . . . . . . 15
β’ (π β (π...π) β π β (β€β₯βπ)) |
140 | | simpll 765 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β π) |
141 | 140, 127,
130 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (πΉβπ) β π) |
142 | 139, 141 | sylan2 593 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΉβπ) β π) |
143 | 63, 138, 142 | mettrifi 36613 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β€ Ξ£π β (π...(π β 1))((πΉβπ)π·(πΉβ(π + 1)))) |
144 | 124, 88 | sylan2 593 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β (π΄ Β· (π΅βπ)) β β) |
145 | 122, 144 | fsumrecl 15676 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β (π...(π β 1))(π΄ Β· (π΅βπ)) β β) |
146 | | geomcau.7 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΉβπ)π·(πΉβ(π + 1))) β€ (π΄ Β· (π΅βπ))) |
147 | 123, 128,
146 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β ((πΉβπ)π·(πΉβ(π + 1))) β€ (π΄ Β· (π΅βπ))) |
148 | 122, 136,
144, 147 | fsumle 15741 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β (π...(π β 1))((πΉβπ)π·(πΉβ(π + 1))) β€ Ξ£π β (π...(π β 1))(π΄ Β· (π΅βπ))) |
149 | | fzssuz 13538 |
. . . . . . . . . . . . . . . 16
β’ (π...(π β 1)) β
(β€β₯βπ) |
150 | 149 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (π...(π β 1)) β
(β€β₯βπ)) |
151 | | 0red 11213 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β 0 β
β) |
152 | | nnz 12575 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β€) |
153 | | rpexpcl 14042 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β β+
β§ π β β€)
β (π΅βπ) β
β+) |
154 | 3, 152, 153 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (π΅βπ) β
β+) |
155 | 135, 154 | rerpdivcld 13043 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (((πΉβπ)π·(πΉβ(π + 1))) / (π΅βπ)) β β) |
156 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π΄ β β) |
157 | | metge0 23842 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Metβπ) β§ (πΉβπ) β π β§ (πΉβ(π + 1)) β π) β 0 β€ ((πΉβπ)π·(πΉβ(π + 1)))) |
158 | 129, 130,
133, 157 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β 0 β€ ((πΉβπ)π·(πΉβ(π + 1)))) |
159 | 135, 154,
158 | divge0d 13052 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β 0 β€ (((πΉβπ)π·(πΉβ(π + 1))) / (π΅βπ))) |
160 | 135, 156,
154 | ledivmul2d 13066 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((((πΉβπ)π·(πΉβ(π + 1))) / (π΅βπ)) β€ π΄ β ((πΉβπ)π·(πΉβ(π + 1))) β€ (π΄ Β· (π΅βπ)))) |
161 | 146, 160 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (((πΉβπ)π·(πΉβ(π + 1))) / (π΅βπ)) β€ π΄) |
162 | 151, 155,
156, 159, 161 | letrd 11367 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β 0 β€ π΄) |
163 | 140, 127,
162 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β 0 β€ π΄) |
164 | 140, 127,
154 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β (π΅βπ) β
β+) |
165 | 164 | rpge0d 13016 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β 0 β€ (π΅βπ)) |
166 | 83, 87, 163, 165 | mulge0d 11787 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ π β (β€β₯βπ))) β§ π β (β€β₯βπ)) β 0 β€ (π΄ Β· (π΅βπ))) |
167 | 73, 76, 122, 150, 82, 88, 166, 117 | isumless 15787 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β (π...(π β 1))(π΄ Β· (π΅βπ)) β€ Ξ£π β (β€β₯βπ)(π΄ Β· (π΅βπ))) |
168 | 137, 145,
118, 148, 167 | letrd 11367 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Ξ£π β (π...(π β 1))((πΉβπ)π·(πΉβ(π + 1))) β€ Ξ£π β (β€β₯βπ)(π΄ Β· (π΅βπ))) |
169 | 72, 137, 118, 143, 168 | letrd 11367 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β€ Ξ£π β (β€β₯βπ)(π΄ Β· (π΅βπ))) |
170 | 169, 113 | breqtrd 5173 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β€ ((π΅βπ) Β· (π΄ / (1 β π΅)))) |
171 | 119 | leabsd 15357 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((π΅βπ) Β· (π΄ / (1 β π΅))) β€ (absβ((π΅βπ) Β· (π΄ / (1 β π΅))))) |
172 | 72, 119, 121, 170, 171 | letrd 11367 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β€ (absβ((π΅βπ) Β· (π΄ / (1 β π΅))))) |
173 | 172 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β€ (absβ((π΅βπ) Β· (π΄ / (1 β π΅))))) |
174 | 72 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) β β) |
175 | 121 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯βπ))) β (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) β β) |
176 | | rpre 12978 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β) |
177 | 176 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯βπ))) β π₯ β β) |
178 | | lelttr 11300 |
. . . . . . . . . 10
β’ ((((πΉβπ)π·(πΉβπ)) β β β§ (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) β β β§ π₯ β β) β ((((πΉβπ)π·(πΉβπ)) β€ (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) β§ (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
179 | 174, 175,
177, 178 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯βπ))) β ((((πΉβπ)π·(πΉβπ)) β€ (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) β§ (absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
180 | 173, 179 | mpand 693 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯βπ))) β ((absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
181 | 180 | anassrs 468 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β ((absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
182 | 181 | ralrimdva 3154 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β β) β
((absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
183 | 61, 182 | syld 47 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β) β
(βπ β
(β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
184 | 183 | reximdva 3168 |
. . . 4
β’ ((π β§ π₯ β β+) β
(βπ β β
βπ β
(β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β βπ β β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
185 | 184 | ralimdva 3167 |
. . 3
β’ (π β (βπ₯ β β+
βπ β β
βπ β
(β€β₯βπ)(absβ((π΅βπ) Β· (π΄ / (1 β π΅)))) < π₯ β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
186 | 53, 185 | mpd 15 |
. 2
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
187 | | metxmet 23831 |
. . . 4
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
188 | 62, 187 | syl 17 |
. . 3
β’ (π β π· β (βMetβπ)) |
189 | | eqidd 2733 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
190 | | eqidd 2733 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
191 | 1, 188, 2, 189, 190, 64 | iscauf 24788 |
. 2
β’ (π β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
192 | 186, 191 | mpbird 256 |
1
β’ (π β πΉ β (Cauβπ·)) |