Step | Hyp | Ref
| Expression |
1 | | ioorp 13406 |
. . . 4
β’
(0(,)+β) = β+ |
2 | 1 | eqcomi 2739 |
. . 3
β’
β+ = (0(,)+β) |
3 | | nnuz 12869 |
. . 3
β’ β =
(β€β₯β1) |
4 | | 1zzd 12597 |
. . 3
β’ (β€
β 1 β β€) |
5 | | ere 16036 |
. . . 4
β’ e β
β |
6 | 5 | a1i 11 |
. . 3
β’ (β€
β e β β) |
7 | | 0re 11220 |
. . . . . 6
β’ 0 β
β |
8 | | epos 16154 |
. . . . . 6
β’ 0 <
e |
9 | 7, 5, 8 | ltleii 11341 |
. . . . 5
β’ 0 β€
e |
10 | 9 | a1i 11 |
. . . 4
β’ (β€
β 0 β€ e) |
11 | | 1re 11218 |
. . . . 5
β’ 1 β
β |
12 | | addge02 11729 |
. . . . 5
β’ ((1
β β β§ e β β) β (0 β€ e β 1 β€ (e +
1))) |
13 | 11, 5, 12 | mp2an 688 |
. . . 4
β’ (0 β€ e
β 1 β€ (e + 1)) |
14 | 10, 13 | sylib 217 |
. . 3
β’ (β€
β 1 β€ (e + 1)) |
15 | 7 | a1i 11 |
. . 3
β’ (β€
β 0 β β) |
16 | | relogcl 26320 |
. . . . . 6
β’ (π¦ β β+
β (logβπ¦) β
β) |
17 | 16 | adantl 480 |
. . . . 5
β’
((β€ β§ π¦
β β+) β (logβπ¦) β β) |
18 | 17 | resqcld 14094 |
. . . 4
β’
((β€ β§ π¦
β β+) β ((logβπ¦)β2) β β) |
19 | 18 | rehalfcld 12463 |
. . 3
β’
((β€ β§ π¦
β β+) β (((logβπ¦)β2) / 2) β
β) |
20 | | rerpdivcl 13008 |
. . . . 5
β’
(((logβπ¦)
β β β§ π¦
β β+) β ((logβπ¦) / π¦) β β) |
21 | 16, 20 | mpancom 684 |
. . . 4
β’ (π¦ β β+
β ((logβπ¦) /
π¦) β
β) |
22 | 21 | adantl 480 |
. . 3
β’
((β€ β§ π¦
β β+) β ((logβπ¦) / π¦) β β) |
23 | | nnrp 12989 |
. . . 4
β’ (π¦ β β β π¦ β
β+) |
24 | 23, 22 | sylan2 591 |
. . 3
β’
((β€ β§ π¦
β β) β ((logβπ¦) / π¦) β β) |
25 | | reelprrecn 11204 |
. . . . . 6
β’ β
β {β, β} |
26 | 25 | a1i 11 |
. . . . 5
β’ (β€
β β β {β, β}) |
27 | | cnelprrecn 11205 |
. . . . . 6
β’ β
β {β, β} |
28 | 27 | a1i 11 |
. . . . 5
β’ (β€
β β β {β, β}) |
29 | 17 | recnd 11246 |
. . . . 5
β’
((β€ β§ π¦
β β+) β (logβπ¦) β β) |
30 | | ovexd 7446 |
. . . . 5
β’
((β€ β§ π¦
β β+) β (1 / π¦) β V) |
31 | | sqcl 14087 |
. . . . . . 7
β’ (π₯ β β β (π₯β2) β
β) |
32 | 31 | adantl 480 |
. . . . . 6
β’
((β€ β§ π₯
β β) β (π₯β2) β β) |
33 | 32 | halfcld 12461 |
. . . . 5
β’
((β€ β§ π₯
β β) β ((π₯β2) / 2) β
β) |
34 | | simpr 483 |
. . . . 5
β’
((β€ β§ π₯
β β) β π₯
β β) |
35 | | relogf1o 26311 |
. . . . . . . . . 10
β’ (log
βΎ β+):β+β1-1-ontoββ |
36 | | f1of 6832 |
. . . . . . . . . 10
β’ ((log
βΎ β+):β+β1-1-ontoββ β (log βΎ
β+):β+βΆβ) |
37 | 35, 36 | mp1i 13 |
. . . . . . . . 9
β’ (β€
β (log βΎ
β+):β+βΆβ) |
38 | 37 | feqmptd 6959 |
. . . . . . . 8
β’ (β€
β (log βΎ β+) = (π¦ β β+ β¦ ((log
βΎ β+)βπ¦))) |
39 | | fvres 6909 |
. . . . . . . . 9
β’ (π¦ β β+
β ((log βΎ β+)βπ¦) = (logβπ¦)) |
40 | 39 | mpteq2ia 5250 |
. . . . . . . 8
β’ (π¦ β β+
β¦ ((log βΎ β+)βπ¦)) = (π¦ β β+ β¦
(logβπ¦)) |
41 | 38, 40 | eqtrdi 2786 |
. . . . . . 7
β’ (β€
β (log βΎ β+) = (π¦ β β+ β¦
(logβπ¦))) |
42 | 41 | oveq2d 7427 |
. . . . . 6
β’ (β€
β (β D (log βΎ β+)) = (β D (π¦ β β+
β¦ (logβπ¦)))) |
43 | | dvrelog 26381 |
. . . . . 6
β’ (β
D (log βΎ β+)) = (π¦ β β+ β¦ (1 /
π¦)) |
44 | 42, 43 | eqtr3di 2785 |
. . . . 5
β’ (β€
β (β D (π¦ β
β+ β¦ (logβπ¦))) = (π¦ β β+ β¦ (1 /
π¦))) |
45 | | ovexd 7446 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (2 Β· π₯) β V) |
46 | | 2nn 12289 |
. . . . . . . . 9
β’ 2 β
β |
47 | | dvexp 25705 |
. . . . . . . . 9
β’ (2 β
β β (β D (π₯ β β β¦ (π₯β2))) = (π₯ β β β¦ (2 Β· (π₯β(2 β
1))))) |
48 | 46, 47 | mp1i 13 |
. . . . . . . 8
β’ (β€
β (β D (π₯ β
β β¦ (π₯β2))) = (π₯ β β β¦ (2 Β· (π₯β(2 β
1))))) |
49 | | 2m1e1 12342 |
. . . . . . . . . . . 12
β’ (2
β 1) = 1 |
50 | 49 | oveq2i 7422 |
. . . . . . . . . . 11
β’ (π₯β(2 β 1)) = (π₯β1) |
51 | | exp1 14037 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯β1) = π₯) |
52 | 51 | adantl 480 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β β) β (π₯β1) = π₯) |
53 | 50, 52 | eqtrid 2782 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β (π₯β(2 β 1)) = π₯) |
54 | 53 | oveq2d 7427 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (2 Β· (π₯β(2 β 1))) = (2 Β· π₯)) |
55 | 54 | mpteq2dva 5247 |
. . . . . . . 8
β’ (β€
β (π₯ β β
β¦ (2 Β· (π₯β(2 β 1)))) = (π₯ β β β¦ (2 Β· π₯))) |
56 | 48, 55 | eqtrd 2770 |
. . . . . . 7
β’ (β€
β (β D (π₯ β
β β¦ (π₯β2))) = (π₯ β β β¦ (2 Β· π₯))) |
57 | | 2cnd 12294 |
. . . . . . 7
β’ (β€
β 2 β β) |
58 | | 2ne0 12320 |
. . . . . . . 8
β’ 2 β
0 |
59 | 58 | a1i 11 |
. . . . . . 7
β’ (β€
β 2 β 0) |
60 | 28, 32, 45, 56, 57, 59 | dvmptdivc 25717 |
. . . . . 6
β’ (β€
β (β D (π₯ β
β β¦ ((π₯β2)
/ 2))) = (π₯ β β
β¦ ((2 Β· π₯) /
2))) |
61 | | 2cn 12291 |
. . . . . . . . 9
β’ 2 β
β |
62 | | divcan3 11902 |
. . . . . . . . 9
β’ ((π₯ β β β§ 2 β
β β§ 2 β 0) β ((2 Β· π₯) / 2) = π₯) |
63 | 61, 58, 62 | mp3an23 1451 |
. . . . . . . 8
β’ (π₯ β β β ((2
Β· π₯) / 2) = π₯) |
64 | 63 | adantl 480 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β ((2 Β· π₯) / 2) = π₯) |
65 | 64 | mpteq2dva 5247 |
. . . . . 6
β’ (β€
β (π₯ β β
β¦ ((2 Β· π₯) /
2)) = (π₯ β β
β¦ π₯)) |
66 | 60, 65 | eqtrd 2770 |
. . . . 5
β’ (β€
β (β D (π₯ β
β β¦ ((π₯β2)
/ 2))) = (π₯ β β
β¦ π₯)) |
67 | | oveq1 7418 |
. . . . . 6
β’ (π₯ = (logβπ¦) β (π₯β2) = ((logβπ¦)β2)) |
68 | 67 | oveq1d 7426 |
. . . . 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 25724 |
. . . 4
β’ (β€
β (β D (π¦ β
β+ β¦ (((logβπ¦)β2) / 2))) = (π¦ β β+ β¦
((logβπ¦) Β· (1
/ π¦)))) |
71 | | rpcn 12988 |
. . . . . . 7
β’ (π¦ β β+
β π¦ β
β) |
72 | 71 | adantl 480 |
. . . . . 6
β’
((β€ β§ π¦
β β+) β π¦ β β) |
73 | | rpne0 12994 |
. . . . . . 7
β’ (π¦ β β+
β π¦ β
0) |
74 | 73 | adantl 480 |
. . . . . 6
β’
((β€ β§ π¦
β β+) β π¦ β 0) |
75 | 29, 72, 74 | divrecd 11997 |
. . . . 5
β’
((β€ β§ π¦
β β+) β ((logβπ¦) / π¦) = ((logβπ¦) Β· (1 / π¦))) |
76 | 75 | mpteq2dva 5247 |
. . . 4
β’ (β€
β (π¦ β
β+ β¦ ((logβπ¦) / π¦)) = (π¦ β β+ β¦
((logβπ¦) Β· (1
/ π¦)))) |
77 | 70, 76 | eqtr4d 2773 |
. . 3
β’ (β€
β (β D (π¦ β
β+ β¦ (((logβπ¦)β2) / 2))) = (π¦ β β+ β¦
((logβπ¦) / π¦))) |
78 | | fveq2 6890 |
. . . 4
β’ (π¦ = π β (logβπ¦) = (logβπ)) |
79 | | id 22 |
. . . 4
β’ (π¦ = π β π¦ = π) |
80 | 78, 79 | oveq12d 7429 |
. . 3
β’ (π¦ = π β ((logβπ¦) / π¦) = ((logβπ) / π)) |
81 | | simp3r 1200 |
. . . 4
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π¦ β€ π) |
82 | | simp2l 1197 |
. . . . . 6
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π¦ β β+) |
83 | 82 | rpred 13020 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π¦ β β) |
84 | | simp3l 1199 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β e β€ π¦) |
85 | | simp2r 1198 |
. . . . . 6
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π β β+) |
86 | 85 | rpred 13020 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β π β β) |
87 | 5 | a1i 11 |
. . . . . 6
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β e β β) |
88 | 87, 83, 86, 84, 81 | letrd 11375 |
. . . . 5
β’
((β€ β§ (π¦
β β+ β§ π β β+) β§ (e β€
π¦ β§ π¦ β€ π)) β e β€ π) |
89 | | logdivle 26366 |
. . . . 5
β’ (((π¦ β β β§ e β€
π¦) β§ (π β β β§ e β€
π)) β (π¦ β€ π β ((logβπ) / π) β€ ((logβπ¦) / π¦))) |
90 | 83, 84, 86, 88, 89 | syl22anc 835 |
. . . 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 26450 |
. . . . . 6
β’ (π¦ β β+
β (π¦βπ1) = π¦) |
94 | 93 | oveq2d 7427 |
. . . . 5
β’ (π¦ β β+
β ((logβπ¦) /
(π¦βπ1)) =
((logβπ¦) / π¦)) |
95 | 94 | mpteq2ia 5250 |
. . . 4
β’ (π¦ β β+
β¦ ((logβπ¦) /
(π¦βπ1))) = (π¦ β β+
β¦ ((logβπ¦) /
π¦)) |
96 | | 1rp 12982 |
. . . . 5
β’ 1 β
β+ |
97 | | cxploglim 26718 |
. . . . 5
β’ (1 β
β+ β (π¦ β β+ β¦
((logβπ¦) / (π¦βπ1)))
βπ 0) |
98 | 96, 97 | mp1i 13 |
. . . 4
β’ (β€
β (π¦ β
β+ β¦ ((logβπ¦) / (π¦βπ1)))
βπ 0) |
99 | 95, 98 | eqbrtrrid 5183 |
. . 3
β’ (β€
β (π¦ β
β+ β¦ ((logβπ¦) / π¦)) βπ
0) |
100 | | fveq2 6890 |
. . . 4
β’ (π¦ = π΄ β (logβπ¦) = (logβπ΄)) |
101 | | id 22 |
. . . 4
β’ (π¦ = π΄ β π¦ = π΄) |
102 | 100, 101 | oveq12d 7429 |
. . 3
β’ (π¦ = π΄ β ((logβπ¦) / π¦) = ((logβπ΄) / π΄)) |
103 | 2, 3, 4, 6, 14, 15, 19, 22, 24, 77, 80, 91, 92, 99, 102 | dvfsumrlim3 25785 |
. 2
β’ (β€
β (πΉ:β+βΆβ β§
πΉ β dom
βπ β§ ((πΉ βπ πΏ β§ π΄ β β+ β§ e β€
π΄) β
(absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄)))) |
104 | 103 | mptru 1546 |
1
β’ (πΉ:β+βΆβ β§
πΉ β dom
βπ β§ ((πΉ βπ πΏ β§ π΄ β β+ β§ e β€
π΄) β
(absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄))) |