Step | Hyp | Ref
| Expression |
1 | | ioorp 13408 |
. . . 4
β’
(0(,)+β) = β+ |
2 | 1 | eqcomi 2735 |
. . 3
β’
β+ = (0(,)+β) |
3 | | logdivsqrle.a |
. . 3
β’ (π β π΄ β
β+) |
4 | | logdivsqrle.b |
. . 3
β’ (π β π΅ β
β+) |
5 | | simpr 484 |
. . . . . 6
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
6 | 5 | relogcld 26512 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
7 | 5 | rpsqrtcld 15364 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β+) |
8 | 7 | rpred 13022 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
9 | | rpsqrtcl 15217 |
. . . . . . 7
β’ (π₯ β β+
β (ββπ₯)
β β+) |
10 | | rpne0 12996 |
. . . . . . 7
β’
((ββπ₯)
β β+ β (ββπ₯) β 0) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (π₯ β β+
β (ββπ₯)
β 0) |
12 | 11 | adantl 481 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
0) |
13 | 6, 8, 12 | redivcld 12046 |
. . . 4
β’ ((π β§ π₯ β β+) β
((logβπ₯) /
(ββπ₯)) β
β) |
14 | 13 | fmpttd 7110 |
. . 3
β’ (π β (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))):β+βΆβ) |
15 | | rpcn 12990 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β) |
16 | 15 | adantl 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β π₯ β
β) |
17 | | rpne0 12996 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
0) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β π₯ β 0) |
19 | 16, 18 | logcld 26459 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
20 | 16 | sqrtcld 15390 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
21 | 19, 20, 12 | divrecd 11997 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((logβπ₯) /
(ββπ₯)) =
((logβπ₯) Β· (1
/ (ββπ₯)))) |
22 | | 2cnd 12294 |
. . . . . . . . . . . . 13
β’ (π β 2 β
β) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β 2 β
β) |
24 | | 2ne0 12320 |
. . . . . . . . . . . . 13
β’ 2 β
0 |
25 | 24 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β 2 β
0) |
26 | 23, 25 | reccld 11987 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (1 / 2)
β β) |
27 | 16, 18, 26 | cxpnegd 26604 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π₯βπ-(1 /
2)) = (1 / (π₯βπ(1 /
2)))) |
28 | | cxpsqrt 26592 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯βπ(1 /
2)) = (ββπ₯)) |
29 | 16, 28 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (π₯βπ(1 /
2)) = (ββπ₯)) |
30 | 29 | oveq2d 7421 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (1 /
(π₯βπ(1 / 2))) = (1 /
(ββπ₯))) |
31 | 27, 30 | eqtrd 2766 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (π₯βπ-(1 /
2)) = (1 / (ββπ₯))) |
32 | 31 | oveq2d 7421 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β·
(π₯βπ-(1 / 2))) =
((logβπ₯) Β· (1
/ (ββπ₯)))) |
33 | 21, 32 | eqtr4d 2769 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((logβπ₯) /
(ββπ₯)) =
((logβπ₯) Β·
(π₯βπ-(1 /
2)))) |
34 | 33 | mpteq2dva 5241 |
. . . . . 6
β’ (π β (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))) =
(π₯ β
β+ β¦ ((logβπ₯) Β· (π₯βπ-(1 /
2))))) |
35 | 34 | oveq2d 7421 |
. . . . 5
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯)))) =
(β D (π₯ β
β+ β¦ ((logβπ₯) Β· (π₯βπ-(1 /
2)))))) |
36 | | reelprrecn 11204 |
. . . . . . 7
β’ β
β {β, β} |
37 | 36 | a1i 11 |
. . . . . 6
β’ (π β β β {β,
β}) |
38 | 5 | rpreccld 13032 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β+) |
39 | | logf1o 26453 |
. . . . . . . . . . 11
β’
log:(β β {0})β1-1-ontoβran
log |
40 | | f1of 6827 |
. . . . . . . . . . 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 3981 |
. . . . . . . . . . 11
β’
β+ β β |
44 | | 0nrp 13015 |
. . . . . . . . . . 11
β’ Β¬ 0
β β+ |
45 | | ssdifsn 4786 |
. . . . . . . . . . 11
β’
(β+ β (β β {0}) β
(β+ β β β§ Β¬ 0 β
β+)) |
46 | 43, 44, 45 | mpbir2an 708 |
. . . . . . . . . 10
β’
β+ β (β β {0}) |
47 | 46 | a1i 11 |
. . . . . . . . 9
β’ (π β β+
β (β β {0})) |
48 | 42, 47 | feqresmpt 6955 |
. . . . . . . 8
β’ (π β (log βΎ
β+) = (π₯
β β+ β¦ (logβπ₯))) |
49 | 48 | oveq2d 7421 |
. . . . . . 7
β’ (π β (β D (log βΎ
β+)) = (β D (π₯ β β+ β¦
(logβπ₯)))) |
50 | | dvrelog 26526 |
. . . . . . 7
β’ (β
D (log βΎ β+)) = (π₯ β β+ β¦ (1 /
π₯)) |
51 | 49, 50 | eqtr3di 2781 |
. . . . . 6
β’ (π β (β D (π₯ β β+
β¦ (logβπ₯))) =
(π₯ β
β+ β¦ (1 / π₯))) |
52 | | 1cnd 11213 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
53 | 52 | halfcld 12461 |
. . . . . . . . 9
β’ (π β (1 / 2) β
β) |
54 | 53 | negcld 11562 |
. . . . . . . 8
β’ (π β -(1 / 2) β
β) |
55 | 54 | adantr 480 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β -(1 / 2)
β β) |
56 | 16, 55 | cxpcld 26597 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (π₯βπ-(1 /
2)) β β) |
57 | 52 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β 1 β
β) |
58 | 55, 57 | subcld 11575 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (-(1 / 2)
β 1) β β) |
59 | 16, 58 | cxpcld 26597 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (π₯βπ(-(1 /
2) β 1)) β β) |
60 | 55, 59 | mulcld 11238 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (-(1 / 2)
Β· (π₯βπ(-(1 / 2) β
1))) β β) |
61 | | dvcxp1 26629 |
. . . . . . 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 25848 |
. . . . 5
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯)
Β· (π₯βπ-(1 / 2))))) =
(π₯ β
β+ β¦ (((1 / π₯) Β· (π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))) |
64 | 35, 63 | eqtrd 2766 |
. . . 4
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯)))) =
(π₯ β
β+ β¦ (((1 / π₯) Β· (π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))) |
65 | | ax-resscn 11169 |
. . . . . 6
β’ β
β β |
66 | 65 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
67 | | eqid 2726 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
68 | 67 | addcn 24736 |
. . . . . . 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 3999 |
. . . . . . . . . 10
β’ β
β β |
72 | 71 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β) |
73 | | cncfmptc 24787 |
. . . . . . . . 9
β’ ((1
β β β§ β+ β β β§ β β
β) β (π₯ β
β+ β¦ 1) β (β+βcnββ)) |
74 | 52, 70, 72, 73 | syl3anc 1368 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ 1) β
(β+βcnββ)) |
75 | | difss 4126 |
. . . . . . . . 9
β’ (β
β {0}) β β |
76 | | cncfmptid 24788 |
. . . . . . . . 9
β’
((β+ β (β β {0}) β§ (β
β {0}) β β) β (π₯ β β+ β¦ π₯) β
(β+βcnβ(β β {0}))) |
77 | 47, 75, 76 | sylancl 585 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ π₯) β
(β+βcnβ(β β {0}))) |
78 | 74, 77 | divcncf 25331 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (1 /
π₯)) β
(β+βcnββ)) |
79 | | ax-1 6 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (π₯ β β
β π₯ β
β+)) |
80 | 15, 79 | jca 511 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ β β
β§ (π₯ β β
β π₯ β
β+))) |
81 | | eqid 2726 |
. . . . . . . . . . . 12
β’ (β
β (-β(,]0)) = (β β (-β(,]0)) |
82 | 81 | ellogdm 26528 |
. . . . . . . . . . 11
β’ (π₯ β (β β
(-β(,]0)) β (π₯
β β β§ (π₯
β β β π₯
β β+))) |
83 | 80, 82 | sylibr 233 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β (β
β (-β(,]0))) |
84 | 83 | ssriv 3981 |
. . . . . . . . 9
β’
β+ β (β β
(-β(,]0)) |
85 | 84 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β (β β (-β(,]0))) |
86 | 54, 85 | cxpcncf1 34136 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (π₯βπ-(1 /
2))) β (β+βcnββ)) |
87 | 78, 86 | mulcncf 25329 |
. . . . . 6
β’ (π β (π₯ β β+ β¦ ((1 /
π₯) Β· (π₯βπ-(1 /
2)))) β (β+βcnββ)) |
88 | | cncfmptc 24787 |
. . . . . . . . 9
β’ ((-(1 /
2) β β β§ β+ β β β§ β
β β) β (π₯
β β+ β¦ -(1 / 2)) β
(β+βcnββ)) |
89 | 54, 70, 72, 88 | syl3anc 1368 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ -(1 / 2))
β (β+βcnββ)) |
90 | 54, 52 | subcld 11575 |
. . . . . . . . 9
β’ (π β (-(1 / 2) β 1)
β β) |
91 | 90, 85 | cxpcncf1 34136 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ (π₯βπ(-(1 /
2) β 1))) β (β+βcnββ)) |
92 | 89, 91 | mulcncf 25329 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (-(1 / 2)
Β· (π₯βπ(-(1 / 2) β
1)))) β (β+βcnββ)) |
93 | | cncfss 24774 |
. . . . . . . . 9
β’ ((β
β β β§ β β β) β
(β+βcnββ) β
(β+βcnββ)) |
94 | 65, 71, 93 | mp2an 689 |
. . . . . . . 8
β’
(β+βcnββ) β
(β+βcnββ) |
95 | | relogcn 26527 |
. . . . . . . . 9
β’ (log
βΎ β+) β (β+βcnββ) |
96 | 48, 95 | eqeltrrdi 2836 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦
(logβπ₯)) β
(β+βcnββ)) |
97 | 94, 96 | sselid 3975 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦
(logβπ₯)) β
(β+βcnββ)) |
98 | 92, 97 | mulcncf 25329 |
. . . . . 6
β’ (π β (π₯ β β+ β¦ ((-(1 /
2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) β (β+βcnββ)) |
99 | 67, 69, 87, 98 | cncfmpt2f 24790 |
. . . . 5
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) |
100 | | rpre 12988 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β
β) |
101 | 100, 17 | rereccld 12045 |
. . . . . . . . 9
β’ (π₯ β β+
β (1 / π₯) β
β) |
102 | | rpge0 12993 |
. . . . . . . . . 10
β’ (π₯ β β+
β 0 β€ π₯) |
103 | | halfre 12430 |
. . . . . . . . . . . 12
β’ (1 / 2)
β β |
104 | 103 | renegcli 11525 |
. . . . . . . . . . 11
β’ -(1 / 2)
β β |
105 | 104 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β β+
β -(1 / 2) β β) |
106 | 100, 102,
105 | recxpcld 26612 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯βπ-(1 / 2)) β
β) |
107 | 101, 106 | remulcld 11248 |
. . . . . . . 8
β’ (π₯ β β+
β ((1 / π₯) Β·
(π₯βπ-(1 / 2))) β
β) |
108 | | 1re 11218 |
. . . . . . . . . . . . 13
β’ 1 β
β |
109 | 104, 108 | resubcli 11526 |
. . . . . . . . . . . 12
β’ (-(1 / 2)
β 1) β β |
110 | 109 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (-(1 / 2) β 1) β β) |
111 | 100, 102,
110 | recxpcld 26612 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯βπ(-(1 / 2) β
1)) β β) |
112 | 105, 111 | remulcld 11248 |
. . . . . . . . 9
β’ (π₯ β β+
β (-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) β β) |
113 | | relogcl 26464 |
. . . . . . . . 9
β’ (π₯ β β+
β (logβπ₯) β
β) |
114 | 112, 113 | remulcld 11248 |
. . . . . . . 8
β’ (π₯ β β+
β ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)) β β) |
115 | 107, 114 | readdcld 11247 |
. . . . . . 7
β’ (π₯ β β+
β (((1 / π₯) Β·
(π₯βπ-(1 / 2))) + ((-(1
/ 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) β β) |
116 | 115 | adantl 481 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) β β) |
117 | 116 | fmpttd 7110 |
. . . . 5
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))):β+βΆβ) |
118 | | cncfcdm 24773 |
. . . . . 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 477 |
. . . . 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 835 |
. . . 4
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) β (β+βcnββ)) |
121 | 64, 120 | eqeltrd 2827 |
. . 3
β’ (π β (β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯)))) β
(β+βcnββ)) |
122 | | logdivsqrle.2 |
. . 3
β’ (π β π΄ β€ π΅) |
123 | 64 | fveq1d 6887 |
. . . . 5
β’ (π β ((β D (π₯ β β+
β¦ ((logβπ₯) /
(ββπ₯))))βπ¦) = ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦)) |
124 | 123 | adantr 480 |
. . . 4
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((β D (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))))βπ¦) = ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦)) |
125 | 57 | negcld 11562 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β -1 β
β) |
126 | | cxpadd 26568 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π₯ β 0) β§ -(1 / 2) β
β β§ -1 β β) β (π₯βπ(-(1 / 2) + -1)) =
((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
127 | 16, 18, 55, 125, 126 | syl211anc 1373 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (π₯βπ(-(1 /
2) + -1)) = ((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
128 | 59 | mullidd 11236 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (1
Β· (π₯βπ(-(1 / 2) β
1))) = (π₯βπ(-(1 / 2) β
1))) |
129 | 55, 57 | negsubd 11581 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (-(1 / 2)
+ -1) = (-(1 / 2) β 1)) |
130 | 129 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (π₯βπ(-(1 /
2) + -1)) = (π₯βπ(-(1 / 2) β
1))) |
131 | 128, 130 | eqtr4d 2769 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (1
Β· (π₯βπ(-(1 / 2) β
1))) = (π₯βπ(-(1 / 2) +
-1))) |
132 | 43, 38 | sselid 3975 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β) |
133 | 132, 56 | mulcomd 11239 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β ((1 /
π₯) Β· (π₯βπ-(1 /
2))) = ((π₯βπ-(1 / 2)) Β·
(1 / π₯))) |
134 | | cxpneg 26570 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π₯ β 0 β§ 1 β β)
β (π₯βπ-1) = (1 / (π₯βπ1))) |
135 | 16, 18, 57, 134 | syl3anc 1368 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (π₯βπ-1) =
(1 / (π₯βπ1))) |
136 | 16 | cxp1d 26595 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β (π₯βπ1) =
π₯) |
137 | 136 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (1 /
(π₯βπ1)) = (1 / π₯)) |
138 | 135, 137 | eqtr2d 2767 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (1 /
π₯) = (π₯βπ-1)) |
139 | 138 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β ((π₯βπ-(1 /
2)) Β· (1 / π₯)) =
((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
140 | 133, 139 | eqtrd 2766 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β ((1 /
π₯) Β· (π₯βπ-(1 /
2))) = ((π₯βπ-(1 / 2)) Β·
(π₯βπ-1))) |
141 | 127, 131,
140 | 3eqtr4rd 2777 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β ((1 /
π₯) Β· (π₯βπ-(1 /
2))) = (1 Β· (π₯βπ(-(1 / 2) β
1)))) |
142 | 55, 59, 19 | mul32d 11428 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β ((-(1 /
2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)) = ((-(1 / 2) Β· (logβπ₯)) Β· (π₯βπ(-(1 / 2) β
1)))) |
143 | 141, 142 | oveq12d 7423 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) = ((1 Β· (π₯βπ(-(1 / 2) β
1))) + ((-(1 / 2) Β· (logβπ₯)) Β· (π₯βπ(-(1 / 2) β
1))))) |
144 | 55, 19 | mulcld 11238 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (-(1 / 2)
Β· (logβπ₯))
β β) |
145 | 57, 144, 59 | adddird 11243 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))) = ((1 Β· (π₯βπ(-(1 / 2) β
1))) + ((-(1 / 2) Β· (logβπ₯)) Β· (π₯βπ(-(1 / 2) β
1))))) |
146 | 143, 145 | eqtr4d 2769 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))) = ((1 + (-(1 / 2) Β·
(logβπ₯))) Β·
(π₯βπ(-(1 / 2) β
1)))) |
147 | 146 | mpteq2dva 5241 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯)))) = (π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))) |
148 | 147 | fveq1d 6887 |
. . . . . 6
β’ (π β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦) = ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦)) |
149 | 148 | adantr 480 |
. . . . 5
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦) = ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦)) |
150 | | eqidd 2727 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1)))) = (π₯ β
β+ β¦ ((1 + (-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))) |
151 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β π₯ = π¦) |
152 | 151 | fveq2d 6889 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (logβπ₯) = (logβπ¦)) |
153 | 152 | oveq2d 7421 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (-(1 / 2) Β· (logβπ₯)) = (-(1 / 2) Β·
(logβπ¦))) |
154 | 153 | oveq2d 7421 |
. . . . . . . 8
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (1 + (-(1 / 2) Β·
(logβπ₯))) = (1 + (-(1
/ 2) Β· (logβπ¦)))) |
155 | 151 | oveq1d 7420 |
. . . . . . . 8
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β (π₯βπ(-(1 / 2) β
1)) = (π¦βπ(-(1 / 2) β
1))) |
156 | 154, 155 | oveq12d 7423 |
. . . . . . 7
β’ (((π β§ π¦ β (π΄(,)π΅)) β§ π₯ = π¦) β ((1 + (-(1 / 2) Β·
(logβπ₯))) Β·
(π₯βπ(-(1 / 2) β
1))) = ((1 + (-(1 / 2) Β· (logβπ¦))) Β· (π¦βπ(-(1 / 2) β
1)))) |
157 | | ioossicc 13416 |
. . . . . . . . . 10
β’ (π΄(,)π΅) β (π΄[,]π΅) |
158 | 157 | a1i 11 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
159 | 2, 3, 4 | fct2relem 34138 |
. . . . . . . . 9
β’ (π β (π΄[,]π΅) β
β+) |
160 | 158, 159 | sstrd 3987 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β
β+) |
161 | 160 | sselda 3977 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β+) |
162 | | ovexd 7440 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) Β·
(π¦βπ(-(1 / 2) β
1))) β V) |
163 | 150, 156,
161, 162 | fvmptd 6999 |
. . . . . 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 26512 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β (logβπ¦) β β) |
167 | 165, 166 | remulcld 11248 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (-(1 / 2) Β·
(logβπ¦)) β
β) |
168 | 164, 167 | readdcld 11247 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 + (-(1 / 2) Β·
(logβπ¦))) β
β) |
169 | | 0red 11221 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β β) |
170 | | rpcxpcl 26565 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ (-(1 / 2) β 1) β β) β (π¦βπ(-(1 / 2) β
1)) β β+) |
171 | 161, 109,
170 | sylancl 585 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦βπ(-(1 / 2) β
1)) β β+) |
172 | 171 | rpred 13022 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦βπ(-(1 / 2) β
1)) β β) |
173 | 171 | rpge0d 13026 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β€ (π¦βπ(-(1 / 2) β
1))) |
174 | | 2cn 12291 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
175 | 174 | mullidi 11223 |
. . . . . . . . . . . . 13
β’ (1
Β· 2) = 2 |
176 | | 2re 12290 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β β) |
178 | 177 | reefcld 16038 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β
β) |
179 | 3 | rpred 13022 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β β) |
180 | 179 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β β) |
181 | 161 | rpred 13022 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β) |
182 | | logdivsqrle.1 |
. . . . . . . . . . . . . . . . 17
β’ (π β (expβ2) β€ π΄) |
183 | 182 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β€ π΄) |
184 | | eliooord 13389 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (π΄(,)π΅) β (π΄ < π¦ β§ π¦ < π΅)) |
185 | 184 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (π΄(,)π΅) β π΄ < π¦) |
186 | 185 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ < π¦) |
187 | 180, 181,
186 | ltled 11366 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β€ π¦) |
188 | 178, 180,
181, 183, 187 | letrd 11375 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β€ π¦) |
189 | | reeflog 26469 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β+
β (expβ(logβπ¦)) = π¦) |
190 | 161, 189 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ(logβπ¦)) = π¦) |
191 | 188, 190 | breqtrrd 5169 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (π΄(,)π΅)) β (expβ2) β€
(expβ(logβπ¦))) |
192 | | efle 16068 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ (logβπ¦) β β) β (2 β€
(logβπ¦) β
(expβ2) β€ (expβ(logβπ¦)))) |
193 | 176, 166,
192 | sylancr 586 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (π΄(,)π΅)) β (2 β€ (logβπ¦) β (expβ2) β€
(expβ(logβπ¦)))) |
194 | 191, 193 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β€ (logβπ¦)) |
195 | 175, 194 | eqbrtrid 5176 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 Β· 2) β€
(logβπ¦)) |
196 | | 2rp 12985 |
. . . . . . . . . . . . . 14
β’ 2 β
β+ |
197 | 196 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β
β+) |
198 | 164, 166,
197 | lemuldivd 13071 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 Β· 2) β€
(logβπ¦) β 1 β€
((logβπ¦) /
2))) |
199 | 195, 198 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β€ ((logβπ¦) / 2)) |
200 | 65, 166 | sselid 3975 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (logβπ¦) β β) |
201 | 22 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β β) |
202 | 24 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β 2 β 0) |
203 | 200, 201,
202 | divrec2d 11998 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((logβπ¦) / 2) = ((1 / 2) Β· (logβπ¦))) |
204 | 199, 203 | breqtrd 5167 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β€ ((1 / 2) Β·
(logβπ¦))) |
205 | 53 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π΄(,)π΅)) β (1 / 2) β
β) |
206 | 205, 200 | mulneg1d 11671 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (-(1 / 2) Β·
(logβπ¦)) = -((1 / 2)
Β· (logβπ¦))) |
207 | 206 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 β (-(1 / 2) Β·
(logβπ¦))) = (0
β -((1 / 2) Β· (logβπ¦)))) |
208 | 65, 169 | sselid 3975 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β β) |
209 | 205, 200 | mulcld 11238 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 / 2) Β· (logβπ¦)) β
β) |
210 | 208, 209 | subnegd 11582 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 β -((1 / 2) Β·
(logβπ¦))) = (0 + ((1
/ 2) Β· (logβπ¦)))) |
211 | 209 | addlidd 11419 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 + ((1 / 2) Β·
(logβπ¦))) = ((1 / 2)
Β· (logβπ¦))) |
212 | 207, 210,
211 | 3eqtrd 2770 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 β (-(1 / 2) Β·
(logβπ¦))) = ((1 / 2)
Β· (logβπ¦))) |
213 | 204, 212 | breqtrrd 5169 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β 1 β€ (0 β (-(1 / 2)
Β· (logβπ¦)))) |
214 | | leaddsub 11694 |
. . . . . . . . . 10
β’ ((1
β β β§ (-(1 / 2) Β· (logβπ¦)) β β β§ 0 β β)
β ((1 + (-(1 / 2) Β· (logβπ¦))) β€ 0 β 1 β€ (0 β (-(1 / 2)
Β· (logβπ¦))))) |
215 | 164, 167,
169, 214 | syl3anc 1368 |
. . . . . . . . 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 12157 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) Β·
(π¦βπ(-(1 / 2) β
1))) β€ (0 Β· (π¦βπ(-(1 / 2) β
1)))) |
218 | 43, 171 | sselid 3975 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦βπ(-(1 / 2) β
1)) β β) |
219 | 218 | mul02d 11416 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β (0 Β· (π¦βπ(-(1 / 2) β
1))) = 0) |
220 | 217, 219 | breqtrd 5167 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((1 + (-(1 / 2) Β·
(logβπ¦))) Β·
(π¦βπ(-(1 / 2) β
1))) β€ 0) |
221 | 163, 220 | eqbrtrd 5163 |
. . . . 5
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ ((1 +
(-(1 / 2) Β· (logβπ₯))) Β· (π₯βπ(-(1 / 2) β
1))))βπ¦) β€
0) |
222 | 149, 221 | eqbrtrd 5163 |
. . . 4
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π₯ β β+ β¦ (((1 /
π₯) Β· (π₯βπ-(1 /
2))) + ((-(1 / 2) Β· (π₯βπ(-(1 / 2) β
1))) Β· (logβπ₯))))βπ¦) β€ 0) |
223 | 124, 222 | eqbrtrd 5163 |
. . 3
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((β D (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))))βπ¦) β€ 0) |
224 | 2, 3, 4, 14, 121, 122, 223 | fdvnegge 34143 |
. 2
β’ (π β ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΅) β€ ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΄)) |
225 | | eqidd 2727 |
. . 3
β’ (π β (π₯ β β+ β¦
((logβπ₯) /
(ββπ₯))) =
(π₯ β
β+ β¦ ((logβπ₯) / (ββπ₯)))) |
226 | | simpr 484 |
. . . . 5
β’ ((π β§ π₯ = π΅) β π₯ = π΅) |
227 | 226 | fveq2d 6889 |
. . . 4
β’ ((π β§ π₯ = π΅) β (logβπ₯) = (logβπ΅)) |
228 | 226 | fveq2d 6889 |
. . . 4
β’ ((π β§ π₯ = π΅) β (ββπ₯) = (ββπ΅)) |
229 | 227, 228 | oveq12d 7423 |
. . 3
β’ ((π β§ π₯ = π΅) β ((logβπ₯) / (ββπ₯)) = ((logβπ΅) / (ββπ΅))) |
230 | | ovex 7438 |
. . . 4
β’
((logβπ΅) /
(ββπ΅)) β
V |
231 | 230 | a1i 11 |
. . 3
β’ (π β ((logβπ΅) / (ββπ΅)) β V) |
232 | 225, 229,
4, 231 | fvmptd 6999 |
. 2
β’ (π β ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΅) = ((logβπ΅) / (ββπ΅))) |
233 | | simpr 484 |
. . . . 5
β’ ((π β§ π₯ = π΄) β π₯ = π΄) |
234 | 233 | fveq2d 6889 |
. . . 4
β’ ((π β§ π₯ = π΄) β (logβπ₯) = (logβπ΄)) |
235 | 233 | fveq2d 6889 |
. . . 4
β’ ((π β§ π₯ = π΄) β (ββπ₯) = (ββπ΄)) |
236 | 234, 235 | oveq12d 7423 |
. . 3
β’ ((π β§ π₯ = π΄) β ((logβπ₯) / (ββπ₯)) = ((logβπ΄) / (ββπ΄))) |
237 | | ovex 7438 |
. . . 4
β’
((logβπ΄) /
(ββπ΄)) β
V |
238 | 237 | a1i 11 |
. . 3
β’ (π β ((logβπ΄) / (ββπ΄)) β V) |
239 | 225, 236,
3, 238 | fvmptd 6999 |
. 2
β’ (π β ((π₯ β β+ β¦
((logβπ₯) /
(ββπ₯)))βπ΄) = ((logβπ΄) / (ββπ΄))) |
240 | 224, 232,
239 | 3brtr3d 5172 |
1
β’ (π β ((logβπ΅) / (ββπ΅)) β€ ((logβπ΄) / (ββπ΄))) |