Metamath Proof Explorer


Theorem logdivsqrle

Description: Conditions for ( ( log x ) / ( sqrt x ) ) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021)

Ref Expression
Hypotheses logdivsqrle.a ( 𝜑𝐴 ∈ ℝ+ )
logdivsqrle.b ( 𝜑𝐵 ∈ ℝ+ )
logdivsqrle.1 ( 𝜑 → ( exp ‘ 2 ) ≤ 𝐴 )
logdivsqrle.2 ( 𝜑𝐴𝐵 )
Assertion logdivsqrle ( 𝜑 → ( ( log ‘ 𝐵 ) / ( √ ‘ 𝐵 ) ) ≤ ( ( log ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 logdivsqrle.a ( 𝜑𝐴 ∈ ℝ+ )
2 logdivsqrle.b ( 𝜑𝐵 ∈ ℝ+ )
3 logdivsqrle.1 ( 𝜑 → ( exp ‘ 2 ) ≤ 𝐴 )
4 logdivsqrle.2 ( 𝜑𝐴𝐵 )
5 ioorp ( 0 (,) +∞ ) = ℝ+
6 5 eqcomi + = ( 0 (,) +∞ )
7 simpr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
8 7 relogcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
9 7 rpsqrtcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
10 9 rpred ( ( 𝜑𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ )
11 rpsqrtcl ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ )
12 rpne0 ( ( √ ‘ 𝑥 ) ∈ ℝ+ → ( √ ‘ 𝑥 ) ≠ 0 )
13 11 12 syl ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ≠ 0 )
14 13 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ≠ 0 )
15 8 10 14 redivcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ∈ ℝ )
16 15 fmpttd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) : ℝ+ ⟶ ℝ )
17 rpcn ( 𝑥 ∈ ℝ+𝑥 ∈ ℂ )
18 17 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
19 rpne0 ( 𝑥 ∈ ℝ+𝑥 ≠ 0 )
20 19 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
21 18 20 logcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
22 18 sqrtcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℂ )
23 21 22 14 divrecd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) )
24 2cnd ( 𝜑 → 2 ∈ ℂ )
25 24 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
26 2ne0 2 ≠ 0
27 26 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → 2 ≠ 0 )
28 25 27 reccld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / 2 ) ∈ ℂ )
29 18 20 28 cxpnegd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 - ( 1 / 2 ) ) = ( 1 / ( 𝑥𝑐 ( 1 / 2 ) ) ) )
30 cxpsqrt ( 𝑥 ∈ ℂ → ( 𝑥𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
31 18 30 syl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
32 31 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥𝑐 ( 1 / 2 ) ) ) = ( 1 / ( √ ‘ 𝑥 ) ) )
33 29 32 eqtrd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 - ( 1 / 2 ) ) = ( 1 / ( √ ‘ 𝑥 ) ) )
34 33 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) = ( ( log ‘ 𝑥 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) )
35 23 34 eqtr4d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) )
36 35 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) ) )
37 36 oveq2d ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) ) ) )
38 reelprrecn ℝ ∈ { ℝ , ℂ }
39 38 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
40 7 rpreccld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
41 logf1o log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
42 f1of ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
43 41 42 ax-mp log : ( ℂ ∖ { 0 } ) ⟶ ran log
44 43 a1i ( 𝜑 → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
45 17 ssriv + ⊆ ℂ
46 0nrp ¬ 0 ∈ ℝ+
47 ssdifsn ( ℝ+ ⊆ ( ℂ ∖ { 0 } ) ↔ ( ℝ+ ⊆ ℂ ∧ ¬ 0 ∈ ℝ+ ) )
48 45 46 47 mpbir2an + ⊆ ( ℂ ∖ { 0 } )
49 48 a1i ( 𝜑 → ℝ+ ⊆ ( ℂ ∖ { 0 } ) )
50 44 49 feqresmpt ( 𝜑 → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
51 50 oveq2d ( 𝜑 → ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) )
52 dvrelog ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
53 51 52 eqtr3di ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
54 1cnd ( 𝜑 → 1 ∈ ℂ )
55 54 halfcld ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
56 55 negcld ( 𝜑 → - ( 1 / 2 ) ∈ ℂ )
57 56 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → - ( 1 / 2 ) ∈ ℂ )
58 18 57 cxpcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 - ( 1 / 2 ) ) ∈ ℂ )
59 54 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
60 57 59 subcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( - ( 1 / 2 ) − 1 ) ∈ ℂ )
61 18 60 cxpcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ∈ ℂ )
62 57 61 mulcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ∈ ℂ )
63 dvcxp1 ( - ( 1 / 2 ) ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥𝑐 - ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) )
64 56 63 syl ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥𝑐 - ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) )
65 39 21 40 53 58 62 64 dvmptmul ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) )
66 37 65 eqtrd ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) )
67 ax-resscn ℝ ⊆ ℂ
68 67 a1i ( 𝜑 → ℝ ⊆ ℂ )
69 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
70 69 addcn + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
71 70 a1i ( 𝜑 → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
72 45 a1i ( 𝜑 → ℝ+ ⊆ ℂ )
73 ssid ℂ ⊆ ℂ
74 73 a1i ( 𝜑 → ℂ ⊆ ℂ )
75 cncfmptc ( ( 1 ∈ ℂ ∧ ℝ+ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ ( ℝ+cn→ ℂ ) )
76 54 72 74 75 syl3anc ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ ( ℝ+cn→ ℂ ) )
77 difss ( ℂ ∖ { 0 } ) ⊆ ℂ
78 cncfmptid ( ( ℝ+ ⊆ ( ℂ ∖ { 0 } ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝑥 ∈ ℝ+𝑥 ) ∈ ( ℝ+cn→ ( ℂ ∖ { 0 } ) ) )
79 49 77 78 sylancl ( 𝜑 → ( 𝑥 ∈ ℝ+𝑥 ) ∈ ( ℝ+cn→ ( ℂ ∖ { 0 } ) ) )
80 76 79 divcncf ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ ( ℝ+cn→ ℂ ) )
81 ax-1 ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) )
82 17 81 jca ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
83 eqid ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
84 83 ellogdm ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
85 82 84 sylibr ( 𝑥 ∈ ℝ+𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
86 85 ssriv + ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
87 86 a1i ( 𝜑 → ℝ+ ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) )
88 56 87 cxpcncf1 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝑥𝑐 - ( 1 / 2 ) ) ) ∈ ( ℝ+cn→ ℂ ) )
89 80 88 mulcncf ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) ) ∈ ( ℝ+cn→ ℂ ) )
90 cncfmptc ( ( - ( 1 / 2 ) ∈ ℂ ∧ ℝ+ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ - ( 1 / 2 ) ) ∈ ( ℝ+cn→ ℂ ) )
91 56 72 74 90 syl3anc ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ - ( 1 / 2 ) ) ∈ ( ℝ+cn→ ℂ ) )
92 56 54 subcld ( 𝜑 → ( - ( 1 / 2 ) − 1 ) ∈ ℂ )
93 92 87 cxpcncf1 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ∈ ( ℝ+cn→ ℂ ) )
94 91 93 mulcncf ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) ∈ ( ℝ+cn→ ℂ ) )
95 cncfss ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ+cn→ ℝ ) ⊆ ( ℝ+cn→ ℂ ) )
96 67 73 95 mp2an ( ℝ+cn→ ℝ ) ⊆ ( ℝ+cn→ ℂ )
97 relogcn ( log ↾ ℝ+ ) ∈ ( ℝ+cn→ ℝ )
98 50 97 eqeltrrdi ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ ( ℝ+cn→ ℝ ) )
99 96 98 sselid ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ ( ℝ+cn→ ℂ ) )
100 94 99 mulcncf ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ∈ ( ℝ+cn→ ℂ ) )
101 69 71 89 100 cncfmpt2f ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ∈ ( ℝ+cn→ ℂ ) )
102 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
103 102 19 rereccld ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ )
104 rpge0 ( 𝑥 ∈ ℝ+ → 0 ≤ 𝑥 )
105 halfre ( 1 / 2 ) ∈ ℝ
106 105 renegcli - ( 1 / 2 ) ∈ ℝ
107 106 a1i ( 𝑥 ∈ ℝ+ → - ( 1 / 2 ) ∈ ℝ )
108 102 104 107 recxpcld ( 𝑥 ∈ ℝ+ → ( 𝑥𝑐 - ( 1 / 2 ) ) ∈ ℝ )
109 103 108 remulcld ( 𝑥 ∈ ℝ+ → ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) ∈ ℝ )
110 1re 1 ∈ ℝ
111 106 110 resubcli ( - ( 1 / 2 ) − 1 ) ∈ ℝ
112 111 a1i ( 𝑥 ∈ ℝ+ → ( - ( 1 / 2 ) − 1 ) ∈ ℝ )
113 102 104 112 recxpcld ( 𝑥 ∈ ℝ+ → ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ∈ ℝ )
114 107 113 remulcld ( 𝑥 ∈ ℝ+ → ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ∈ ℝ )
115 relogcl ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
116 114 115 remulcld ( 𝑥 ∈ ℝ+ → ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
117 109 116 readdcld ( 𝑥 ∈ ℝ+ → ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
118 117 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
119 118 fmpttd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) : ℝ+ ⟶ ℝ )
120 cncffvrn ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 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 ‘ 𝑥 ) ) ) ) : ℝ+ ⟶ ℝ ) )
121 120 biimpar ( ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 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→ ℝ ) )
122 68 101 119 121 syl21anc ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ∈ ( ℝ+cn→ ℝ ) )
123 66 122 eqeltrd ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ) ∈ ( ℝ+cn→ ℝ ) )
124 66 fveq1d ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) )
125 124 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) )
126 59 negcld ( ( 𝜑𝑥 ∈ ℝ+ ) → - 1 ∈ ℂ )
127 cxpadd ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ - ( 1 / 2 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( 𝑥𝑐 ( - ( 1 / 2 ) + - 1 ) ) = ( ( 𝑥𝑐 - ( 1 / 2 ) ) · ( 𝑥𝑐 - 1 ) ) )
128 18 20 57 126 127 syl211anc ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 ( - ( 1 / 2 ) + - 1 ) ) = ( ( 𝑥𝑐 - ( 1 / 2 ) ) · ( 𝑥𝑐 - 1 ) ) )
129 61 mulid2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) = ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) )
130 57 59 negsubd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( - ( 1 / 2 ) + - 1 ) = ( - ( 1 / 2 ) − 1 ) )
131 130 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 ( - ( 1 / 2 ) + - 1 ) ) = ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) )
132 129 131 eqtr4d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) = ( 𝑥𝑐 ( - ( 1 / 2 ) + - 1 ) ) )
133 45 40 sselid ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℂ )
134 133 58 mulcomd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) = ( ( 𝑥𝑐 - ( 1 / 2 ) ) · ( 1 / 𝑥 ) ) )
135 cxpneg ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ∧ 1 ∈ ℂ ) → ( 𝑥𝑐 - 1 ) = ( 1 / ( 𝑥𝑐 1 ) ) )
136 18 20 59 135 syl3anc ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 - 1 ) = ( 1 / ( 𝑥𝑐 1 ) ) )
137 18 cxp1d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥𝑐 1 ) = 𝑥 )
138 137 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥𝑐 1 ) ) = ( 1 / 𝑥 ) )
139 136 138 eqtr2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) = ( 𝑥𝑐 - 1 ) )
140 139 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 𝑥𝑐 - ( 1 / 2 ) ) · ( 1 / 𝑥 ) ) = ( ( 𝑥𝑐 - ( 1 / 2 ) ) · ( 𝑥𝑐 - 1 ) ) )
141 134 140 eqtrd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) = ( ( 𝑥𝑐 - ( 1 / 2 ) ) · ( 𝑥𝑐 - 1 ) ) )
142 128 132 141 3eqtr4rd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) = ( 1 · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) )
143 57 61 21 mul32d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) = ( ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) )
144 142 143 oveq12d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( ( 1 · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) + ( ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) )
145 57 21 mulcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
146 59 145 61 adddird ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) = ( ( 1 · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) + ( ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) )
147 144 146 eqtr4d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) )
148 147 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) )
149 148 fveq1d ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) ‘ 𝑦 ) )
150 149 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) ‘ 𝑦 ) )
151 eqidd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) )
152 simpr ( ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
153 152 fveq2d ( ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ( log ‘ 𝑥 ) = ( log ‘ 𝑦 ) )
154 153 oveq2d ( ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) = ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) )
155 154 oveq2d ( ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) = ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) )
156 152 oveq1d ( ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) = ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) )
157 155 156 oveq12d ( ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) = ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) )
158 ioossicc ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
159 158 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
160 6 1 2 fct2relem ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ+ )
161 159 160 sstrd ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ+ )
162 161 sselda ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ+ )
163 ovexd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ∈ V )
164 151 157 162 163 fvmptd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) ‘ 𝑦 ) = ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) )
165 110 a1i ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
166 106 a1i ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( 1 / 2 ) ∈ ℝ )
167 162 relogcld ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
168 166 167 remulcld ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ∈ ℝ )
169 165 168 readdcld ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
170 0red ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
171 rpcxpcl ( ( 𝑦 ∈ ℝ+ ∧ ( - ( 1 / 2 ) − 1 ) ∈ ℝ ) → ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ∈ ℝ+ )
172 162 111 171 sylancl ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ∈ ℝ+ )
173 172 rpred ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ∈ ℝ )
174 172 rpge0d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) )
175 2cn 2 ∈ ℂ
176 175 mulid2i ( 1 · 2 ) = 2
177 2re 2 ∈ ℝ
178 177 a1i ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℝ )
179 178 reefcld ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( exp ‘ 2 ) ∈ ℝ )
180 1 rpred ( 𝜑𝐴 ∈ ℝ )
181 180 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
182 162 rpred ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ )
183 3 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( exp ‘ 2 ) ≤ 𝐴 )
184 eliooord ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑦𝑦 < 𝐵 ) )
185 184 simpld ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 < 𝑦 )
186 185 adantl ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑦 )
187 181 182 186 ltled ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴𝑦 )
188 179 181 182 183 187 letrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( exp ‘ 2 ) ≤ 𝑦 )
189 reeflog ( 𝑦 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝑦 ) ) = 𝑦 )
190 162 189 syl ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( exp ‘ ( log ‘ 𝑦 ) ) = 𝑦 )
191 188 190 breqtrrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( exp ‘ 2 ) ≤ ( exp ‘ ( log ‘ 𝑦 ) ) )
192 efle ( ( 2 ∈ ℝ ∧ ( log ‘ 𝑦 ) ∈ ℝ ) → ( 2 ≤ ( log ‘ 𝑦 ) ↔ ( exp ‘ 2 ) ≤ ( exp ‘ ( log ‘ 𝑦 ) ) ) )
193 177 167 192 sylancr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 ≤ ( log ‘ 𝑦 ) ↔ ( exp ‘ 2 ) ≤ ( exp ‘ ( log ‘ 𝑦 ) ) ) )
194 191 193 mpbird ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≤ ( log ‘ 𝑦 ) )
195 176 194 eqbrtrid ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 · 2 ) ≤ ( log ‘ 𝑦 ) )
196 2rp 2 ∈ ℝ+
197 196 a1i ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℝ+ )
198 165 167 197 lemuldivd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 · 2 ) ≤ ( log ‘ 𝑦 ) ↔ 1 ≤ ( ( log ‘ 𝑦 ) / 2 ) ) )
199 195 198 mpbid ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ≤ ( ( log ‘ 𝑦 ) / 2 ) )
200 67 167 sselid ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
201 24 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
202 26 a1i ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
203 200 201 202 divrec2d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 𝑦 ) / 2 ) = ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) )
204 199 203 breqtrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ≤ ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) )
205 55 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 2 ) ∈ ℂ )
206 205 200 mulneg1d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) = - ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) )
207 206 oveq2d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 − ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) = ( 0 − - ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) )
208 67 170 sselid ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℂ )
209 205 200 mulcld ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ∈ ℂ )
210 208 209 subnegd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 − - ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) = ( 0 + ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) )
211 209 addid2d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 + ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) = ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) )
212 207 210 211 3eqtrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 − ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) = ( ( 1 / 2 ) · ( log ‘ 𝑦 ) ) )
213 204 212 breqtrrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ≤ ( 0 − ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) )
214 leaddsub ( ( 1 ∈ ℝ ∧ ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) ≤ 0 ↔ 1 ≤ ( 0 − ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) ) )
215 165 168 170 214 syl3anc ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) ≤ 0 ↔ 1 ≤ ( 0 − ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) ) )
216 213 215 mpbird ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) ≤ 0 )
217 169 170 173 174 216 lemul1ad ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ≤ ( 0 · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) )
218 45 172 sselid ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ∈ ℂ )
219 218 mul02d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) = 0 )
220 217 219 breqtrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑦 ) ) ) · ( 𝑦𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ≤ 0 )
221 164 220 eqbrtrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( - ( 1 / 2 ) · ( log ‘ 𝑥 ) ) ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) ) ‘ 𝑦 ) ≤ 0 )
222 150 221 eqbrtrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( 1 / 𝑥 ) · ( 𝑥𝑐 - ( 1 / 2 ) ) ) + ( ( - ( 1 / 2 ) · ( 𝑥𝑐 ( - ( 1 / 2 ) − 1 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) ≤ 0 )
223 125 222 eqbrtrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) ≤ 0 )
224 6 1 2 16 123 4 223 fdvnegge ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ‘ 𝐵 ) ≤ ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ‘ 𝐴 ) )
225 eqidd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) )
226 simpr ( ( 𝜑𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
227 226 fveq2d ( ( 𝜑𝑥 = 𝐵 ) → ( log ‘ 𝑥 ) = ( log ‘ 𝐵 ) )
228 226 fveq2d ( ( 𝜑𝑥 = 𝐵 ) → ( √ ‘ 𝑥 ) = ( √ ‘ 𝐵 ) )
229 227 228 oveq12d ( ( 𝜑𝑥 = 𝐵 ) → ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) = ( ( log ‘ 𝐵 ) / ( √ ‘ 𝐵 ) ) )
230 ovex ( ( log ‘ 𝐵 ) / ( √ ‘ 𝐵 ) ) ∈ V
231 230 a1i ( 𝜑 → ( ( log ‘ 𝐵 ) / ( √ ‘ 𝐵 ) ) ∈ V )
232 225 229 2 231 fvmptd ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ( log ‘ 𝐵 ) / ( √ ‘ 𝐵 ) ) )
233 simpr ( ( 𝜑𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
234 233 fveq2d ( ( 𝜑𝑥 = 𝐴 ) → ( log ‘ 𝑥 ) = ( log ‘ 𝐴 ) )
235 233 fveq2d ( ( 𝜑𝑥 = 𝐴 ) → ( √ ‘ 𝑥 ) = ( √ ‘ 𝐴 ) )
236 234 235 oveq12d ( ( 𝜑𝑥 = 𝐴 ) → ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) = ( ( log ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) )
237 ovex ( ( log ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) ∈ V
238 237 a1i ( 𝜑 → ( ( log ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) ∈ V )
239 225 236 1 238 fvmptd ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) ) ‘ 𝐴 ) = ( ( log ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) )
240 224 232 239 3brtr3d ( 𝜑 → ( ( log ‘ 𝐵 ) / ( √ ‘ 𝐵 ) ) ≤ ( ( log ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) )