Theorem 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	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \log \left(A+1\right)\le \sqrt{A}$$

Proof

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