Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β π₯ β
(2[,)+β)) |
2 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
3 | | elicopnf 13369 |
. . . . . . . . . 10
β’ (2 β
β β (π₯ β
(2[,)+β) β (π₯
β β β§ 2 β€ π₯))) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯)) |
5 | 1, 4 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β (π₯ β β β§ 2 β€
π₯)) |
6 | 5 | simpld 496 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β π₯ β
β) |
7 | | 0red 11165 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β 0 β
β) |
8 | 2 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β 2 β
β) |
9 | | 2pos 12263 |
. . . . . . . . 9
β’ 0 <
2 |
10 | 9 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β 0 <
2) |
11 | 5 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β 2 β€ π₯) |
12 | 7, 8, 6, 10, 11 | ltletrd 11322 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β 0 < π₯) |
13 | 6, 12 | elrpd 12961 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β π₯ β
β+) |
14 | | chtppilim.1 |
. . . . . . . 8
β’ (π β π΄ β
β+) |
15 | 14 | rpred 12964 |
. . . . . . 7
β’ (π β π΄ β β) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β π΄ β
β) |
17 | 13, 16 | rpcxpcld 26103 |
. . . . 5
β’ ((π β§ π₯ β (2[,)+β)) β (π₯βππ΄) β
β+) |
18 | | ppinncl 26539 |
. . . . . . 7
β’ ((π₯ β β β§ 2 β€
π₯) β
(Οβπ₯)
β β) |
19 | 5, 18 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β
(Οβπ₯)
β β) |
20 | 19 | nnrpd 12962 |
. . . . 5
β’ ((π β§ π₯ β (2[,)+β)) β
(Οβπ₯)
β β+) |
21 | 17, 20 | rpdivcld 12981 |
. . . 4
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯βππ΄) / (Οβπ₯)) β
β+) |
22 | 21 | ralrimiva 3144 |
. . 3
β’ (π β βπ₯ β (2[,)+β)((π₯βππ΄) / (Οβπ₯)) β
β+) |
23 | | chtppilim.2 |
. . . 4
β’ (π β π΄ < 1) |
24 | | 1re 11162 |
. . . . 5
β’ 1 β
β |
25 | | difrp 12960 |
. . . . 5
β’ ((π΄ β β β§ 1 β
β) β (π΄ < 1
β (1 β π΄) β
β+)) |
26 | 15, 24, 25 | sylancl 587 |
. . . 4
β’ (π β (π΄ < 1 β (1 β π΄) β
β+)) |
27 | 23, 26 | mpbid 231 |
. . 3
β’ (π β (1 β π΄) β
β+) |
28 | | ovexd 7397 |
. . . . . 6
β’ (π β (2[,)+β) β
V) |
29 | 24 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β 1 β
β) |
30 | | 1lt2 12331 |
. . . . . . . . . . 11
β’ 1 <
2 |
31 | 30 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β 1 <
2) |
32 | 29, 8, 6, 31, 11 | ltletrd 11322 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β 1 < π₯) |
33 | 6, 32 | rplogcld 26000 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β
(logβπ₯) β
β+) |
34 | 13, 33 | rpdivcld 12981 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β (π₯ / (logβπ₯)) β
β+) |
35 | 34, 20 | rpdivcld 12981 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯ / (logβπ₯)) / (Οβπ₯)) β
β+) |
36 | 27 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β (1 β
π΄) β
β+) |
37 | 36 | rpred 12964 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β (1 β
π΄) β
β) |
38 | 13, 37 | rpcxpcld 26103 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β (π₯βπ(1
β π΄)) β
β+) |
39 | 33, 38 | rpdivcld 12981 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β
((logβπ₯) / (π₯βπ(1
β π΄))) β
β+) |
40 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β (2[,)+β) β¦ ((π₯ / (logβπ₯)) / (Οβπ₯))) = (π₯ β (2[,)+β) β¦ ((π₯ / (logβπ₯)) / (Οβπ₯)))) |
41 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄)))) = (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄))))) |
42 | 28, 35, 39, 40, 41 | offval2 7642 |
. . . . 5
β’ (π β ((π₯ β (2[,)+β) β¦ ((π₯ / (logβπ₯)) / (Οβπ₯))) βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄))))) = (π₯ β (2[,)+β) β¦
(((π₯ / (logβπ₯)) / (Οβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))))) |
43 | 34 | rpcnd 12966 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β (π₯ / (logβπ₯)) β β) |
44 | 39 | rpcnd 12966 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β
((logβπ₯) / (π₯βπ(1
β π΄))) β
β) |
45 | 20 | rpcnne0d 12973 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β
((Οβπ₯)
β β β§ (Οβπ₯) β 0)) |
46 | | div23 11839 |
. . . . . . . 8
β’ (((π₯ / (logβπ₯)) β β β§ ((logβπ₯) / (π₯βπ(1 β π΄))) β β β§
((Οβπ₯)
β β β§ (Οβπ₯) β 0)) β (((π₯ / (logβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))) / (Οβπ₯)) = (((π₯ / (logβπ₯)) / (Οβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄))))) |
47 | 43, 44, 45, 46 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β (((π₯ / (logβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))) / (Οβπ₯)) = (((π₯ / (logβπ₯)) / (Οβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄))))) |
48 | 33 | rpcnne0d 12973 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β
((logβπ₯) β
β β§ (logβπ₯)
β 0)) |
49 | 38 | rpcnne0d 12973 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯βπ(1
β π΄)) β β
β§ (π₯βπ(1 β π΄)) β 0)) |
50 | 6 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β π₯ β
β) |
51 | | dmdcan 11872 |
. . . . . . . . . 10
β’
((((logβπ₯)
β β β§ (logβπ₯) β 0) β§ ((π₯βπ(1 β π΄)) β β β§ (π₯βπ(1
β π΄)) β 0) β§
π₯ β β) β
(((logβπ₯) / (π₯βπ(1
β π΄))) Β·
(π₯ / (logβπ₯))) = (π₯ / (π₯βπ(1 β π΄)))) |
52 | 48, 49, 50, 51 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β
(((logβπ₯) / (π₯βπ(1
β π΄))) Β·
(π₯ / (logβπ₯))) = (π₯ / (π₯βπ(1 β π΄)))) |
53 | 43, 44 | mulcomd 11183 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯ / (logβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))) = (((logβπ₯) / (π₯βπ(1 β π΄))) Β· (π₯ / (logβπ₯)))) |
54 | 13 | rpcnne0d 12973 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (2[,)+β)) β (π₯ β β β§ π₯ β 0)) |
55 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
β’ 1 β
β |
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (2[,)+β)) β 1 β
β) |
57 | 36 | rpcnd 12966 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (2[,)+β)) β (1 β
π΄) β
β) |
58 | | cxpsub 26053 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π₯ β 0) β§ 1 β β
β§ (1 β π΄) β
β) β (π₯βπ(1 β (1
β π΄))) = ((π₯βπ1) /
(π₯βπ(1 β π΄)))) |
59 | 54, 56, 57, 58 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (2[,)+β)) β (π₯βπ(1
β (1 β π΄))) =
((π₯βπ1) / (π₯βπ(1
β π΄)))) |
60 | 16 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (2[,)+β)) β π΄ β
β) |
61 | | nncan 11437 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ π΄
β β) β (1 β (1 β π΄)) = π΄) |
62 | 55, 60, 61 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (2[,)+β)) β (1 β (1
β π΄)) = π΄) |
63 | 62 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (2[,)+β)) β (π₯βπ(1
β (1 β π΄))) =
(π₯βππ΄)) |
64 | 59, 63 | eqtr3d 2779 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯βπ1) /
(π₯βπ(1 β π΄))) = (π₯βππ΄)) |
65 | 50 | cxp1d 26077 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (2[,)+β)) β (π₯βπ1) =
π₯) |
66 | 65 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯βπ1) /
(π₯βπ(1 β π΄))) = (π₯ / (π₯βπ(1 β π΄)))) |
67 | 64, 66 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β (π₯βππ΄) = (π₯ / (π₯βπ(1 β π΄)))) |
68 | 52, 53, 67 | 3eqtr4d 2787 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯ / (logβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))) = (π₯βππ΄)) |
69 | 68 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β (((π₯ / (logβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))) / (Οβπ₯)) = ((π₯βππ΄) / (Οβπ₯))) |
70 | 47, 69 | eqtr3d 2779 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β (((π₯ / (logβπ₯)) / (Οβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄)))) = ((π₯βππ΄) / (Οβπ₯))) |
71 | 70 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (2[,)+β) β¦ (((π₯ / (logβπ₯)) / (Οβπ₯)) Β· ((logβπ₯) / (π₯βπ(1 β π΄))))) = (π₯ β (2[,)+β) β¦ ((π₯βππ΄) / (Οβπ₯)))) |
72 | 42, 71 | eqtrd 2777 |
. . . 4
β’ (π β ((π₯ β (2[,)+β) β¦ ((π₯ / (logβπ₯)) / (Οβπ₯))) βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄))))) = (π₯ β (2[,)+β) β¦
((π₯βππ΄) / (Οβπ₯)))) |
73 | | chebbnd1 26836 |
. . . . 5
β’ (π₯ β (2[,)+β) β¦
((π₯ / (logβπ₯)) / (Οβπ₯))) β
π(1) |
74 | 13 | ex 414 |
. . . . . . 7
β’ (π β (π₯ β (2[,)+β) β π₯ β
β+)) |
75 | 74 | ssrdv 3955 |
. . . . . 6
β’ (π β (2[,)+β) β
β+) |
76 | | cxploglim 26343 |
. . . . . . 7
β’ ((1
β π΄) β
β+ β (π₯ β β+ β¦
((logβπ₯) / (π₯βπ(1
β π΄))))
βπ 0) |
77 | 27, 76 | syl 17 |
. . . . . 6
β’ (π β (π₯ β β+ β¦
((logβπ₯) / (π₯βπ(1
β π΄))))
βπ 0) |
78 | 75, 77 | rlimres2 15450 |
. . . . 5
β’ (π β (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄))))
βπ 0) |
79 | | o1rlimmul 15508 |
. . . . 5
β’ (((π₯ β (2[,)+β) β¦
((π₯ / (logβπ₯)) / (Οβπ₯))) β π(1) β§
(π₯ β (2[,)+β)
β¦ ((logβπ₯) /
(π₯βπ(1 β π΄)))) βπ
0) β ((π₯ β
(2[,)+β) β¦ ((π₯
/ (logβπ₯)) /
(Οβπ₯)))
βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄)))))
βπ 0) |
80 | 73, 78, 79 | sylancr 588 |
. . . 4
β’ (π β ((π₯ β (2[,)+β) β¦ ((π₯ / (logβπ₯)) / (Οβπ₯))) βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1
β π΄)))))
βπ 0) |
81 | 72, 80 | eqbrtrrd 5134 |
. . 3
β’ (π β (π₯ β (2[,)+β) β¦ ((π₯βππ΄) / (Οβπ₯))) βπ
0) |
82 | 22, 27, 81 | rlimi 15402 |
. 2
β’ (π β βπ§ β β βπ₯ β (2[,)+β)(π§ β€ π₯ β (absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) < (1 β π΄))) |
83 | 21 | rpcnd 12966 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯βππ΄) / (Οβπ₯)) β
β) |
84 | 83 | subid1d 11508 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β (((π₯βππ΄) / (Οβπ₯)) β 0) = ((π₯βππ΄) / (Οβπ₯))) |
85 | 84 | fveq2d 6851 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β
(absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) = (absβ((π₯βππ΄) / (Οβπ₯)))) |
86 | 21 | rpred 12964 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β ((π₯βππ΄) / (Οβπ₯)) β
β) |
87 | 21 | rpge0d 12968 |
. . . . . . . . 9
β’ ((π β§ π₯ β (2[,)+β)) β 0 β€ ((π₯βππ΄) / (Οβπ₯))) |
88 | 86, 87 | absidd 15314 |
. . . . . . . 8
β’ ((π β§ π₯ β (2[,)+β)) β
(absβ((π₯βππ΄) / (Οβπ₯))) = ((π₯βππ΄) / (Οβπ₯))) |
89 | 85, 88 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π₯ β (2[,)+β)) β
(absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) = ((π₯βππ΄) / (Οβπ₯))) |
90 | 89 | breq1d 5120 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β
((absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) < (1 β π΄) β ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄))) |
91 | 14 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (2[,)+β) β§ ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄))) β π΄ β
β+) |
92 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (2[,)+β) β§ ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄))) β π΄ < 1) |
93 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π₯ β (2[,)+β) β§ ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄))) β π₯ β (2[,)+β)) |
94 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π₯ β (2[,)+β) β§ ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄))) β ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄)) |
95 | 91, 92, 93, 94 | chtppilimlem1 26837 |
. . . . . . 7
β’ ((π β§ (π₯ β (2[,)+β) β§ ((π₯βππ΄) / (Οβπ₯)) < (1 β π΄))) β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯)) |
96 | 95 | expr 458 |
. . . . . 6
β’ ((π β§ π₯ β (2[,)+β)) β (((π₯βππ΄) / (Οβπ₯)) < (1 β π΄) β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯))) |
97 | 90, 96 | sylbid 239 |
. . . . 5
β’ ((π β§ π₯ β (2[,)+β)) β
((absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) < (1 β π΄) β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯))) |
98 | 97 | imim2d 57 |
. . . 4
β’ ((π β§ π₯ β (2[,)+β)) β ((π§ β€ π₯ β (absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) < (1 β π΄)) β (π§ β€ π₯ β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯)))) |
99 | 98 | ralimdva 3165 |
. . 3
β’ (π β (βπ₯ β (2[,)+β)(π§ β€ π₯ β (absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) < (1 β π΄)) β βπ₯ β (2[,)+β)(π§ β€ π₯ β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯)))) |
100 | 99 | reximdv 3168 |
. 2
β’ (π β (βπ§ β β βπ₯ β (2[,)+β)(π§ β€ π₯ β (absβ(((π₯βππ΄) / (Οβπ₯)) β 0)) < (1 β π΄)) β βπ§ β β βπ₯ β (2[,)+β)(π§ β€ π₯ β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯)))) |
101 | 82, 100 | mpd 15 |
1
β’ (π β βπ§ β β βπ₯ β (2[,)+β)(π§ β€ π₯ β ((π΄β2) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯))) |