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 cncffvrn ( ( ℝ+ ⊆ ℂ ∧ ( 𝑥 ∈ ( 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 mulid1d ( ( ( 𝐴 ∈ ℝ ∧ 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 ) ) ≤ ( √ ‘ 𝐴 ) )