logdivsqrle

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

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

Proof

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

Metamath Proof Explorer

Theorem logdivsqrle

Proof