Step | Hyp | Ref
| Expression |
1 | | ioorp 13402 |
. . . 4
β’
(0(,)+β) = β+ |
2 | 1 | eqcomi 2742 |
. . 3
β’
β+ = (0(,)+β) |
3 | | nnuz 12865 |
. . 3
β’ β =
(β€β₯β1) |
4 | | 1zzd 12593 |
. . 3
β’ (β€
β 1 β β€) |
5 | | ere 16032 |
. . . 4
β’ e β
β |
6 | 5 | a1i 11 |
. . 3
β’ (β€
β e β β) |
7 | | 0re 11216 |
. . . . . 6
β’ 0 β
β |
8 | | epos 16150 |
. . . . . 6
β’ 0 <
e |
9 | 7, 5, 8 | ltleii 11337 |
. . . . 5
β’ 0 β€
e |
10 | 9 | a1i 11 |
. . . 4
β’ (β€
β 0 β€ e) |
11 | | 1re 11214 |
. . . . 5
β’ 1 β
β |
12 | | addge02 11725 |
. . . . 5
β’ ((1
β β β§ e β β) β (0 β€ e β 1 β€ (e +
1))) |
13 | 11, 5, 12 | mp2an 691 |
. . . 4
β’ (0 β€ e
β 1 β€ (e + 1)) |
14 | 10, 13 | sylib 217 |
. . 3
β’ (β€
β 1 β€ (e + 1)) |
15 | 7 | a1i 11 |
. . 3
β’ (β€
β 0 β β) |
16 | | relogcl 26084 |
. . . . . 6
β’ (π¦ β β+
β (logβπ¦) β
β) |
17 | 16 | adantl 483 |
. . . . 5
β’
((β€ β§ π¦
β β+) β (logβπ¦) β β) |
18 | 17 | resqcld 14090 |
. . . 4
β’
((β€ β§ π¦
β β+) β ((logβπ¦)β2) β β) |
19 | 18 | rehalfcld 12459 |
. . 3
β’
((β€ β§ π¦
β β+) β (((logβπ¦)β2) / 2) β
β) |
20 | | rerpdivcl 13004 |
. . . . 5
β’
(((logβπ¦)
β β β§ π¦
β β+) β ((logβπ¦) / π¦) β β) |
21 | 16, 20 | mpancom 687 |
. . . 4
β’ (π¦ β β+
β ((logβπ¦) /
π¦) β
β) |
22 | 21 | adantl 483 |
. . 3
β’
((β€ β§ π¦
β β+) β ((logβπ¦) / π¦) β β) |
23 | | nnrp 12985 |
. . . 4
β’ (π¦ β β β π¦ β
β+) |
24 | 23, 22 | sylan2 594 |
. . 3
β’
((β€ β§ π¦
β β) β ((logβπ¦) / π¦) β β) |
25 | | reelprrecn 11202 |
. . . . . 6
β’ β
β {β, β} |
26 | 25 | a1i 11 |
. . . . 5
β’ (β€
β β β {β, β}) |
27 | | cnelprrecn 11203 |
. . . . . 6
β’ β
β {β, β} |
28 | 27 | a1i 11 |
. . . . 5
β’ (β€
β β β {β, β}) |
29 | 17 | recnd 11242 |
. . . . 5
β’
((β€ β§ π¦
β β+) β (logβπ¦) β β) |
30 | | ovexd 7444 |
. . . . 5
β’
((β€ β§ π¦
β β+) β (1 / π¦) β V) |
31 | | sqcl 14083 |
. . . . . . 7
β’ (π₯ β β β (π₯β2) β
β) |
32 | 31 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β β) β (π₯β2) β β) |
33 | 32 | halfcld 12457 |
. . . . 5
β’
((β€ β§ π₯
β β) β ((π₯β2) / 2) β
β) |
34 | | simpr 486 |
. . . . 5
β’
((β€ β§ π₯
β β) β π₯
β β) |
35 | | relogf1o 26075 |
. . . . . . . . . 10
β’ (log
βΎ β+):β+β1-1-ontoββ |
36 | | f1of 6834 |
. . . . . . . . . 10
β’ ((log
βΎ β+):β+β1-1-ontoββ β (log βΎ
β+):β+βΆβ) |
37 | 35, 36 | mp1i 13 |
. . . . . . . . 9
β’ (β€
β (log βΎ
β+):β+βΆβ) |
38 | 37 | feqmptd 6961 |
. . . . . . . 8
β’ (β€
β (log βΎ β+) = (π¦ β β+ β¦ ((log
βΎ β+)βπ¦))) |
39 | | fvres 6911 |
. . . . . . . . 9
β’ (π¦ β β+
β ((log βΎ β+)βπ¦) = (logβπ¦)) |
40 | 39 | mpteq2ia 5252 |
. . . . . . . 8
β’ (π¦ β β+
β¦ ((log βΎ β+)βπ¦)) = (π¦ β β+ β¦
(logβπ¦)) |
41 | 38, 40 | eqtrdi 2789 |
. . . . . . 7
β’ (β€
β (log βΎ β+) = (π¦ β β+ β¦
(logβπ¦))) |
42 | 41 | oveq2d 7425 |
. . . . . 6
β’ (β€
β (β D (log βΎ β+)) = (β D (π¦ β β+
β¦ (logβπ¦)))) |
43 | | dvrelog 26145 |
. . . . . 6
β’ (β
D (log βΎ β+)) = (π¦ β β+ β¦ (1 /
π¦)) |
44 | 42, 43 | eqtr3di 2788 |
. . . . 5
β’ (β€
β (β D (π¦ β
β+ β¦ (logβπ¦))) = (π¦ β β+ β¦ (1 /
π¦))) |
45 | | ovexd 7444 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (2 Β· π₯) β V) |
46 | | 2nn 12285 |
. . . . . . . . 9
β’ 2 β
β |
47 | | dvexp 25470 |
. . . . . . . . 9
β’ (2 β
β β (β D (π₯ β β β¦ (π₯β2))) = (π₯ β β β¦ (2 Β· (π₯β(2 β
1))))) |
48 | 46, 47 | mp1i 13 |
. . . . . . . 8
β’ (β€
β (β D (π₯ β
β β¦ (π₯β2))) = (π₯ β β β¦ (2 Β· (π₯β(2 β
1))))) |
49 | | 2m1e1 12338 |
. . . . . . . . . . . 12
β’ (2
β 1) = 1 |
50 | 49 | oveq2i 7420 |
. . . . . . . . . . 11
β’ (π₯β(2 β 1)) = (π₯β1) |
51 | | exp1 14033 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯β1) = π₯) |
52 | 51 | adantl 483 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β β) β (π₯β1) = π₯) |
53 | 50, 52 | eqtrid 2785 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β (π₯β(2 β 1)) = π₯) |
54 | 53 | oveq2d 7425 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (2 Β· (π₯β(2 β 1))) = (2 Β· π₯)) |
55 | 54 | mpteq2dva 5249 |
. . . . . . . 8
β’ (β€
β (π₯ β β
β¦ (2 Β· (π₯β(2 β 1)))) = (π₯ β β β¦ (2 Β· π₯))) |
56 | 48, 55 | eqtrd 2773 |
. . . . . . 7
β’ (β€
β (β D (π₯ β
β β¦ (π₯β2))) = (π₯ β β β¦ (2 Β· π₯))) |
57 | | 2cnd 12290 |
. . . . . . 7
β’ (β€
β 2 β β) |
58 | | 2ne0 12316 |
. . . . . . . 8
β’ 2 β
0 |
59 | 58 | a1i 11 |
. . . . . . 7
β’ (β€
β 2 β 0) |
60 | 28, 32, 45, 56, 57, 59 | dvmptdivc 25482 |
. . . . . 6
β’ (β€
β (β D (π₯ β
β β¦ ((π₯β2)
/ 2))) = (π₯ β β
β¦ ((2 Β· π₯) /
2))) |
61 | | 2cn 12287 |
. . . . . . . . 9
β’ 2 β
β |
62 | | divcan3 11898 |
. . . . . . . . 9
β’ ((π₯ β β β§ 2 β
β β§ 2 β 0) β ((2 Β· π₯) / 2) = π₯) |
63 | 61, 58, 62 | mp3an23 1454 |
. . . . . . . 8
β’ (π₯ β β β ((2
Β· π₯) / 2) = π₯) |
64 | 63 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β ((2 Β· π₯) / 2) = π₯) |
65 | 64 | mpteq2dva 5249 |
. . . . . 6
β’ (β€
β (π₯ β β
β¦ ((2 Β· π₯) /
2)) = (π₯ β β
β¦ π₯)) |
66 | 60, 65 | eqtrd 2773 |
. . . . 5
β’ (β€
β (β D (π₯ β
β β¦ ((π₯β2)
/ 2))) = (π₯ β β
β¦ π₯)) |
67 | | oveq1 7416 |
. . . . . 6
β’ (π₯ = (logβπ¦) β (π₯β2) = ((logβπ¦)β2)) |
68 | 67 | oveq1d 7424 |
. . . . 5
β’ (π₯ = (logβπ¦) β ((π₯β2) / 2) = (((logβπ¦)β2) / 2)) |
69 | | id 22 |
. . . . 5
β’ (π₯ = (logβπ¦) β π₯ = (logβπ¦)) |
70 | 26, 28, 29, 30, 33, 34, 44, 66, 68, 69 | dvmptco 25489 |
. . . 4
β’ (β€
β (β D (π¦ β
β+ β¦ (((logβπ¦)β2) / 2))) = (π¦ β β+ β¦
((logβπ¦) Β· (1
/ π¦)))) |
71 | | rpcn 12984 |
. . . . . . 7
β’ (π¦ β β+
β π¦ β
β) |
72 | 71 | adantl 483 |
. . . . . 6
β’
((β€ β§ π¦
β β+) β π¦ β β) |
73 | | rpne0 12990 |
. . . . . . 7
β’ (π¦ β β+
β π¦ β
0) |
74 | 73 | adantl 483 |
. . . . . 6
β’
((β€ β§ π¦
β β+) β π¦ β 0) |
75 | 29, 72, 74 | divrecd 11993 |
. . . . 5
β’
((β€ β§ π¦
β β+) β ((logβπ¦) / π¦) = ((logβπ¦) Β· (1 / π¦))) |
76 | 75 | mpteq2dva 5249 |
. . . 4
β’ (β€
β (π¦ β
β+ β¦ ((logβπ¦) / π¦)) = (π¦ β β+ β¦
((logβπ¦) Β· (1
/ π¦)))) |
77 | 70, 76 | eqtr4d 2776 |
. . 3
β’ (β€
β (β D (π¦ β
β+ β¦ (((logβπ¦)β2) / 2))) = (π¦ β β+ β¦
((logβπ¦) / π¦))) |
78 | | fveq2 6892 |
. . . 4
β’ (π¦ = π β (logβπ¦) = (logβπ)) |
79 | | id 22 |
. . . 4
β’ (π¦ = π β π¦ = π) |
80 | 78, 79 | oveq12d 7427 |
. . 3
β’ (π¦ = π β ((logβπ¦) / π¦) = ((logβπ) / π)) |
81 | | simp3r 1203 |
. . . 4
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π¦ β€ π) |
82 | | simp2l 1200 |
. . . . . 6
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π¦ β β+) |
83 | 82 | rpred 13016 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π¦ β β) |
84 | | simp3l 1202 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β e β€ π¦) |
85 | | simp2r 1201 |
. . . . . 6
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π β β+) |
86 | 85 | rpred 13016 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π β β) |
87 | 5 | a1i 11 |
. . . . . 6
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β e β β) |
88 | 87, 83, 86, 84, 81 | letrd 11371 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β e β€ π) |
89 | | logdivle 26130 |
. . . . 5
β’ (((π¦ β β β§ e β€
π¦) β§ (π β β β§ e β€
π)) β (π¦ β€ π β ((logβπ) / π) β€ ((logβπ¦) / π¦))) |
90 | 83, 84, 86, 88, 89 | syl22anc 838 |
. . . 4
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β (π¦ β€ π β ((logβπ) / π) β€ ((logβπ¦) / π¦))) |
91 | 81, 90 | mpbid 231 |
. . 3
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β ((logβπ) / π) β€ ((logβπ¦) / π¦)) |
92 | | logdivsum.1 |
. . 3
β’ πΉ = (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))((logβπ) / π) β (((logβπ¦)β2) / 2))) |
93 | 71 | cxp1d 26214 |
. . . . . 6
β’ (π¦ β β+
β (π¦βπ1) = π¦) |
94 | 93 | oveq2d 7425 |
. . . . 5
β’ (π¦ β β+
β ((logβπ¦) /
(π¦βπ1)) =
((logβπ¦) / π¦)) |
95 | 94 | mpteq2ia 5252 |
. . . 4
β’ (π¦ β β+
β¦ ((logβπ¦) /
(π¦βπ1))) = (π¦ β β+
β¦ ((logβπ¦) /
π¦)) |
96 | | 1rp 12978 |
. . . . 5
β’ 1 β
β+ |
97 | | cxploglim 26482 |
. . . . 5
β’ (1 β
β+ β (π¦ β β+ β¦
((logβπ¦) / (π¦βπ1)))
βπ 0) |
98 | 96, 97 | mp1i 13 |
. . . 4
β’ (β€
β (π¦ β
β+ β¦ ((logβπ¦) / (π¦βπ1)))
βπ 0) |
99 | 95, 98 | eqbrtrrid 5185 |
. . 3
β’ (β€
β (π¦ β
β+ β¦ ((logβπ¦) / π¦)) βπ
0) |
100 | | fveq2 6892 |
. . . 4
β’ (π¦ = π΄ β (logβπ¦) = (logβπ΄)) |
101 | | id 22 |
. . . 4
β’ (π¦ = π΄ β π¦ = π΄) |
102 | 100, 101 | oveq12d 7427 |
. . 3
β’ (π¦ = π΄ β ((logβπ¦) / π¦) = ((logβπ΄) / π΄)) |
103 | 2, 3, 4, 6, 14, 15, 19, 22, 24, 77, 80, 91, 92, 99, 102 | dvfsumrlim3 25550 |
. 2
β’ (β€
β (πΉ:β+βΆβ β§
πΉ β dom
βπ β§ ((πΉ βπ πΏ β§ π΄ β β+ β§ e β€
π΄) β
(absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄)))) |
104 | 103 | mptru 1549 |
1
β’ (πΉ:β+βΆβ β§
πΉ β dom
βπ β§ ((πΉ βπ πΏ β§ π΄ β β+ β§ e β€
π΄) β
(absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄))) |