Step | Hyp | Ref
| Expression |
1 | | ioorp 13351 |
. . . 4
β’
(0(,)+β) = β+ |
2 | 1 | eqcomi 2742 |
. . 3
β’
β+ = (0(,)+β) |
3 | | logdivsqrle.a |
. . 3
β’ (π β π΄ β
β+) |
4 | | logdivsqrle.b |
. . 3
β’ (π β π΅ β
β+) |
5 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
6 | 5 | relogcld 26001 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
7 | 5 | rpsqrtcld 15305 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β+) |
8 | 7 | rpred 12965 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
9 | | rpsqrtcl 15158 |
. . . . . . 7
β’ (π₯ β β+
β (ββπ₯)
β β+) |
10 | | rpne0 12939 |
. . . . . . 7
β’
((ββπ₯)
β β+ β (ββπ₯) β 0) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (π₯ β β+
β (ββπ₯)
β 0) |
12 | 11 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
0) |
13 | 6, 8, 12 | redivcld 11991 |
. . . 4
β’ ((π β§ π₯ β β+) β
((logβπ₯) /
(ββπ₯)) β
β) |
14 | 13 | fmpttd 7067 |
. . 3
β’ (π β (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))):β+βΆβ) |
15 | | rpcn 12933 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β) |
16 | 15 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β π₯ β
β) |
17 | | rpne0 12939 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
0) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β π₯ β 0) |
19 | 16, 18 | logcld 25949 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
20 | 16 | sqrtcld 15331 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
21 | 19, 20, 12 | divrecd 11942 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((logβπ₯) /
(ββπ₯)) =
((logβπ₯) Β· (1
/ (ββπ₯)))) |
22 | | 2cnd 12239 |
. . . . . . . . . . . . 13
β’ (π β 2 β
β) |
23 | 22 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β 2 β
β) |
24 | | 2ne0 12265 |
. . . . . . . . . . . . 13
β’ 2 β
0 |
25 | 24 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β 2 β
0) |
26 | 23, 25 | reccld 11932 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (1 / 2)
β β) |
27 | 16, 18, 26 | cxpnegd 26093 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π₯βπ-(1 /
2)) = (1 / (π₯βπ(1 /
2)))) |
28 | | cxpsqrt 26081 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯βπ(1 /
2)) = (ββπ₯)) |
29 | 16, 28 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (π₯βπ(1 /
2)) = (ββπ₯)) |
30 | 29 | oveq2d 7377 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (1 /
(π₯βπ(1 / 2))) = (1 /
(ββπ₯))) |
31 | 27, 30 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (π₯βπ-(1 /
2)) = (1 / (ββπ₯))) |
32 | 31 | oveq2d 7377 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β·
(π₯βπ-(1 / 2))) =
((logβπ₯) Β· (1
/ (ββπ₯)))) |
33 | 21, 32 | eqtr4d 2776 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((logβπ₯) /
(ββπ₯)) =
((logβπ₯) Β·
(π₯βπ-(1 /
2)))) |
34 | 33 | mpteq2dva 5209 |
. . . . . 6
β’ (π β (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))) =
(π₯ β
β+ β¦ ((logβπ₯) Β· (π₯βπ-(1 /
2))))) |
35 | 34 | oveq2d 7377 |
. . . . 5
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯)))) =
(β D (π₯ β
β+ β¦ ((logβπ₯) Β· (π₯βπ-(1 /
2)))))) |
36 | | reelprrecn 11151 |
. . . . . . 7
β’ β
β {β, β} |
37 | 36 | a1i 11 |
. . . . . 6
β’ (π β β β {β,
β}) |
38 | 5 | rpreccld 12975 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β+) |
39 | | logf1o 25943 |
. . . . . . . . . . 11
β’
log:(β β {0})β1-1-ontoβran
log |
40 | | f1of 6788 |
. . . . . . . . . . 11
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})βΆran log) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . 10
β’
log:(β β {0})βΆran log |
42 | 41 | a1i 11 |
. . . . . . . . 9
β’ (π β log:(β β
{0})βΆran log) |
43 | 15 | ssriv 3952 |
. . . . . . . . . . 11
β’
β+ β β |
44 | | 0nrp 12958 |
. . . . . . . . . . 11
β’ Β¬ 0
β β+ |
45 | | ssdifsn 4752 |
. . . . . . . . . . 11
β’
(β+ β (β β {0}) β
(β+ β β β§ Β¬ 0 β
β+)) |
46 | 43, 44, 45 | mpbir2an 710 |
. . . . . . . . . 10
β’
β+ β (β β {0}) |
47 | 46 | a1i 11 |
. . . . . . . . 9
β’ (π β β+
β (β β {0})) |
48 | 42, 47 | feqresmpt 6915 |
. . . . . . . 8
β’ (π β (log βΎ
β+) = (π₯
β β+ β¦ (logβπ₯))) |
49 | 48 | oveq2d 7377 |
. . . . . . 7
β’ (π β (β D (log βΎ
β+)) = (β D (π₯ β β+ β¦
(logβπ₯)))) |
50 | | dvrelog 26015 |
. . . . . . 7
β’ (β
D (log βΎ β+)) = (π₯ β β+ β¦ (1 /
π₯)) |
51 | 49, 50 | eqtr3di 2788 |
. . . . . 6
β’ (π β (β D (π₯ β β+
β¦ (logβπ₯))) =
(π₯ β
β+ β¦ (1 / π₯))) |
52 | | 1cnd 11158 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
53 | 52 | halfcld 12406 |
. . . . . . . . 9
β’ (π β (1 / 2) β
β) |
54 | 53 | negcld 11507 |
. . . . . . . 8
β’ (π β -(1 / 2) β
β) |
55 | 54 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β -(1 / 2)
β β) |
56 | 16, 55 | cxpcld 26086 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (π₯βπ-(1 /
2)) β β) |
57 | 52 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β 1 β
β) |
58 | 55, 57 | subcld 11520 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (-(1 / 2)
β 1) β β) |
59 | 16, 58 | cxpcld 26086 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (π₯βπ(-(1 /
2) β 1)) β β) |
60 | 55, 59 | mulcld 11183 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (-(1 / 2)
Β· (π₯βπ(-(1 / 2) β
1))) β β) |
61 | | dvcxp1 26116 |
. . . . . . 7
β’ (-(1 / 2)
β β β (β D (π₯ β β+ β¦ (π₯βπ-(1 /
2)))) = (π₯ β
β+ β¦ (-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))))) |
62 | 54, 61 | syl 17 |
. . . . . 6
β’ (π β (β D (π₯ β β+
β¦ (π₯βπ-(1 / 2)))) =
(π₯ β
β+ β¦ (-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))))) |
63 | 37, 19, 38, 51, 56, 60, 62 | dvmptmul 25348 |
. . . . 5
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯)
Β· (π₯βπ-(1 / 2))))) =
(π₯ β
β+ β¦ (((1 / π₯) Β· (π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))) |
64 | 35, 63 | eqtrd 2773 |
. . . 4
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯)))) =
(π₯ β
β+ β¦ (((1 / π₯) Β· (π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))) |
65 | | ax-resscn 11116 |
. . . . . 6
β’ β
β β |
66 | 65 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
67 | | eqid 2733 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
68 | 67 | addcn 24251 |
. . . . . . 7
β’ + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
69 | 68 | a1i 11 |
. . . . . 6
β’ (π β + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
70 | 43 | a1i 11 |
. . . . . . . . 9
β’ (π β β+
β β) |
71 | | ssid 3970 |
. . . . . . . . . 10
β’ β
β β |
72 | 71 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β) |
73 | | cncfmptc 24298 |
. . . . . . . . 9
β’ ((1
β β β§ β+ β β β§ β β
β) β (π₯ β
β+ β¦ 1) β (β+βcnββ)) |
74 | 52, 70, 72, 73 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ 1) β
(β+βcnββ)) |
75 | | difss 4095 |
. . . . . . . . 9
β’ (β
β {0}) β β |
76 | | cncfmptid 24299 |
. . . . . . . . 9
β’
((β+ β (β β {0}) β§ (β
β {0}) β β) β (π₯ β β+ β¦ π₯) β
(β+βcnβ(β β {0}))) |
77 | 47, 75, 76 | sylancl 587 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ π₯) β
(β+βcnβ(β β {0}))) |
78 | 74, 77 | divcncf 24834 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (1 /
π₯)) β
(β+βcnββ)) |
79 | | ax-1 6 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (π₯ β β
β π₯ β
β+)) |
80 | 15, 79 | jca 513 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ β β
β§ (π₯ β β
β π₯ β
β+))) |
81 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (β
β (-β(,]0)) = (β β (-β(,]0)) |
82 | 81 | ellogdm 26017 |
. . . . . . . . . . 11
β’ (π₯ β (β β
(-β(,]0)) β (π₯
β β β§ (π₯
β β β π₯
β β+))) |
83 | 80, 82 | sylibr 233 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β (β
β (-β(,]0))) |
84 | 83 | ssriv 3952 |
. . . . . . . . 9
β’
β+ β (β β
(-β(,]0)) |
85 | 84 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β (β β (-β(,]0))) |
86 | 54, 85 | cxpcncf1 33272 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (π₯βπ-(1 /
2))) β (β+βcnββ)) |
87 | 78, 86 | mulcncf 24833 |
. . . . . 6
β’ (π β (π₯ β β+ β¦ ((1 /
π₯) Β· (π₯βπ-(1 /
2)))) β (β+βcnββ)) |
88 | | cncfmptc 24298 |
. . . . . . . . 9
β’ ((-(1 /
2) β β β§ β+ β β β§ β
β β) β (π₯
β β+ β¦ -(1 / 2)) β
(β+βcnββ)) |
89 | 54, 70, 72, 88 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ -(1 / 2))
β (β+βcnββ)) |
90 | 54, 52 | subcld 11520 |
. . . . . . . . 9
β’ (π β (-(1 / 2) β 1)
β β) |
91 | 90, 85 | cxpcncf1 33272 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ (π₯βπ(-(1 /
2) β 1))) β (β+βcnββ)) |
92 | 89, 91 | mulcncf 24833 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (-(1 / 2)
Β· (π₯βπ(-(1 / 2) β
1)))) β (β+βcnββ)) |
93 | | cncfss 24285 |
. . . . . . . . 9
β’ ((β
β β β§ β β β) β
(β+βcnββ) β
(β+βcnββ)) |
94 | 65, 71, 93 | mp2an 691 |
. . . . . . . 8
β’
(β+βcnββ) β
(β+βcnββ) |
95 | | relogcn 26016 |
. . . . . . . . 9
β’ (log
βΎ β+) β (β+βcnββ) |
96 | 48, 95 | eqeltrrdi 2843 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦
(logβπ₯)) β
(β+βcnββ)) |
97 | 94, 96 | sselid 3946 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦
(logβπ₯)) β
(β+βcnββ)) |
98 | 92, 97 | mulcncf 24833 |
. . . . . 6
β’ (π β (π₯ β β+ β¦ ((-(1 /
2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) β (β+βcnββ)) |
99 | 67, 69, 87, 98 | cncfmpt2f 24301 |
. . . . 5
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) |
100 | | rpre 12931 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β
β) |
101 | 100, 17 | rereccld 11990 |
. . . . . . . . 9
β’ (π₯ β β+
β (1 / π₯) β
β) |
102 | | rpge0 12936 |
. . . . . . . . . 10
β’ (π₯ β β+
β 0 β€ π₯) |
103 | | halfre 12375 |
. . . . . . . . . . . 12
β’ (1 / 2)
β β |
104 | 103 | renegcli 11470 |
. . . . . . . . . . 11
β’ -(1 / 2)
β β |
105 | 104 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β β+
β -(1 / 2) β β) |
106 | 100, 102,
105 | recxpcld 26101 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯βπ-(1 / 2)) β
β) |
107 | 101, 106 | remulcld 11193 |
. . . . . . . 8
β’ (π₯ β β+
β ((1 / π₯) Β·
(π₯βπ-(1 / 2))) β
β) |
108 | | 1re 11163 |
. . . . . . . . . . . . 13
β’ 1 β
β |
109 | 104, 108 | resubcli 11471 |
. . . . . . . . . . . 12
β’ (-(1 / 2)
β 1) β β |
110 | 109 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (-(1 / 2) β 1) β β) |
111 | 100, 102,
110 | recxpcld 26101 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯βπ(-(1 / 2) β
1)) β β) |
112 | 105, 111 | remulcld 11193 |
. . . . . . . . 9
β’ (π₯ β β+
β (-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) β β) |
113 | | relogcl 25954 |
. . . . . . . . 9
β’ (π₯ β β+
β (logβπ₯) β
β) |
114 | 112, 113 | remulcld 11193 |
. . . . . . . 8
β’ (π₯ β β+
β ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)) β β) |
115 | 107, 114 | readdcld 11192 |
. . . . . . 7
β’ (π₯ β β+
β (((1 / π₯) Β·
(π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) β β) |
116 | 115 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) β β) |
117 | 116 | fmpttd 7067 |
. . . . 5
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))):β+βΆβ) |
118 | | cncfcdm 24284 |
. . . . . 6
β’ ((β
β β β§ (π₯
β β+ β¦ (((1 / π₯) Β· (π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ) β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))):β+βΆβ)) |
119 | 118 | biimpar 479 |
. . . . 5
β’
(((β β β β§ (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) β§ (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))):β+βΆβ)
β (π₯ β
β+ β¦ (((1 / π₯) Β· (π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) |
120 | 66, 99, 117, 119 | syl21anc 837 |
. . . 4
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) |
121 | 64, 120 | eqeltrd 2834 |
. . 3
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯)))) β
(β+βcnββ)) |
122 | | logdivsqrle.2 |
. . 3
β’ (π β π΄ β€ π΅) |
123 | 64 | fveq1d 6848 |
. . . . 5
β’ (π β ((β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯))))βπ¦) = ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦)) |
124 | 123 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((β D (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))))βπ¦) = ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦)) |
125 | 57 | negcld 11507 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β -1 β
β) |
126 | | cxpadd 26057 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π₯ β 0) β§ -(1 / 2) β
β β§ -1 β β) β (π₯βπ(-(1 / 2) + -1)) =
((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
127 | 16, 18, 55, 125, 126 | syl211anc 1377 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (π₯βπ(-(1 /
2) + -1)) = ((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
128 | 59 | mulid2d 11181 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (1
Β· (π₯βπ(-(1 / 2) β
1))) = (π₯βπ(-(1 / 2) β
1))) |
129 | 55, 57 | negsubd 11526 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (-(1 / 2)
+ -1) = (-(1 / 2) β 1)) |
130 | 129 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (π₯βπ(-(1 /
2) + -1)) = (π₯βπ(-(1 / 2) β
1))) |
131 | 128, 130 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (1
Β· (π₯βπ(-(1 / 2) β
1))) = (π₯βπ(-(1 / 2) +
-1))) |
132 | 43, 38 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β) |
133 | 132, 56 | mulcomd 11184 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β ((1 /
π₯) Β· (π₯βπ-(1 /
2))) = ((π₯βπ-(1 / 2)) Β·
(1 / π₯))) |
134 | | cxpneg 26059 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π₯ β 0 β§ 1 β β)
β (π₯βπ-1) = (1 / (π₯βπ1))) |
135 | 16, 18, 57, 134 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (π₯βπ-1) =
(1 / (π₯βπ1))) |
136 | 16 | cxp1d 26084 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β (π₯βπ1) =
π₯) |
137 | 136 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (1 /
(π₯βπ1)) = (1 / π₯)) |
138 | 135, 137 | eqtr2d 2774 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (1 /
π₯) = (π₯βπ-1)) |
139 | 138 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β ((π₯βπ-(1 /
2)) Β· (1 / π₯)) =
((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
140 | 133, 139 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β ((1 /
π₯) Β· (π₯βπ-(1 /
2))) = ((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
141 | 127, 131,
140 | 3eqtr4rd 2784 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β ((1 /
π₯) Β· (π₯βπ-(1 /
2))) = (1 Β· (π₯βπ(-(1 / 2) β
1)))) |
142 | 55, 59, 19 | mul32d 11373 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β ((-(1 /
2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)) = ((-(1 / 2) Β· (logβπ₯)) Β· (π₯βπ(-(1 / 2) β
1)))) |
143 | 141, 142 | oveq12d 7379 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) = ((1 Β· (π₯βπ(-(1 / 2) β
1))) + ((-(1 / 2) Β· (logβπ₯)) Β· (π₯βπ(-(1 / 2) β
1))))) |
144 | 55, 19 | mulcld 11183 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (-(1 / 2)
Β· (logβπ₯))
β β) |
145 | 57, 144, 59 | adddird 11188 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))) = ((1 Β· (π₯βπ(-(1 / 2) β
1))) + ((-(1 / 2) Β· (logβπ₯)) Β· (π₯βπ(-(1 / 2) β
1))))) |
146 | 143, 145 | eqtr4d 2776 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) = ((1 + (-(1 / 2) Β·
(logβπ₯))) Β·
(π₯βπ(-(1 / 2) β
1)))) |
147 | 146 | mpteq2dva 5209 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) = (π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))) |
148 | 147 | fveq1d 6848 |
. . . . . 6
β’ (π β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦) = ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦)) |
149 | 148 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦) = ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦)) |
150 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1)))) = (π₯ β
β+ β¦ ((1 + (-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))) |
151 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β π₯ = π¦) |
152 | 151 | fveq2d 6850 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (logβπ₯) = (logβπ¦)) |
153 | 152 | oveq2d 7377 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (-(1 / 2) Β· (logβπ₯)) = (-(1 / 2) Β·
(logβπ¦))) |
154 | 153 | oveq2d 7377 |
. . . . . . . 8
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (1 + (-(1 / 2) Β·
(logβπ₯))) = (1 + (-(1
/ 2) Β· (logβπ¦)))) |
155 | 151 | oveq1d 7376 |
. . . . . . . 8
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (π₯βπ(-(1 / 2) β
1)) = (π¦βπ(-(1 / 2) β
1))) |
156 | 154, 155 | oveq12d 7379 |
. . . . . . 7
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β ((1 + (-(1 / 2) Β·
(logβπ₯))) Β·
(π₯βπ(-(1 / 2) β
1))) = ((1 + (-(1 / 2) Β· (logβπ¦))) Β· (π¦βπ(-(1 / 2) β
1)))) |
157 | | ioossicc 13359 |
. . . . . . . . . 10
β’ (π΄(,)π΅) β (π΄[,]π΅) |
158 | 157 | a1i 11 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
159 | 2, 3, 4 | fct2relem 33274 |
. . . . . . . . 9
β’ (π β (π΄[,]π΅) β
β+) |
160 | 158, 159 | sstrd 3958 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β
β+) |
161 | 160 | sselda 3948 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β+) |
162 | | ovexd 7396 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) Β·
(π¦βπ(-(1 / 2) β
1))) β V) |
163 | 150, 156,
161, 162 | fvmptd 6959 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦) = ((1 + (-(1
/ 2) Β· (logβπ¦))) Β· (π¦βπ(-(1 / 2) β
1)))) |
164 | 108 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β β) |
165 | 104 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β -(1 / 2) β
β) |
166 | 161 | relogcld 26001 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β (logβπ¦) β β) |
167 | 165, 166 | remulcld 11193 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (-(1 / 2) Β·
(logβπ¦)) β
β) |
168 | 164, 167 | readdcld 11192 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 + (-(1 / 2) Β·
(logβπ¦))) β
β) |
169 | | 0red 11166 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β β) |
170 | | rpcxpcl 26054 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ (-(1 / 2) β 1) β β) β (π¦βπ(-(1 / 2) β
1)) β β+) |
171 | 161, 109,
170 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦βπ(-(1 / 2) β
1)) β β+) |
172 | 171 | rpred 12965 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦βπ(-(1 / 2) β
1)) β β) |
173 | 171 | rpge0d 12969 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β€ (π¦βπ(-(1 / 2) β
1))) |
174 | | 2cn 12236 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
175 | 174 | mulid2i 11168 |
. . . . . . . . . . . . 13
β’ (1
Β· 2) = 2 |
176 | | 2re 12235 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β β) |
178 | 177 | reefcld 15978 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β
β) |
179 | 3 | rpred 12965 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β β) |
180 | 179 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β β) |
181 | 161 | rpred 12965 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β) |
182 | | logdivsqrle.1 |
. . . . . . . . . . . . . . . . 17
β’ (π β (expβ2) β€ π΄) |
183 | 182 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β€ π΄) |
184 | | eliooord 13332 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (π΄(,)π΅) β (π΄ < π¦ β§ π¦ < π΅)) |
185 | 184 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (π΄(,)π΅) β π΄ < π¦) |
186 | 185 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ < π¦) |
187 | 180, 181,
186 | ltled 11311 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β€ π¦) |
188 | 178, 180,
181, 183, 187 | letrd 11320 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β€ π¦) |
189 | | reeflog 25959 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β+
β (expβ(logβπ¦)) = π¦) |
190 | 161, 189 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ(logβπ¦)) = π¦) |
191 | 188, 190 | breqtrrd 5137 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β€
(expβ(logβπ¦))) |
192 | | efle 16008 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ (logβπ¦) β β) β (2 β€
(logβπ¦) β
(expβ2) β€ (expβ(logβπ¦)))) |
193 | 176, 166,
192 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (π΄(,)π΅)) β (2 β€ (logβπ¦) β (expβ2) β€
(expβ(logβπ¦)))) |
194 | 191, 193 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β€ (logβπ¦)) |
195 | 175, 194 | eqbrtrid 5144 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 Β· 2) β€
(logβπ¦)) |
196 | | 2rp 12928 |
. . . . . . . . . . . . . 14
β’ 2 β
β+ |
197 | 196 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β
β+) |
198 | 164, 166,
197 | lemuldivd 13014 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 Β· 2) β€
(logβπ¦) β 1 β€
((logβπ¦) /
2))) |
199 | 195, 198 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β€ ((logβπ¦) / 2)) |
200 | 65, 166 | sselid 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (logβπ¦) β β) |
201 | 22 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β β) |
202 | 24 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β 0) |
203 | 200, 201,
202 | divrec2d 11943 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((logβπ¦) / 2) = ((1 / 2) Β· (logβπ¦))) |
204 | 199, 203 | breqtrd 5135 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β€ ((1 / 2) Β·
(logβπ¦))) |
205 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 / 2) β
β) |
206 | 205, 200 | mulneg1d 11616 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (-(1 / 2) Β·
(logβπ¦)) = -((1 / 2)
Β· (logβπ¦))) |
207 | 206 | oveq2d 7377 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 β (-(1 / 2) Β·
(logβπ¦))) = (0
β -((1 / 2) Β· (logβπ¦)))) |
208 | 65, 169 | sselid 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β β) |
209 | 205, 200 | mulcld 11183 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 / 2) Β· (logβπ¦)) β
β) |
210 | 208, 209 | subnegd 11527 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 β -((1 / 2) Β·
(logβπ¦))) = (0 + ((1
/ 2) Β· (logβπ¦)))) |
211 | 209 | addid2d 11364 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 + ((1 / 2) Β·
(logβπ¦))) = ((1 / 2)
Β· (logβπ¦))) |
212 | 207, 210,
211 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 β (-(1 / 2) Β·
(logβπ¦))) = ((1 / 2)
Β· (logβπ¦))) |
213 | 204, 212 | breqtrrd 5137 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β€ (0 β (-(1 / 2)
Β· (logβπ¦)))) |
214 | | leaddsub 11639 |
. . . . . . . . . 10
β’ ((1
β β β§ (-(1 / 2) Β· (logβπ¦)) β β β§ 0 β β)
β ((1 + (-(1 / 2) Β· (logβπ¦))) β€ 0 β 1 β€ (0 β (-(1 / 2)
Β· (logβπ¦))))) |
215 | 164, 167,
169, 214 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) β€ 0
β 1 β€ (0 β (-(1 / 2) Β· (logβπ¦))))) |
216 | 213, 215 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 + (-(1 / 2) Β·
(logβπ¦))) β€
0) |
217 | 168, 169,
172, 173, 216 | lemul1ad 12102 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) Β·
(π¦βπ(-(1 / 2) β
1))) β€ (0 Β· (π¦βπ(-(1 / 2) β
1)))) |
218 | 43, 171 | sselid 3946 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦βπ(-(1 / 2) β
1)) β β) |
219 | 218 | mul02d 11361 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 Β· (π¦βπ(-(1 / 2) β
1))) = 0) |
220 | 217, 219 | breqtrd 5135 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) Β·
(π¦βπ(-(1 / 2) β
1))) β€ 0) |
221 | 163, 220 | eqbrtrd 5131 |
. . . . 5
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦) β€
0) |
222 | 149, 221 | eqbrtrd 5131 |
. . . 4
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦) β€ 0) |
223 | 124, 222 | eqbrtrd 5131 |
. . 3
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((β D (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))))βπ¦) β€ 0) |
224 | 2, 3, 4, 14, 121, 122, 223 | fdvnegge 33279 |
. 2
β’ (π β ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΅) β€ ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΄)) |
225 | | eqidd 2734 |
. . 3
β’ (π β (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))) =
(π₯ β
β+ β¦ ((logβπ₯) / (ββπ₯)))) |
226 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ = π΅) β π₯ = π΅) |
227 | 226 | fveq2d 6850 |
. . . 4
β’ ((π β§ π₯ = π΅) β (logβπ₯) = (logβπ΅)) |
228 | 226 | fveq2d 6850 |
. . . 4
β’ ((π β§ π₯ = π΅) β (ββπ₯) = (ββπ΅)) |
229 | 227, 228 | oveq12d 7379 |
. . 3
β’ ((π β§ π₯ = π΅) β ((logβπ₯) / (ββπ₯)) = ((logβπ΅) / (ββπ΅))) |
230 | | ovex 7394 |
. . . 4
β’
((logβπ΅) /
(ββπ΅)) β
V |
231 | 230 | a1i 11 |
. . 3
β’ (π β ((logβπ΅) / (ββπ΅)) β V) |
232 | 225, 229,
4, 231 | fvmptd 6959 |
. 2
β’ (π β ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΅) = ((logβπ΅) / (ββπ΅))) |
233 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ = π΄) β π₯ = π΄) |
234 | 233 | fveq2d 6850 |
. . . 4
β’ ((π β§ π₯ = π΄) β (logβπ₯) = (logβπ΄)) |
235 | 233 | fveq2d 6850 |
. . . 4
β’ ((π β§ π₯ = π΄) β (ββπ₯) = (ββπ΄)) |
236 | 234, 235 | oveq12d 7379 |
. . 3
β’ ((π β§ π₯ = π΄) β ((logβπ₯) / (ββπ₯)) = ((logβπ΄) / (ββπ΄))) |
237 | | ovex 7394 |
. . . 4
β’
((logβπ΄) /
(ββπ΄)) β
V |
238 | 237 | a1i 11 |
. . 3
β’ (π β ((logβπ΄) / (ββπ΄)) β V) |
239 | 225, 236,
3, 238 | fvmptd 6959 |
. 2
β’ (π β ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΄) = ((logβπ΄) / (ββπ΄))) |
240 | 224, 232,
239 | 3brtr3d 5140 |
1
β’ (π β ((logβπ΅) / (ββπ΅)) β€ ((logβπ΄) / (ββπ΄))) |