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 
|- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( A + 1 ) ) <_ ( sqrt ` A ) )

Proof

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