Theorem logdivsqrle

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

	Ref	Expression
Hypotheses	logdivsqrle.a	$$⊢\phi \to A\in {ℝ}^{+}$$
	logdivsqrle.b	$$⊢\phi \to B\in {ℝ}^{+}$$
	logdivsqrle.1	$$⊢\phi \to {\mathrm{e}}^2\le A$$
	logdivsqrle.2	$$⊢\phi \to A\le B$$
Assertion	logdivsqrle	$$⊢\phi \to \frac{\log B}{\sqrt{B}}\le \frac{\log A}{\sqrt{A}}$$

Proof

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