ioodvbdlimc2lem

Description: Limit at the upper 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	ioodvbdlimc2lem.a	\|- ( ph -> A e. RR )
	ioodvbdlimc2lem.b	\|- ( ph -> B e. RR )
	ioodvbdlimc2lem.altb	\|- ( ph -> A < B )
	ioodvbdlimc2lem.f	\|- ( ph -> F : ( A (,) B ) --> RR )
	ioodvbdlimc2lem.dmdv	\|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
	ioodvbdlimc2lem.dvbd	\|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
	ioodvbdlimc2lem.y	\|- Y = sup ( ran ( x e. ( A (,) B ) \|-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
	ioodvbdlimc2lem.m	\|- M = ( ( \|_ ` ( 1 / ( B - A ) ) ) + 1 )
	ioodvbdlimc2lem.s	\|- S = ( j e. ( ZZ>= ` M ) \|-> ( F ` ( B - ( 1 / j ) ) ) )
	ioodvbdlimc2lem.r	\|- R = ( j e. ( ZZ>= ` M ) \|-> ( B - ( 1 / j ) ) )
	ioodvbdlimc2lem.n	\|- N = if ( M <_ ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( \|_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
	ioodvbdlimc2lem.ch	\|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) )
Assertion	ioodvbdlimc2lem	\|- ( ph -> ( limsup ` S ) e. ( F limCC B ) )

Proof

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

Metamath Proof Explorer

Theorem ioodvbdlimc2lem

Proof