loglesqrt

Description: An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016) (Proof shortened by AV, 2-Aug-2021)

		Ref	Expression
	Assertion	loglesqrt	$⊢ (A \in ℝ \land 0 \leq A) \to \log (A + 1) \leq \sqrt{A}$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2	1	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \in ℝ$
3		simpl	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℝ$
4		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (x \in [0, A] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq A))$
5	1 3 4	sylancr	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq A))$
6	5	biimpa	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in [0, A]) \to (x \in ℝ \land 0 \leq x \land x \leq A)$
7	6	simp1d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in [0, A]) \to x \in ℝ$
8	6	simp2d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in [0, A]) \to 0 \leq x$
9	7 8	ge0p1rpd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in [0, A]) \to x + 1 \in ℝ^{+}$
10	9	fvresd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in [0, A]) \to ({log ↾}_{ℝ^{+}}) (x + 1) = \log (x + 1)$
11	10	mpteq2dva	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ ({log ↾}_{ℝ^{+}}) (x + 1)) = (x \in [0, A] ⟼ \log (x + 1))$
12		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
13	12	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
14	7	ex	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] \to x \in ℝ)$
15	14	ssrdv	$⊢ (A \in ℝ \land 0 \leq A) \to [0, A] \subseteq ℝ$
16		ax-resscn	$⊢ ℝ \subseteq ℂ$
17	15 16	sstrdi	$⊢ (A \in ℝ \land 0 \leq A) \to [0, A] \subseteq ℂ$
18		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [0, A] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A] \in TopOn ([0, A])$
19	13 17 18	sylancr	$⊢ (A \in ℝ \land 0 \leq A) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A] \in TopOn ([0, A])$
20	9	fmpttd	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ x + 1) : [0, A] ⟶ ℝ^{+}$
21		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
22	21 16	sstri	$⊢ ℝ^{+} \subseteq ℂ$
23	12	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
24	23	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
25		ssid	$⊢ ℂ \subseteq ℂ$
26		cncfmptid	$⊢ ([0, A] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [0, A] ⟼ x) : [0, A] \underset{cn}{⟶} ℂ$
27	17 25 26	sylancl	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ x) : [0, A] \underset{cn}{⟶} ℂ$
28		1cnd	$⊢ (A \in ℝ \land 0 \leq A) \to 1 \in ℂ$
29	25	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to ℂ \subseteq ℂ$
30		cncfmptc	$⊢ (1 \in ℂ \land [0, A] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [0, A] ⟼ 1) : [0, A] \underset{cn}{⟶} ℂ$
31	28 17 29 30	syl3anc	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ 1) : [0, A] \underset{cn}{⟶} ℂ$
32	12 24 27 31	cncfmpt2f	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ x + 1) : [0, A] \underset{cn}{⟶} ℂ$
33		cncffvrn	$⊢ (ℝ^{+} \subseteq ℂ \land (x \in [0, A] ⟼ x + 1) : [0, A] \underset{cn}{⟶} ℂ) \to ((x \in [0, A] ⟼ x + 1) : [0, A] \underset{cn}{⟶} ℝ^{+} \leftrightarrow (x \in [0, A] ⟼ x + 1) : [0, A] ⟶ ℝ^{+})$
34	22 32 33	sylancr	$⊢ (A \in ℝ \land 0 \leq A) \to ((x \in [0, A] ⟼ x + 1) : [0, A] \underset{cn}{⟶} ℝ^{+} \leftrightarrow (x \in [0, A] ⟼ x + 1) : [0, A] ⟶ ℝ^{+})$
35	20 34	mpbird	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ x + 1) : [0, A] \underset{cn}{⟶} ℝ^{+}$
36		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A] = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]$
37		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+} = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+}$
38	12 36 37	cncfcn	$⊢ ([0, A] \subseteq ℂ \land ℝ^{+} \subseteq ℂ) \to [0, A] \underset{cn}{⟶} ℝ^{+} = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+})$
39	17 22 38	sylancl	$⊢ (A \in ℝ \land 0 \leq A) \to [0, A] \underset{cn}{⟶} ℝ^{+} = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+})$
40	35 39	eleqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ x + 1) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+}))$
41		relogcn	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{cn}{⟶} ℝ$
42		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
43	12 37 42	cncfcn	$⊢ (ℝ^{+} \subseteq ℂ \land ℝ \subseteq ℂ) \to ℝ^{+} \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+}) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
44	22 16 43	mp2an	$⊢ ℝ^{+} \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+}) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
45	41 44	eleqtri	$⊢ {log ↾}_{ℝ^{+}} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+}) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
46	45	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to {log ↾}_{ℝ^{+}} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ^{+}) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
47	19 40 46	cnmpt11f	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ ({log ↾}_{ℝ^{+}}) (x + 1)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
48	12 36 42	cncfcn	$⊢ ([0, A] \subseteq ℂ \land ℝ \subseteq ℂ) \to [0, A] \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
49	17 16 48	sylancl	$⊢ (A \in ℝ \land 0 \leq A) \to [0, A] \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, A]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
50	47 49	eleqtrrd	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ ({log ↾}_{ℝ^{+}}) (x + 1)) : [0, A] \underset{cn}{⟶} ℝ$
51	11 50	eqeltrrd	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ \log (x + 1)) : [0, A] \underset{cn}{⟶} ℝ$
52		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
53	52	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to ℝ \in \{ℝ, ℂ\}$
54		simpr	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
55		1rp	$⊢ 1 \in ℝ^{+}$
56		rpaddcl	$⊢ (x \in ℝ^{+} \land 1 \in ℝ^{+}) \to x + 1 \in ℝ^{+}$
57	54 55 56	sylancl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to x + 1 \in ℝ^{+}$
58	57	relogcld	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \log (x + 1) \in ℝ$
59	58	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \log (x + 1) \in ℂ$
60	57	rpreccld	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \frac{1}{x + 1} \in ℝ^{+}$
61		1cnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 1 \in ℂ$
62		relogcl	$⊢ y \in ℝ^{+} \to \log y \in ℝ$
63	62	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ^{+}) \to \log y \in ℝ$
64	63	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ^{+}) \to \log y \in ℂ$
65		rpreccl	$⊢ y \in ℝ^{+} \to \frac{1}{y} \in ℝ^{+}$
66	65	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ^{+}) \to \frac{1}{y} \in ℝ^{+}$
67		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
68	67	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ) \to x + 1 \in ℝ$
69	68	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ) \to x + 1 \in ℂ$
70		1cnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ) \to 1 \in ℂ$
71	16	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to ℝ \subseteq ℂ$
72	71	sselda	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ) \to x \in ℂ$
73	53	dvmptid	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
74		0cnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ) \to 0 \in ℂ$
75	53 28	dvmptc	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ⟼ 1)}{d_{ℝ} x} = (x \in ℝ ⟼ 0)$
76	53 72 70 73 70 74 75	dvmptadd	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ⟼ x + 1)}{d_{ℝ} x} = (x \in ℝ ⟼ 1 + 0)$
77		1p0e1	$⊢ 1 + 0 = 1$
78	77	mpteq2i	$⊢ (x \in ℝ ⟼ 1 + 0) = (x \in ℝ ⟼ 1)$
79	76 78	eqtrdi	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ⟼ x + 1)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
80	21	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to ℝ^{+} \subseteq ℝ$
81	12	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
82		ioorp	$⊢ (0, +∞) = ℝ^{+}$
83		iooretop	$⊢ (0, +∞) \in topGen (ran (.))$
84	82 83	eqeltrri	$⊢ ℝ^{+} \in topGen (ran (.))$
85	84	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to ℝ^{+} \in topGen (ran (.))$
86	53 69 70 79 80 81 12 85	dvmptres	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ^{+}⟼ x + 1)}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ 1)$
87		relogf1o	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ$
88		f1of	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
89	87 88	mp1i	$⊢ (A \in ℝ \land 0 \leq A) \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
90	89	feqmptd	$⊢ (A \in ℝ \land 0 \leq A) \to {log ↾}_{ℝ^{+}} = (y \in ℝ^{+} ⟼ ({log ↾}_{ℝ^{+}}) (y))$
91		fvres	$⊢ y \in ℝ^{+} \to ({log ↾}_{ℝ^{+}}) (y) = \log y$
92	91	mpteq2ia	$⊢ (y \in ℝ^{+} ⟼ ({log ↾}_{ℝ^{+}}) (y)) = (y \in ℝ^{+} ⟼ \log y)$
93	90 92	eqtrdi	$⊢ (A \in ℝ \land 0 \leq A) \to {log ↾}_{ℝ^{+}} = (y \in ℝ^{+} ⟼ \log y)$
94	93	oveq2d	$⊢ (A \in ℝ \land 0 \leq A) \to ℝ D ({log ↾}_{ℝ^{+}}) = \frac{d (y \in ℝ^{+}⟼ \log y)}{d_{ℝ} y}$
95		dvrelog	$⊢ ℝ D ({log ↾}_{ℝ^{+}}) = (y \in ℝ^{+} ⟼ \frac{1}{y})$
96	94 95	eqtr3di	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (y \in ℝ^{+}⟼ \log y)}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{1}{y})$
97		fveq2	$⊢ y = x + 1 \to \log y = \log (x + 1)$
98		oveq2	$⊢ y = x + 1 \to \frac{1}{y} = \frac{1}{x + 1}$
99	53 53 57 61 64 66 86 96 97 98	dvmptco	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ^{+}⟼ \log (x + 1))}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ (\frac{1}{x + 1}) \cdot 1)$
100	60	rpcnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \frac{1}{x + 1} \in ℂ$
101	100	mulid1d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to (\frac{1}{x + 1}) \cdot 1 = \frac{1}{x + 1}$
102	101	mpteq2dva	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in ℝ^{+} ⟼ (\frac{1}{x + 1}) \cdot 1) = (x \in ℝ^{+} ⟼ \frac{1}{x + 1})$
103	99 102	eqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ^{+}⟼ \log (x + 1))}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{1}{x + 1})$
104		ioossicc	$⊢ (0, A) \subseteq [0, A]$
105	104	sseli	$⊢ x \in (0, A) \to x \in [0, A]$
106	105 7	sylan2	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in (0, A)) \to x \in ℝ$
107		eliooord	$⊢ x \in (0, A) \to (0 < x \land x < A)$
108	107	simpld	$⊢ x \in (0, A) \to 0 < x$
109	108	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in (0, A)) \to 0 < x$
110	106 109	elrpd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in (0, A)) \to x \in ℝ^{+}$
111	110	ex	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in (0, A) \to x \in ℝ^{+})$
112	111	ssrdv	$⊢ (A \in ℝ \land 0 \leq A) \to (0, A) \subseteq ℝ^{+}$
113		iooretop	$⊢ (0, A) \in topGen (ran (.))$
114	113	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to (0, A) \in topGen (ran (.))$
115	53 59 60 103 112 81 12 114	dvmptres	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in (0, A)⟼ \log (x + 1))}{d_{ℝ} x} = (x \in (0, A) ⟼ \frac{1}{x + 1})$
116		elrege0	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x)$
117	7 8 116	sylanbrc	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in [0, A]) \to x \in [0, +∞)$
118	117	ex	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] \to x \in [0, +∞))$
119	118	ssrdv	$⊢ (A \in ℝ \land 0 \leq A) \to [0, A] \subseteq [0, +∞)$
120	119	resabs1d	$⊢ (A \in ℝ \land 0 \leq A) \to {({\sqrt ↾}_{[0, +∞)}) ↾}_{[0, A]} = {\sqrt ↾}_{[0, A]}$
121		sqrtf	$⊢ \sqrt : ℂ ⟶ ℂ$
122	121	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt : ℂ ⟶ ℂ$
123	122 17	feqresmpt	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt ↾}_{[0, A]} = (x \in [0, A] ⟼ \sqrt{x})$
124	120 123	eqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to {({\sqrt ↾}_{[0, +∞)}) ↾}_{[0, A]} = (x \in [0, A] ⟼ \sqrt{x})$
125		resqrtcn	$⊢ ({\sqrt ↾}_{[0, +∞)}) : [0, +∞) \underset{cn}{⟶} ℝ$
126		rescncf	$⊢ [0, A] \subseteq [0, +∞) \to (({\sqrt ↾}_{[0, +∞)}) : [0, +∞) \underset{cn}{⟶} ℝ \to ({({\sqrt ↾}_{[0, +∞)}) ↾}_{[0, A]}) : [0, A] \underset{cn}{⟶} ℝ)$
127	119 125 126	mpisyl	$⊢ (A \in ℝ \land 0 \leq A) \to ({({\sqrt ↾}_{[0, +∞)}) ↾}_{[0, A]}) : [0, A] \underset{cn}{⟶} ℝ$
128	124 127	eqeltrrd	$⊢ (A \in ℝ \land 0 \leq A) \to (x \in [0, A] ⟼ \sqrt{x}) : [0, A] \underset{cn}{⟶} ℝ$
129		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
130	129	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to x \in ℂ$
131	130	sqrtcld	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \sqrt{x} \in ℂ$
132		2rp	$⊢ 2 \in ℝ^{+}$
133		rpsqrtcl	$⊢ x \in ℝ^{+} \to \sqrt{x} \in ℝ^{+}$
134	133	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ^{+}$
135		rpmulcl	$⊢ (2 \in ℝ^{+} \land \sqrt{x} \in ℝ^{+}) \to 2 \sqrt{x} \in ℝ^{+}$
136	132 134 135	sylancr	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 2 \sqrt{x} \in ℝ^{+}$
137	136	rpreccld	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \frac{1}{2 \sqrt{x}} \in ℝ^{+}$
138		dvsqrt	$⊢ \frac{d (x \in ℝ^{+}⟼ \sqrt{x})}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{1}{2 \sqrt{x}})$
139	138	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in ℝ^{+}⟼ \sqrt{x})}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{1}{2 \sqrt{x}})$
140	53 131 137 139 112 81 12 114	dvmptres	$⊢ (A \in ℝ \land 0 \leq A) \to \frac{d (x \in (0, A)⟼ \sqrt{x})}{d_{ℝ} x} = (x \in (0, A) ⟼ \frac{1}{2 \sqrt{x}})$
141	134	rpred	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ$
142		1re	$⊢ 1 \in ℝ$
143		resubcl	$⊢ (\sqrt{x} \in ℝ \land 1 \in ℝ) \to \sqrt{x} - 1 \in ℝ$
144	141 142 143	sylancl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \sqrt{x} - 1 \in ℝ$
145	144	sqge0d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 0 \leq {(\sqrt{x} - 1)}^{2}$
146	130	sqsqrtd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to {\sqrt{x}}^{2} = x$
147	146	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to {\sqrt{x}}^{2} - 2 \sqrt{x} = x - 2 \sqrt{x}$
148	147	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to {\sqrt{x}}^{2} - 2 \sqrt{x} + 1 = x - 2 \sqrt{x} + 1$
149		binom2sub1	$⊢ \sqrt{x} \in ℂ \to {(\sqrt{x} - 1)}^{2} = {\sqrt{x}}^{2} - 2 \sqrt{x} + 1$
150	131 149	syl	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to {(\sqrt{x} - 1)}^{2} = {\sqrt{x}}^{2} - 2 \sqrt{x} + 1$
151	136	rpcnd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 2 \sqrt{x} \in ℂ$
152	130 61 151	addsubd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to x + 1 - 2 \sqrt{x} = x - 2 \sqrt{x} + 1$
153	148 150 152	3eqtr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to {(\sqrt{x} - 1)}^{2} = x + 1 - 2 \sqrt{x}$
154	145 153	breqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 0 \leq x + 1 - 2 \sqrt{x}$
155	57	rpred	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to x + 1 \in ℝ$
156	136	rpred	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 2 \sqrt{x} \in ℝ$
157	155 156	subge0d	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to (0 \leq x + 1 - 2 \sqrt{x} \leftrightarrow 2 \sqrt{x} \leq x + 1)$
158	154 157	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to 2 \sqrt{x} \leq x + 1$
159	136 57	lerecd	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to (2 \sqrt{x} \leq x + 1 \leftrightarrow \frac{1}{x + 1} \leq \frac{1}{2 \sqrt{x}})$
160	158 159	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in ℝ^{+}) \to \frac{1}{x + 1} \leq \frac{1}{2 \sqrt{x}}$
161	110 160	syldan	$⊢ ((A \in ℝ \land 0 \leq A) \land x \in (0, A)) \to \frac{1}{x + 1} \leq \frac{1}{2 \sqrt{x}}$
162		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
163		0xr	$⊢ 0 \in ℝ^{*}$
164		lbicc2	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land 0 \leq A) \to 0 \in [0, A]$
165	163 164	mp3an1	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to 0 \in [0, A]$
166	162 165	sylan	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \in [0, A]$
167		ubicc2	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land 0 \leq A) \to A \in [0, A]$
168	163 167	mp3an1	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to A \in [0, A]$
169	162 168	sylan	$⊢ (A \in ℝ \land 0 \leq A) \to A \in [0, A]$
170		simpr	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq A$
171		fv0p1e1	$⊢ x = 0 \to \log (x + 1) = \log 1$
172		log1	$⊢ \log 1 = 0$
173	171 172	eqtrdi	$⊢ x = 0 \to \log (x + 1) = 0$
174		fveq2	$⊢ x = 0 \to \sqrt{x} = \sqrt{0}$
175		sqrt0	$⊢ \sqrt{0} = 0$
176	174 175	eqtrdi	$⊢ x = 0 \to \sqrt{x} = 0$
177		fvoveq1	$⊢ x = A \to \log (x + 1) = \log (A + 1)$
178		fveq2	$⊢ x = A \to \sqrt{x} = \sqrt{A}$
179	2 3 51 115 128 140 161 166 169 170 173 176 177 178	dvle	$⊢ (A \in ℝ \land 0 \leq A) \to \log (A + 1) - 0 \leq \sqrt{A} - 0$
180		ge0p1rp	$⊢ (A \in ℝ \land 0 \leq A) \to A + 1 \in ℝ^{+}$
181	180	relogcld	$⊢ (A \in ℝ \land 0 \leq A) \to \log (A + 1) \in ℝ$
182		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
183	181 182 2	lesub1d	$⊢ (A \in ℝ \land 0 \leq A) \to (\log (A + 1) \leq \sqrt{A} \leftrightarrow \log (A + 1) - 0 \leq \sqrt{A} - 0)$
184	179 183	mpbird	$⊢ (A \in ℝ \land 0 \leq A) \to \log (A + 1) \leq \sqrt{A}$

Metamath Proof Explorer

Theorem loglesqrt

Proof