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	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( 𝐴 + 1 ) ) ≤ ( √ ‘ 𝐴 ) )

Proof

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