This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 tgioo4 ⊢ ( 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 ) ) ≤ ( √ ‘ 𝐴 ) )