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		cncffvrn	|- ( ( 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	12	tgioo2	|- ( 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	mulid1d	|- ( ( ( 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 ) )