This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 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 mullidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 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 mullidi ⊢ ( 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 addlidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 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 ‘ 𝐴 ) / ( √ ‘ 𝐴 ) ) )