ioodvbdlimc1lem2

Description: Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	ioodvbdlimc1lem2.a	\|- ( ph -> A e. RR )
	ioodvbdlimc1lem2.b	\|- ( ph -> B e. RR )
	ioodvbdlimc1lem2.altb	\|- ( ph -> A < B )
	ioodvbdlimc1lem2.f	\|- ( ph -> F : ( A (,) B ) --> RR )
	ioodvbdlimc1lem2.dmdv	\|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
	ioodvbdlimc1lem2.dvbd	\|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
	ioodvbdlimc1lem2.y	\|- Y = sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
	ioodvbdlimc1lem2.m	\|- M = ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 )
	ioodvbdlimc1lem2.s	\|- S = ( j e. ( ZZ>= ` M ) \|-> ( F ` ( A + ( 1 / j ) ) ) )
	ioodvbdlimc1lem2.r	\|- R = ( j e. ( ZZ>= ` M ) \|-> ( A + ( 1 / j ) ) )
	ioodvbdlimc1lem2.n	\|- N = if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
	ioodvbdlimc1lem2.ch	\|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
Assertion	ioodvbdlimc1lem2	\|- ( ph -> ( limsup ` S ) e. ( F limCC A ) )

Proof

Step	Hyp	Ref	Expression
1		ioodvbdlimc1lem2.a	\|- ( ph -> A e. RR )
2		ioodvbdlimc1lem2.b	\|- ( ph -> B e. RR )
3		ioodvbdlimc1lem2.altb	\|- ( ph -> A < B )
4		ioodvbdlimc1lem2.f	\|- ( ph -> F : ( A (,) B ) --> RR )
5		ioodvbdlimc1lem2.dmdv	\|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6		ioodvbdlimc1lem2.dvbd	\|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
7		ioodvbdlimc1lem2.y	\|- Y = sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
8		ioodvbdlimc1lem2.m	\|- M = ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 )
9		ioodvbdlimc1lem2.s	\|- S = ( j e. ( ZZ>= ` M ) \|-> ( F ` ( A + ( 1 / j ) ) ) )
10		ioodvbdlimc1lem2.r	\|- R = ( j e. ( ZZ>= ` M ) \|-> ( A + ( 1 / j ) ) )
11		ioodvbdlimc1lem2.n	\|- N = if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
12		ioodvbdlimc1lem2.ch	\|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
13		uzssz	\|- ( ZZ>= ` M ) C_ ZZ
14		zssre	\|- ZZ C_ RR
15	13 14	sstri	\|- ( ZZ>= ` M ) C_ RR
16	15	a1i	\|- ( ph -> ( ZZ>= ` M ) C_ RR )
17	2 1	resubcld	\|- ( ph -> ( B - A ) e. RR )
18	1 2	posdifd	\|- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
19	3 18	mpbid	\|- ( ph -> 0 < ( B - A ) )
20	19	gt0ne0d	\|- ( ph -> ( B - A ) =/= 0 )
21	17 20	rereccld	\|- ( ph -> ( 1 / ( B - A ) ) e. RR )
22		0red	\|- ( ph -> 0 e. RR )
23	17 19	recgt0d	\|- ( ph -> 0 < ( 1 / ( B - A ) ) )
24	22 21 23	ltled	\|- ( ph -> 0 <_ ( 1 / ( B - A ) ) )
25		flge0nn0	\|- ( ( ( 1 / ( B - A ) ) e. RR /\ 0 <_ ( 1 / ( B - A ) ) ) -> ( \|_ ` ( 1 / ( B - A ) ) ) e. NN0 )
26	21 24 25	syl2anc	\|- ( ph -> ( \|_ ` ( 1 / ( B - A ) ) ) e. NN0 )
27		peano2nn0	\|- ( ( \|_ ` ( 1 / ( B - A ) ) ) e. NN0 -> ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) e. NN0 )
28	26 27	syl	\|- ( ph -> ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) e. NN0 )
29	8 28	eqeltrid	\|- ( ph -> M e. NN0 )
30	29	nn0zd	\|- ( ph -> M e. ZZ )
31		eqid	\|- ( ZZ>= ` M ) = ( ZZ>= ` M )
32	31	uzsup	\|- ( M e. ZZ -> sup ( ( ZZ>= ` M ) , RR* , < ) = +oo )
33	30 32	syl	\|- ( ph -> sup ( ( ZZ>= ` M ) , RR* , < ) = +oo )
34	4	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> F : ( A (,) B ) --> RR )
35	1	rexrd	\|- ( ph -> A e. RR* )
36	35	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A e. RR* )
37	2	rexrd	\|- ( ph -> B e. RR* )
38	37	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> B e. RR* )
39	1	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A e. RR )
40		eluzelre	\|- ( j e. ( ZZ>= ` M ) -> j e. RR )
41	40	adantl	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. RR )
42		0red	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 e. RR )
43		0red	\|- ( j e. ( ZZ>= ` M ) -> 0 e. RR )
44		1red	\|- ( j e. ( ZZ>= ` M ) -> 1 e. RR )
45	43 44	readdcld	\|- ( j e. ( ZZ>= ` M ) -> ( 0 + 1 ) e. RR )
46	45	adantl	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) e. RR )
47	43	ltp1d	\|- ( j e. ( ZZ>= ` M ) -> 0 < ( 0 + 1 ) )
48	47	adantl	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 < ( 0 + 1 ) )
49		eluzel2	\|- ( j e. ( ZZ>= ` M ) -> M e. ZZ )
50	49	zred	\|- ( j e. ( ZZ>= ` M ) -> M e. RR )
51	50	adantl	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M e. RR )
52	21	flcld	\|- ( ph -> ( \|_ ` ( 1 / ( B - A ) ) ) e. ZZ )
53	52	zred	\|- ( ph -> ( \|_ ` ( 1 / ( B - A ) ) ) e. RR )
54		1red	\|- ( ph -> 1 e. RR )
55	26	nn0ge0d	\|- ( ph -> 0 <_ ( \|_ ` ( 1 / ( B - A ) ) ) )
56	22 53 54 55	leadd1dd	\|- ( ph -> ( 0 + 1 ) <_ ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) )
57	56 8	breqtrrdi	\|- ( ph -> ( 0 + 1 ) <_ M )
58	57	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) <_ M )
59		eluzle	\|- ( j e. ( ZZ>= ` M ) -> M <_ j )
60	59	adantl	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M <_ j )
61	46 51 41 58 60	letrd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) <_ j )
62	42 46 41 48 61	ltletrd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 < j )
63	62	gt0ne0d	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j =/= 0 )
64	41 63	rereccld	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) e. RR )
65	39 64	readdcld	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) e. RR )
66	41 62	elrpd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. RR+ )
67	66	rpreccld	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) e. RR+ )
68	39 67	ltaddrpd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A < ( A + ( 1 / j ) ) )
69	29	nn0red	\|- ( ph -> M e. RR )
70	22 54	readdcld	\|- ( ph -> ( 0 + 1 ) e. RR )
71	53 54	readdcld	\|- ( ph -> ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) e. RR )
72	22	ltp1d	\|- ( ph -> 0 < ( 0 + 1 ) )
73	22 70 71 72 56	ltletrd	\|- ( ph -> 0 < ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) )
74	73 8	breqtrrdi	\|- ( ph -> 0 < M )
75	74	gt0ne0d	\|- ( ph -> M =/= 0 )
76	69 75	rereccld	\|- ( ph -> ( 1 / M ) e. RR )
77	76	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / M ) e. RR )
78	39 77	readdcld	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / M ) ) e. RR )
79	2	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> B e. RR )
80	69 74	elrpd	\|- ( ph -> M e. RR+ )
81	80	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M e. RR+ )
82		1red	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 1 e. RR )
83		0le1	\|- 0 <_ 1
84	83	a1i	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 <_ 1 )
85	81 66 82 84 60	lediv2ad	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) <_ ( 1 / M ) )
86	64 77 39 85	leadd2dd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) <_ ( A + ( 1 / M ) ) )
87	8	eqcomi	\|- ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) = M
88	87	oveq2i	\|- ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) = ( 1 / M )
89	88 76	eqeltrid	\|- ( ph -> ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) e. RR )
90	21 23	elrpd	\|- ( ph -> ( 1 / ( B - A ) ) e. RR+ )
91	71 73	elrpd	\|- ( ph -> ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) e. RR+ )
92		1rp	\|- 1 e. RR+
93	92	a1i	\|- ( ph -> 1 e. RR+ )
94		fllelt	\|- ( ( 1 / ( B - A ) ) e. RR -> ( ( \|_ ` ( 1 / ( B - A ) ) ) <_ ( 1 / ( B - A ) ) /\ ( 1 / ( B - A ) ) < ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
95	21 94	syl	\|- ( ph -> ( ( \|_ ` ( 1 / ( B - A ) ) ) <_ ( 1 / ( B - A ) ) /\ ( 1 / ( B - A ) ) < ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
96	95	simprd	\|- ( ph -> ( 1 / ( B - A ) ) < ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) )
97	90 91 93 96	ltdiv2dd	\|- ( ph -> ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) < ( 1 / ( 1 / ( B - A ) ) ) )
98	17	recnd	\|- ( ph -> ( B - A ) e. CC )
99	98 20	recrecd	\|- ( ph -> ( 1 / ( 1 / ( B - A ) ) ) = ( B - A ) )
100	97 99	breqtrd	\|- ( ph -> ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) < ( B - A ) )
101	89 17 1 100	ltadd2dd	\|- ( ph -> ( A + ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) < ( A + ( B - A ) ) )
102	8	oveq2i	\|- ( 1 / M ) = ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) )
103	102	oveq2i	\|- ( A + ( 1 / M ) ) = ( A + ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
104	103	a1i	\|- ( ph -> ( A + ( 1 / M ) ) = ( A + ( 1 / ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) )
105	1	recnd	\|- ( ph -> A e. CC )
106	2	recnd	\|- ( ph -> B e. CC )
107	105 106	pncan3d	\|- ( ph -> ( A + ( B - A ) ) = B )
108	107	eqcomd	\|- ( ph -> B = ( A + ( B - A ) ) )
109	101 104 108	3brtr4d	\|- ( ph -> ( A + ( 1 / M ) ) < B )
110	109	adantr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / M ) ) < B )
111	65 78 79 86 110	lelttrd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) < B )
112	36 38 65 68 111	eliood	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) e. ( A (,) B ) )
113	34 112	ffvelcdmd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( A + ( 1 / j ) ) ) e. RR )
114	113 9	fmptd	\|- ( ph -> S : ( ZZ>= ` M ) --> RR )
115	1 2 3 4 5 6	dvbdfbdioo	\|- ( ph -> E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
116	69	adantr	\|- ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> M e. RR )
117		simpr	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ( ZZ>= ` M ) )
118	9	fvmpt2	\|- ( ( j e. ( ZZ>= ` M ) /\ ( F ` ( A + ( 1 / j ) ) ) e. RR ) -> ( S ` j ) = ( F ` ( A + ( 1 / j ) ) ) )
119	117 113 118	syl2anc	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( S ` j ) = ( F ` ( A + ( 1 / j ) ) ) )
120	119	fveq2d	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) = ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) )
121	120	adantlr	\|- ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) = ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) )
122		simplr	\|- ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
123	112	adantlr	\|- ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) e. ( A (,) B ) )
124		2fveq3	\|- ( x = ( A + ( 1 / j ) ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) )
125	124	breq1d	\|- ( x = ( A + ( 1 / j ) ) -> ( ( abs ` ( F ` x ) ) <_ b <-> ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) <_ b ) )
126	125	rspccva	\|- ( ( A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b /\ ( A + ( 1 / j ) ) e. ( A (,) B ) ) -> ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) <_ b )
127	122 123 126	syl2anc	\|- ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) <_ b )
128	121 127	eqbrtrd	\|- ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) <_ b )
129	128	a1d	\|- ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
130	129	ralrimiva	\|- ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
131		breq1	\|- ( k = M -> ( k <_ j <-> M <_ j ) )
132	131	imbi1d	\|- ( k = M -> ( ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) <-> ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
133	132	ralbidv	\|- ( k = M -> ( A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) <-> A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
134	133	rspcev	\|- ( ( M e. RR /\ A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
135	116 130 134	syl2anc	\|- ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
136	135	ex	\|- ( ph -> ( A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
137	136	reximdv	\|- ( ph -> ( E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b -> E. b e. RR E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
138	115 137	mpd	\|- ( ph -> E. b e. RR E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
139	16 33 114 138	limsupre	\|- ( ph -> ( limsup ` S ) e. RR )
140	139	recnd	\|- ( ph -> ( limsup ` S ) e. CC )
141		eluzelre	\|- ( j e. ( ZZ>= ` N ) -> j e. RR )
142	141	adantl	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> j e. RR )
143		0red	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 e. RR )
144	52	peano2zd	\|- ( ph -> ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 ) e. ZZ )
145	8 144	eqeltrid	\|- ( ph -> M e. ZZ )
146	145	adantr	\|- ( ( ph /\ x e. RR+ ) -> M e. ZZ )
147	146	zred	\|- ( ( ph /\ x e. RR+ ) -> M e. RR )
148	147	adantr	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M e. RR )
149	74	ad2antrr	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < M )
150		ioomidp	\|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
151	1 2 3 150	syl3anc	\|- ( ph -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
152		ne0i	\|- ( ( ( A + B ) / 2 ) e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
153	151 152	syl	\|- ( ph -> ( A (,) B ) =/= (/) )
154		ioossre	\|- ( A (,) B ) C_ RR
155	154	a1i	\|- ( ph -> ( A (,) B ) C_ RR )
156		dvfre	\|- ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
157	4 155 156	syl2anc	\|- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
158	5	feq2d	\|- ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : ( A (,) B ) --> RR ) )
159	157 158	mpbid	\|- ( ph -> ( RR _D F ) : ( A (,) B ) --> RR )
160	159	ffvelcdmda	\|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
161	160	recnd	\|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
162	161	abscld	\|- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
163		eqid	\|- ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) )
164		eqid	\|- sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
165	153 162 6 163 164	suprnmpt	\|- ( ph -> ( sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR /\ A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) )
166	165	simpld	\|- ( ph -> sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR )
167	7 166	eqeltrid	\|- ( ph -> Y e. RR )
168	167	adantr	\|- ( ( ph /\ x e. RR+ ) -> Y e. RR )
169		rpre	\|- ( x e. RR+ -> x e. RR )
170	169	rehalfcld	\|- ( x e. RR+ -> ( x / 2 ) e. RR )
171	170	adantl	\|- ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR )
172	169	recnd	\|- ( x e. RR+ -> x e. CC )
173	172	adantl	\|- ( ( ph /\ x e. RR+ ) -> x e. CC )
174		2cnd	\|- ( ( ph /\ x e. RR+ ) -> 2 e. CC )
175		rpne0	\|- ( x e. RR+ -> x =/= 0 )
176	175	adantl	\|- ( ( ph /\ x e. RR+ ) -> x =/= 0 )
177		2ne0	\|- 2 =/= 0
178	177	a1i	\|- ( ( ph /\ x e. RR+ ) -> 2 =/= 0 )
179	173 174 176 178	divne0d	\|- ( ( ph /\ x e. RR+ ) -> ( x / 2 ) =/= 0 )
180	168 171 179	redivcld	\|- ( ( ph /\ x e. RR+ ) -> ( Y / ( x / 2 ) ) e. RR )
181	180	flcld	\|- ( ( ph /\ x e. RR+ ) -> ( \|_ ` ( Y / ( x / 2 ) ) ) e. ZZ )
182	181	peano2zd	\|- ( ( ph /\ x e. RR+ ) -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. ZZ )
183	182 146	ifcld	\|- ( ( ph /\ x e. RR+ ) -> if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) e. ZZ )
184	11 183	eqeltrid	\|- ( ( ph /\ x e. RR+ ) -> N e. ZZ )
185	184	zred	\|- ( ( ph /\ x e. RR+ ) -> N e. RR )
186	185	adantr	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> N e. RR )
187	182	zred	\|- ( ( ph /\ x e. RR+ ) -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR )
188		max1	\|- ( ( M e. RR /\ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
189	147 187 188	syl2anc	\|- ( ( ph /\ x e. RR+ ) -> M <_ if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
190	189 11	breqtrrdi	\|- ( ( ph /\ x e. RR+ ) -> M <_ N )
191	190	adantr	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M <_ N )
192		eluzle	\|- ( j e. ( ZZ>= ` N ) -> N <_ j )
193	192	adantl	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> N <_ j )
194	148 186 142 191 193	letrd	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M <_ j )
195	143 148 142 149 194	ltletrd	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < j )
196	195	gt0ne0d	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> j =/= 0 )
197	142 196	rereccld	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> ( 1 / j ) e. RR )
198	142 195	recgt0d	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < ( 1 / j ) )
199	197 198	elrpd	\|- ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> ( 1 / j ) e. RR+ )
200	199	adantr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> ( 1 / j ) e. RR+ )
201	12	biimpi	\|- ( ch -> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
202		simp-5l	\|- ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ph )
203	201 202	syl	\|- ( ch -> ph )
204	203 4	syl	\|- ( ch -> F : ( A (,) B ) --> RR )
205	201	simplrd	\|- ( ch -> z e. ( A (,) B ) )
206	204 205	ffvelcdmd	\|- ( ch -> ( F ` z ) e. RR )
207	206	recnd	\|- ( ch -> ( F ` z ) e. CC )
208	203 114	syl	\|- ( ch -> S : ( ZZ>= ` M ) --> RR )
209		simp-5r	\|- ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> x e. RR+ )
210	201 209	syl	\|- ( ch -> x e. RR+ )
211		eluz2	\|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
212	146 184 190 211	syl3anbrc	\|- ( ( ph /\ x e. RR+ ) -> N e. ( ZZ>= ` M ) )
213	203 210 212	syl2anc	\|- ( ch -> N e. ( ZZ>= ` M ) )
214		uzss	\|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
215	213 214	syl	\|- ( ch -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
216		simp-4r	\|- ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> j e. ( ZZ>= ` N ) )
217	201 216	syl	\|- ( ch -> j e. ( ZZ>= ` N ) )
218	215 217	sseldd	\|- ( ch -> j e. ( ZZ>= ` M ) )
219	208 218	ffvelcdmd	\|- ( ch -> ( S ` j ) e. RR )
220	219	recnd	\|- ( ch -> ( S ` j ) e. CC )
221	203 140	syl	\|- ( ch -> ( limsup ` S ) e. CC )
222	207 220 221	npncand	\|- ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) = ( ( F ` z ) - ( limsup ` S ) ) )
223	222	eqcomd	\|- ( ch -> ( ( F ` z ) - ( limsup ` S ) ) = ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) )
224	223	fveq2d	\|- ( ch -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) = ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) )
225	206 219	resubcld	\|- ( ch -> ( ( F ` z ) - ( S ` j ) ) e. RR )
226	203 139	syl	\|- ( ch -> ( limsup ` S ) e. RR )
227	219 226	resubcld	\|- ( ch -> ( ( S ` j ) - ( limsup ` S ) ) e. RR )
228	225 227	readdcld	\|- ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) e. RR )
229	228	recnd	\|- ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) e. CC )
230	229	abscld	\|- ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) e. RR )
231	225	recnd	\|- ( ch -> ( ( F ` z ) - ( S ` j ) ) e. CC )
232	231	abscld	\|- ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) e. RR )
233	227	recnd	\|- ( ch -> ( ( S ` j ) - ( limsup ` S ) ) e. CC )
234	233	abscld	\|- ( ch -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) e. RR )
235	232 234	readdcld	\|- ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) e. RR )
236	210	rpred	\|- ( ch -> x e. RR )
237	231 233	abstrid	\|- ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) <_ ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) )
238	236	rehalfcld	\|- ( ch -> ( x / 2 ) e. RR )
239	207 220	abssubd	\|- ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) = ( abs ` ( ( S ` j ) - ( F ` z ) ) ) )
240	203 218 119	syl2anc	\|- ( ch -> ( S ` j ) = ( F ` ( A + ( 1 / j ) ) ) )
241	240	fvoveq1d	\|- ( ch -> ( abs ` ( ( S ` j ) - ( F ` z ) ) ) = ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) )
242	203 218 113	syl2anc	\|- ( ch -> ( F ` ( A + ( 1 / j ) ) ) e. RR )
243	242 206	resubcld	\|- ( ch -> ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) e. RR )
244	243	recnd	\|- ( ch -> ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) e. CC )
245	244	abscld	\|- ( ch -> ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) e. RR )
246	203 167	syl	\|- ( ch -> Y e. RR )
247	203 218 65	syl2anc	\|- ( ch -> ( A + ( 1 / j ) ) e. RR )
248	154 205	sselid	\|- ( ch -> z e. RR )
249	247 248	resubcld	\|- ( ch -> ( ( A + ( 1 / j ) ) - z ) e. RR )
250	246 249	remulcld	\|- ( ch -> ( Y x. ( ( A + ( 1 / j ) ) - z ) ) e. RR )
251	203 1	syl	\|- ( ch -> A e. RR )
252	203 2	syl	\|- ( ch -> B e. RR )
253	203 5	syl	\|- ( ch -> dom ( RR _D F ) = ( A (,) B ) )
254	165	simprd	\|- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
255	7	breq2i	\|- ( ( abs ` ( ( RR _D F ) ` x ) ) <_ Y <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
256	255	ralbii	\|- ( A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
257	254 256	sylibr	\|- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
258	203 257	syl	\|- ( ch -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
259		2fveq3	\|- ( w = x -> ( abs ` ( ( RR _D F ) ` w ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
260	259	breq1d	\|- ( w = x -> ( ( abs ` ( ( RR _D F ) ` w ) ) <_ Y <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ Y ) )
261	260	cbvralvw	\|- ( A. w e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` w ) ) <_ Y <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
262	258 261	sylibr	\|- ( ch -> A. w e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` w ) ) <_ Y )
263	248	rexrd	\|- ( ch -> z e. RR* )
264	203 37	syl	\|- ( ch -> B e. RR* )
265	248 251	resubcld	\|- ( ch -> ( z - A ) e. RR )
266	265	recnd	\|- ( ch -> ( z - A ) e. CC )
267	266	abscld	\|- ( ch -> ( abs ` ( z - A ) ) e. RR )
268	15 218	sselid	\|- ( ch -> j e. RR )
269	203 218 63	syl2anc	\|- ( ch -> j =/= 0 )
270	268 269	rereccld	\|- ( ch -> ( 1 / j ) e. RR )
271	265	leabsd	\|- ( ch -> ( z - A ) <_ ( abs ` ( z - A ) ) )
272	201	simprd	\|- ( ch -> ( abs ` ( z - A ) ) < ( 1 / j ) )
273	265 267 270 271 272	lelttrd	\|- ( ch -> ( z - A ) < ( 1 / j ) )
274	248 251 270	ltsubadd2d	\|- ( ch -> ( ( z - A ) < ( 1 / j ) <-> z < ( A + ( 1 / j ) ) ) )
275	273 274	mpbid	\|- ( ch -> z < ( A + ( 1 / j ) ) )
276	203 218 111	syl2anc	\|- ( ch -> ( A + ( 1 / j ) ) < B )
277	263 264 247 275 276	eliood	\|- ( ch -> ( A + ( 1 / j ) ) e. ( z (,) B ) )
278	251 252 204 253 246 262 205 277	dvbdfbdioolem1	\|- ( ch -> ( ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( Y x. ( ( A + ( 1 / j ) ) - z ) ) /\ ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( Y x. ( B - A ) ) ) )
279	278	simpld	\|- ( ch -> ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( Y x. ( ( A + ( 1 / j ) ) - z ) ) )
280	203 218 64	syl2anc	\|- ( ch -> ( 1 / j ) e. RR )
281	246 280	remulcld	\|- ( ch -> ( Y x. ( 1 / j ) ) e. RR )
282	159 151	ffvelcdmd	\|- ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. RR )
283	282	recnd	\|- ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. CC )
284	283	abscld	\|- ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) e. RR )
285	283	absge0d	\|- ( ph -> 0 <_ ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
286		2fveq3	\|- ( x = ( ( A + B ) / 2 ) -> ( abs ` ( ( RR _D F ) ` x ) ) = ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
287	7	eqcomi	\|- sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = Y
288	287	a1i	\|- ( x = ( ( A + B ) / 2 ) -> sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = Y )
289	286 288	breq12d	\|- ( x = ( ( A + B ) / 2 ) -> ( ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y ) )
290	289	rspcva	\|- ( ( ( ( A + B ) / 2 ) e. ( A (,) B ) /\ A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y )
291	151 254 290	syl2anc	\|- ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y )
292	22 284 167 285 291	letrd	\|- ( ph -> 0 <_ Y )
293	203 292	syl	\|- ( ch -> 0 <_ Y )
294	203 35	syl	\|- ( ch -> A e. RR* )
295		ioogtlb	\|- ( ( A e. RR* /\ B e. RR* /\ z e. ( A (,) B ) ) -> A < z )
296	294 264 205 295	syl3anc	\|- ( ch -> A < z )
297	251 248 247 296	ltsub2dd	\|- ( ch -> ( ( A + ( 1 / j ) ) - z ) < ( ( A + ( 1 / j ) ) - A ) )
298	203 105	syl	\|- ( ch -> A e. CC )
299	280	recnd	\|- ( ch -> ( 1 / j ) e. CC )
300	298 299	pncan2d	\|- ( ch -> ( ( A + ( 1 / j ) ) - A ) = ( 1 / j ) )
301	297 300	breqtrd	\|- ( ch -> ( ( A + ( 1 / j ) ) - z ) < ( 1 / j ) )
302	249 270 301	ltled	\|- ( ch -> ( ( A + ( 1 / j ) ) - z ) <_ ( 1 / j ) )
303	249 270 246 293 302	lemul2ad	\|- ( ch -> ( Y x. ( ( A + ( 1 / j ) ) - z ) ) <_ ( Y x. ( 1 / j ) ) )
304	281	adantr	\|- ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) e. RR )
305	238	adantr	\|- ( ( ch /\ Y = 0 ) -> ( x / 2 ) e. RR )
306		oveq1	\|- ( Y = 0 -> ( Y x. ( 1 / j ) ) = ( 0 x. ( 1 / j ) ) )
307	299	mul02d	\|- ( ch -> ( 0 x. ( 1 / j ) ) = 0 )
308	306 307	sylan9eqr	\|- ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) = 0 )
309	210	rphalfcld	\|- ( ch -> ( x / 2 ) e. RR+ )
310	309	rpgt0d	\|- ( ch -> 0 < ( x / 2 ) )
311	310	adantr	\|- ( ( ch /\ Y = 0 ) -> 0 < ( x / 2 ) )
312	308 311	eqbrtrd	\|- ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) < ( x / 2 ) )
313	304 305 312	ltled	\|- ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
314	246	adantr	\|- ( ( ch /\ -. Y = 0 ) -> Y e. RR )
315	293	adantr	\|- ( ( ch /\ -. Y = 0 ) -> 0 <_ Y )
316		neqne	\|- ( -. Y = 0 -> Y =/= 0 )
317	316	adantl	\|- ( ( ch /\ -. Y = 0 ) -> Y =/= 0 )
318	314 315 317	ne0gt0d	\|- ( ( ch /\ -. Y = 0 ) -> 0 < Y )
319	281	adantr	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) e. RR )
320	15 213	sselid	\|- ( ch -> N e. RR )
321		0red	\|- ( ch -> 0 e. RR )
322	203 210 147	syl2anc	\|- ( ch -> M e. RR )
323	203 74	syl	\|- ( ch -> 0 < M )
324	203 210 190	syl2anc	\|- ( ch -> M <_ N )
325	321 322 320 323 324	ltletrd	\|- ( ch -> 0 < N )
326	325	gt0ne0d	\|- ( ch -> N =/= 0 )
327	320 326	rereccld	\|- ( ch -> ( 1 / N ) e. RR )
328	246 327	remulcld	\|- ( ch -> ( Y x. ( 1 / N ) ) e. RR )
329	328	adantr	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) e. RR )
330	238	adantr	\|- ( ( ch /\ 0 < Y ) -> ( x / 2 ) e. RR )
331	280	adantr	\|- ( ( ch /\ 0 < Y ) -> ( 1 / j ) e. RR )
332	327	adantr	\|- ( ( ch /\ 0 < Y ) -> ( 1 / N ) e. RR )
333	246	adantr	\|- ( ( ch /\ 0 < Y ) -> Y e. RR )
334	293	adantr	\|- ( ( ch /\ 0 < Y ) -> 0 <_ Y )
335	320 325	elrpd	\|- ( ch -> N e. RR+ )
336	203 218 66	syl2anc	\|- ( ch -> j e. RR+ )
337		1red	\|- ( ch -> 1 e. RR )
338	83	a1i	\|- ( ch -> 0 <_ 1 )
339	217 192	syl	\|- ( ch -> N <_ j )
340	335 336 337 338 339	lediv2ad	\|- ( ch -> ( 1 / j ) <_ ( 1 / N ) )
341	340	adantr	\|- ( ( ch /\ 0 < Y ) -> ( 1 / j ) <_ ( 1 / N ) )
342	331 332 333 334 341	lemul2ad	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) <_ ( Y x. ( 1 / N ) ) )
343	236	recnd	\|- ( ch -> x e. CC )
344		2cnd	\|- ( ch -> 2 e. CC )
345	210	rpne0d	\|- ( ch -> x =/= 0 )
346	177	a1i	\|- ( ch -> 2 =/= 0 )
347	343 344 345 346	divne0d	\|- ( ch -> ( x / 2 ) =/= 0 )
348	246 238 347	redivcld	\|- ( ch -> ( Y / ( x / 2 ) ) e. RR )
349	348	adantr	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. RR )
350		simpr	\|- ( ( ch /\ 0 < Y ) -> 0 < Y )
351	310	adantr	\|- ( ( ch /\ 0 < Y ) -> 0 < ( x / 2 ) )
352	333 330 350 351	divgt0d	\|- ( ( ch /\ 0 < Y ) -> 0 < ( Y / ( x / 2 ) ) )
353	349 352	elrpd	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. RR+ )
354	353	rprecred	\|- ( ( ch /\ 0 < Y ) -> ( 1 / ( Y / ( x / 2 ) ) ) e. RR )
355	335	adantr	\|- ( ( ch /\ 0 < Y ) -> N e. RR+ )
356		1red	\|- ( ( ch /\ 0 < Y ) -> 1 e. RR )
357	83	a1i	\|- ( ( ch /\ 0 < Y ) -> 0 <_ 1 )
358	348	flcld	\|- ( ch -> ( \|_ ` ( Y / ( x / 2 ) ) ) e. ZZ )
359	358	peano2zd	\|- ( ch -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. ZZ )
360	359	zred	\|- ( ch -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR )
361	203 145	syl	\|- ( ch -> M e. ZZ )
362	359 361	ifcld	\|- ( ch -> if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) e. ZZ )
363	11 362	eqeltrid	\|- ( ch -> N e. ZZ )
364	363	zred	\|- ( ch -> N e. RR )
365		flltp1	\|- ( ( Y / ( x / 2 ) ) e. RR -> ( Y / ( x / 2 ) ) < ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) )
366	348 365	syl	\|- ( ch -> ( Y / ( x / 2 ) ) < ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) )
367	203 69	syl	\|- ( ch -> M e. RR )
368		max2	\|- ( ( M e. RR /\ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR ) -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
369	367 360 368	syl2anc	\|- ( ch -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
370	369 11	breqtrrdi	\|- ( ch -> ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ N )
371	348 360 364 366 370	ltletrd	\|- ( ch -> ( Y / ( x / 2 ) ) < N )
372	348 320 371	ltled	\|- ( ch -> ( Y / ( x / 2 ) ) <_ N )
373	372	adantr	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) <_ N )
374	353 355 356 357 373	lediv2ad	\|- ( ( ch /\ 0 < Y ) -> ( 1 / N ) <_ ( 1 / ( Y / ( x / 2 ) ) ) )
375	332 354 333 334 374	lemul2ad	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) <_ ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) )
376	333	recnd	\|- ( ( ch /\ 0 < Y ) -> Y e. CC )
377	349	recnd	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. CC )
378	352	gt0ne0d	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) =/= 0 )
379	376 377 378	divrecd	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( Y / ( x / 2 ) ) ) = ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) )
380	330	recnd	\|- ( ( ch /\ 0 < Y ) -> ( x / 2 ) e. CC )
381	350	gt0ne0d	\|- ( ( ch /\ 0 < Y ) -> Y =/= 0 )
382	347	adantr	\|- ( ( ch /\ 0 < Y ) -> ( x / 2 ) =/= 0 )
383	376 380 381 382	ddcand	\|- ( ( ch /\ 0 < Y ) -> ( Y / ( Y / ( x / 2 ) ) ) = ( x / 2 ) )
384	379 383	eqtr3d	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) = ( x / 2 ) )
385	375 384	breqtrd	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) <_ ( x / 2 ) )
386	319 329 330 342 385	letrd	\|- ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
387	318 386	syldan	\|- ( ( ch /\ -. Y = 0 ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
388	313 387	pm2.61dan	\|- ( ch -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
389	250 281 238 303 388	letrd	\|- ( ch -> ( Y x. ( ( A + ( 1 / j ) ) - z ) ) <_ ( x / 2 ) )
390	245 250 238 279 389	letrd	\|- ( ch -> ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( x / 2 ) )
391	241 390	eqbrtrd	\|- ( ch -> ( abs ` ( ( S ` j ) - ( F ` z ) ) ) <_ ( x / 2 ) )
392	239 391	eqbrtrd	\|- ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) <_ ( x / 2 ) )
393		simpllr	\|- ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
394	201 393	syl	\|- ( ch -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
395	232 234 238 238 392 394	leltaddd	\|- ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) < ( ( x / 2 ) + ( x / 2 ) ) )
396	343	2halvesd	\|- ( ch -> ( ( x / 2 ) + ( x / 2 ) ) = x )
397	395 396	breqtrd	\|- ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) < x )
398	230 235 236 237 397	lelttrd	\|- ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) < x )
399	224 398	eqbrtrd	\|- ( ch -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
400	12 399	sylbir	\|- ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
401	400	adantrl	\|- ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
402	401	ex	\|- ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) -> ( ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
403	402	ralrimiva	\|- ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
404		brimralrspcev	\|- ( ( ( 1 / j ) e. RR+ /\ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
405	200 403 404	syl2anc	\|- ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
406		simpr	\|- ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> b <_ N )
407	406	iftrued	\|- ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> if ( b <_ N , N , b ) = N )
408		uzid	\|- ( N e. ZZ -> N e. ( ZZ>= ` N ) )
409	184 408	syl	\|- ( ( ph /\ x e. RR+ ) -> N e. ( ZZ>= ` N ) )
410	409	adantr	\|- ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> N e. ( ZZ>= ` N ) )
411	407 410	eqeltrd	\|- ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
412	411	adantlr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
413		iffalse	\|- ( -. b <_ N -> if ( b <_ N , N , b ) = b )
414	413	adantl	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> if ( b <_ N , N , b ) = b )
415	184	ad2antrr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N e. ZZ )
416		simplr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. ZZ )
417	415	zred	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N e. RR )
418	416	zred	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. RR )
419		simpr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> -. b <_ N )
420	417 418	ltnled	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> ( N < b <-> -. b <_ N ) )
421	419 420	mpbird	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N < b )
422	417 418 421	ltled	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N <_ b )
423		eluz2	\|- ( b e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ b e. ZZ /\ N <_ b ) )
424	415 416 422 423	syl3anbrc	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. ( ZZ>= ` N ) )
425	414 424	eqeltrd	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
426	412 425	pm2.61dan	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
427	426	adantr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
428		simpr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
429		simpr	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b e. ZZ )
430	184	adantr	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> N e. ZZ )
431	430 429	ifcld	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ZZ )
432	429	zred	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b e. RR )
433	430	zred	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> N e. RR )
434		max1	\|- ( ( b e. RR /\ N e. RR ) -> b <_ if ( b <_ N , N , b ) )
435	432 433 434	syl2anc	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b <_ if ( b <_ N , N , b ) )
436		eluz2	\|- ( if ( b <_ N , N , b ) e. ( ZZ>= ` b ) <-> ( b e. ZZ /\ if ( b <_ N , N , b ) e. ZZ /\ b <_ if ( b <_ N , N , b ) ) )
437	429 431 435 436	syl3anbrc	\|- ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` b ) )
438	437	adantr	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` b ) )
439		fveq2	\|- ( c = if ( b <_ N , N , b ) -> ( S ` c ) = ( S ` if ( b <_ N , N , b ) ) )
440	439	eleq1d	\|- ( c = if ( b <_ N , N , b ) -> ( ( S ` c ) e. CC <-> ( S ` if ( b <_ N , N , b ) ) e. CC ) )
441	439	fvoveq1d	\|- ( c = if ( b <_ N , N , b ) -> ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) = ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) )
442	441	breq1d	\|- ( c = if ( b <_ N , N , b ) -> ( ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) <-> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
443	440 442	anbi12d	\|- ( c = if ( b <_ N , N , b ) -> ( ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) <-> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
444	443	rspccva	\|- ( ( A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ if ( b <_ N , N , b ) e. ( ZZ>= ` b ) ) -> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
445	428 438 444	syl2anc	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
446	445	simprd	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) )
447		fveq2	\|- ( j = if ( b <_ N , N , b ) -> ( S ` j ) = ( S ` if ( b <_ N , N , b ) ) )
448	447	fvoveq1d	\|- ( j = if ( b <_ N , N , b ) -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) = ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) )
449	448	breq1d	\|- ( j = if ( b <_ N , N , b ) -> ( ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) <-> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
450	449	rspcev	\|- ( ( if ( b <_ N , N , b ) e. ( ZZ>= ` N ) /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
451	427 446 450	syl2anc	\|- ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
452		ax-resscn	\|- RR C_ CC
453	452	a1i	\|- ( ph -> RR C_ CC )
454	4 453	fssd	\|- ( ph -> F : ( A (,) B ) --> CC )
455		dvcn	\|- ( ( ( RR C_ CC /\ F : ( A (,) B ) --> CC /\ ( A (,) B ) C_ RR ) /\ dom ( RR _D F ) = ( A (,) B ) ) -> F e. ( ( A (,) B ) -cn-> CC ) )
456	453 454 155 5 455	syl31anc	\|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
457		cncfcdm	\|- ( ( RR C_ CC /\ F e. ( ( A (,) B ) -cn-> CC ) ) -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
458	453 456 457	syl2anc	\|- ( ph -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
459	4 458	mpbird	\|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
460	112 10	fmptd	\|- ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
461		eqid	\|- ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) ) = ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) )
462		climrel	\|- Rel ~~>
463	462	a1i	\|- ( ph -> Rel ~~> )
464		fvex	\|- ( ZZ>= ` M ) e. _V
465	464	mptex	\|- ( j e. ( ZZ>= ` M ) \|-> A ) e. _V
466	465	a1i	\|- ( ph -> ( j e. ( ZZ>= ` M ) \|-> A ) e. _V )
467		eqidd	\|- ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) \|-> A ) = ( j e. ( ZZ>= ` M ) \|-> A ) )
468		eqidd	\|- ( ( ( ph /\ m e. ( ZZ>= ` M ) ) /\ j = m ) -> A = A )
469		simpr	\|- ( ( ph /\ m e. ( ZZ>= ` M ) ) -> m e. ( ZZ>= ` M ) )
470	1	adantr	\|- ( ( ph /\ m e. ( ZZ>= ` M ) ) -> A e. RR )
471	467 468 469 470	fvmptd	\|- ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) \|-> A ) ` m ) = A )
472	31 145 466 105 471	climconst	\|- ( ph -> ( j e. ( ZZ>= ` M ) \|-> A ) ~~> A )
473	464	mptex	\|- ( j e. ( ZZ>= ` M ) \|-> ( A + ( 1 / j ) ) ) e. _V
474	10 473	eqeltri	\|- R e. _V
475	474	a1i	\|- ( ph -> R e. _V )
476		1cnd	\|- ( ph -> 1 e. CC )
477		elnnnn0b	\|- ( M e. NN <-> ( M e. NN0 /\ 0 < M ) )
478	29 74 477	sylanbrc	\|- ( ph -> M e. NN )
479		divcnvg	\|- ( ( 1 e. CC /\ M e. NN ) -> ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) ~~> 0 )
480	476 478 479	syl2anc	\|- ( ph -> ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) ~~> 0 )
481		eqidd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) \|-> A ) = ( j e. ( ZZ>= ` M ) \|-> A ) )
482		eqidd	\|- ( ( ( ph /\ i e. ( ZZ>= ` M ) ) /\ j = i ) -> A = A )
483		simpr	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
484	1	adantr	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A e. RR )
485	481 482 483 484	fvmptd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) \|-> A ) ` i ) = A )
486	105	adantr	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A e. CC )
487	485 486	eqeltrd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) \|-> A ) ` i ) e. CC )
488		eqidd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) = ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) )
489		oveq2	\|- ( j = i -> ( 1 / j ) = ( 1 / i ) )
490	489	adantl	\|- ( ( ( ph /\ i e. ( ZZ>= ` M ) ) /\ j = i ) -> ( 1 / j ) = ( 1 / i ) )
491	15 483	sselid	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
492		0red	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 e. RR )
493	69	adantr	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
494	74	adantr	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 < M )
495		eluzle	\|- ( i e. ( ZZ>= ` M ) -> M <_ i )
496	495	adantl	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
497	492 493 491 494 496	ltletrd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 < i )
498	497	gt0ne0d	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i =/= 0 )
499	491 498	rereccld	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( 1 / i ) e. RR )
500	488 490 483 499	fvmptd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) ` i ) = ( 1 / i ) )
501	491	recnd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. CC )
502	501 498	reccld	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( 1 / i ) e. CC )
503	500 502	eqeltrd	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) ` i ) e. CC )
504	489	oveq2d	\|- ( j = i -> ( A + ( 1 / j ) ) = ( A + ( 1 / i ) ) )
505	484 499	readdcld	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( A + ( 1 / i ) ) e. RR )
506	10 504 483 505	fvmptd3	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( R ` i ) = ( A + ( 1 / i ) ) )
507	485 500	oveq12d	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( ( j e. ( ZZ>= ` M ) \|-> A ) ` i ) + ( ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) ` i ) ) = ( A + ( 1 / i ) ) )
508	506 507	eqtr4d	\|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( R ` i ) = ( ( ( j e. ( ZZ>= ` M ) \|-> A ) ` i ) + ( ( j e. ( ZZ>= ` M ) \|-> ( 1 / j ) ) ` i ) ) )
509	31 145 472 475 480 487 503 508	climadd	\|- ( ph -> R ~~> ( A + 0 ) )
510	105	addridd	\|- ( ph -> ( A + 0 ) = A )
511	509 510	breqtrd	\|- ( ph -> R ~~> A )
512		releldm	\|- ( ( Rel ~~> /\ R ~~> A ) -> R e. dom ~~> )
513	463 511 512	syl2anc	\|- ( ph -> R e. dom ~~> )
514		fveq2	\|- ( l = k -> ( ZZ>= ` l ) = ( ZZ>= ` k ) )
515		fveq2	\|- ( l = k -> ( R ` l ) = ( R ` k ) )
516	515	oveq2d	\|- ( l = k -> ( ( R ` h ) - ( R ` l ) ) = ( ( R ` h ) - ( R ` k ) ) )
517	516	fveq2d	\|- ( l = k -> ( abs ` ( ( R ` h ) - ( R ` l ) ) ) = ( abs ` ( ( R ` h ) - ( R ` k ) ) ) )
518	517	breq1d	\|- ( l = k -> ( ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
519	514 518	raleqbidv	\|- ( l = k -> ( A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
520	519	cbvrabv	\|- { l e. ( ZZ>= ` M ) \| A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) \| A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
521		fveq2	\|- ( h = i -> ( R ` h ) = ( R ` i ) )
522	521	fvoveq1d	\|- ( h = i -> ( abs ` ( ( R ` h ) - ( R ` k ) ) ) = ( abs ` ( ( R ` i ) - ( R ` k ) ) ) )
523	522	breq1d	\|- ( h = i -> ( ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
524	523	cbvralvw	\|- ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
525	524	rgenw	\|- A. k e. ( ZZ>= ` M ) ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
526		rabbi	\|- ( A. k e. ( ZZ>= ` M ) ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) <-> { k e. ( ZZ>= ` M ) \| A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) \| A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } )
527	525 526	mpbi	\|- { k e. ( ZZ>= ` M ) \| A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) \| A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
528	520 527	eqtri	\|- { l e. ( ZZ>= ` M ) \| A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) \| A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
529	528	infeq1i	\|- inf ( { l e. ( ZZ>= ` M ) \| A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < ) = inf ( { k e. ( ZZ>= ` M ) \| A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < )
530	1 2 3 459 5 6 30 460 461 513 529	ioodvbdlimc1lem1	\|- ( ph -> ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) ) ~~> ( limsup ` ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) ) ) )
531	10	fvmpt2	\|- ( ( j e. ( ZZ>= ` M ) /\ ( A + ( 1 / j ) ) e. RR ) -> ( R ` j ) = ( A + ( 1 / j ) ) )
532	117 65 531	syl2anc	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( R ` j ) = ( A + ( 1 / j ) ) )
533	532	eqcomd	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) = ( R ` j ) )
534	533	fveq2d	\|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( A + ( 1 / j ) ) ) = ( F ` ( R ` j ) ) )
535	534	mpteq2dva	\|- ( ph -> ( j e. ( ZZ>= ` M ) \|-> ( F ` ( A + ( 1 / j ) ) ) ) = ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) ) )
536	9 535	eqtrid	\|- ( ph -> S = ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) ) )
537	536	fveq2d	\|- ( ph -> ( limsup ` S ) = ( limsup ` ( j e. ( ZZ>= ` M ) \|-> ( F ` ( R ` j ) ) ) ) )
538	530 536 537	3brtr4d	\|- ( ph -> S ~~> ( limsup ` S ) )
539	464	mptex	\|- ( j e. ( ZZ>= ` M ) \|-> ( F ` ( A + ( 1 / j ) ) ) ) e. _V
540	9 539	eqeltri	\|- S e. _V
541	540	a1i	\|- ( ph -> S e. _V )
542		eqidd	\|- ( ( ph /\ c e. ZZ ) -> ( S ` c ) = ( S ` c ) )
543	541 542	clim	\|- ( ph -> ( S ~~> ( limsup ` S ) <-> ( ( limsup ` S ) e. CC /\ A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) ) ) )
544	538 543	mpbid	\|- ( ph -> ( ( limsup ` S ) e. CC /\ A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) ) )
545	544	simprd	\|- ( ph -> A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) )
546	545	adantr	\|- ( ( ph /\ x e. RR+ ) -> A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) )
547		simpr	\|- ( ( ph /\ x e. RR+ ) -> x e. RR+ )
548	547	rphalfcld	\|- ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
549		breq2	\|- ( a = ( x / 2 ) -> ( ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a <-> ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
550	549	anbi2d	\|- ( a = ( x / 2 ) -> ( ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) <-> ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
551	550	rexralbidv	\|- ( a = ( x / 2 ) -> ( E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) <-> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
552	551	rspccva	\|- ( ( A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) /\ ( x / 2 ) e. RR+ ) -> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
553	546 548 552	syl2anc	\|- ( ( ph /\ x e. RR+ ) -> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
554	451 553	r19.29a	\|- ( ( ph /\ x e. RR+ ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
555	405 554	r19.29a	\|- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
556	555	ralrimiva	\|- ( ph -> A. x e. RR+ E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
557		ioosscn	\|- ( A (,) B ) C_ CC
558	557	a1i	\|- ( ph -> ( A (,) B ) C_ CC )
559	454 558 105	ellimc3	\|- ( ph -> ( ( limsup ` S ) e. ( F limCC A ) <-> ( ( limsup ` S ) e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) ) ) )
560	140 556 559	mpbir2and	\|- ( ph -> ( limsup ` S ) e. ( F limCC A ) )

Metamath Proof Explorer

Theorem ioodvbdlimc1lem2

Proof