Theorem ioodvbdlimc1lem1

Description: If F has bounded derivative on ( A (,) B ) then a sequence of points in its image converges to its limsup . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	ioodvbdlimc1lem1.a	|- ( ph -> A e. RR )
	ioodvbdlimc1lem1.b	|- ( ph -> B e. RR )
	ioodvbdlimc1lem1.altb	|- ( ph -> A < B )
	ioodvbdlimc1lem1.f	|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
	ioodvbdlimc1lem1.dmdv	|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
	ioodvbdlimc1lem1.dvbd	|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
	ioodvbdlimc1lem1.m	|- ( ph -> M e. ZZ )
	ioodvbdlimc1lem1.r	|- ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
	ioodvbdlimc1lem1.s	|- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )
	ioodvbdlimc1lem1.rcnv	|- ( ph -> R e. dom ~~> )
	ioodvbdlimc1lem1.k	|- K = 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 , < )
Assertion	ioodvbdlimc1lem1	|- ( ph -> S ~~> ( limsup ` S ) )

Proof

Step	Hyp	Ref	Expression
1		ioodvbdlimc1lem1.a	|- ( ph -> A e. RR )
2		ioodvbdlimc1lem1.b	|- ( ph -> B e. RR )
3		ioodvbdlimc1lem1.altb	|- ( ph -> A < B )
4		ioodvbdlimc1lem1.f	|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
5		ioodvbdlimc1lem1.dmdv	|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6		ioodvbdlimc1lem1.dvbd	|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
7		ioodvbdlimc1lem1.m	|- ( ph -> M e. ZZ )
8		ioodvbdlimc1lem1.r	|- ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
9		ioodvbdlimc1lem1.s	|- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )
10		ioodvbdlimc1lem1.rcnv	|- ( ph -> R e. dom ~~> )
11		ioodvbdlimc1lem1.k	|- K = 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 , < )
12		eqid	|- ( ZZ>= ` M ) = ( ZZ>= ` M )
13		cncff	|- ( F e. ( ( A (,) B ) -cn-> RR ) -> F : ( A (,) B ) --> RR )
14	4 13	syl	|- ( ph -> F : ( A (,) B ) --> RR )
15	14	adantr	|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> F : ( A (,) B ) --> RR )
16	8	ffvelrnda	|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( R ` j ) e. ( A (,) B ) )
17	15 16	ffvelrnd	|- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( R ` j ) ) e. RR )
18	17 9	fmptd	|- ( ph -> S : ( ZZ>= ` M ) --> RR )
19		ssrab2	|- { 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 ) ) } C_ ( ZZ>= ` M )
20		rpre	|- ( x e. RR+ -> x e. RR )
21	20	adantl	|- ( ( ph /\ x e. RR+ ) -> x e. RR )
22		2fveq3	|- ( z = x -> ( abs ` ( ( RR _D F ) ` z ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
23	22	cbvmptv	|- ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) = ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
24	23	rneqi	|- ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) = ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
25	24	supeq1i	|- sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
26		ioomidp	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
27	1 2 3 26	syl3anc	|- ( ph -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
28	27	ne0d	|- ( ph -> ( A (,) B ) =/= (/) )
29		ioossre	|- ( A (,) B ) C_ RR
30	29	a1i	|- ( ph -> ( A (,) B ) C_ RR )
31		dvfre	|- ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
32	14 30 31	syl2anc	|- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
33	5	feq2d	|- ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : ( A (,) B ) --> RR ) )
34	32 33	mpbid	|- ( ph -> ( RR _D F ) : ( A (,) B ) --> RR )
35		ax-resscn	|- RR C_ CC
36	35	a1i	|- ( ph -> RR C_ CC )
37	34 36	fssd	|- ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
38	37	ffvelrnda	|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
39	38	abscld	|- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
40		eqid	|- ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
41		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 , < )
42	28 39 6 40 41	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 , < ) ) )
43	42	simpld	|- ( ph -> sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR )
44	25 43	eqeltrid	|- ( ph -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
45	44	adantr	|- ( ( ph /\ x e. RR+ ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
46		peano2re	|- ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
47	45 46	syl	|- ( ( ph /\ x e. RR+ ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
48		0red	|- ( ph -> 0 e. RR )
49		1red	|- ( ph -> 1 e. RR )
50	48 49	readdcld	|- ( ph -> ( 0 + 1 ) e. RR )
51	44 46	syl	|- ( ph -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
52	48	ltp1d	|- ( ph -> 0 < ( 0 + 1 ) )
53	37 27	ffvelrnd	|- ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. CC )
54	53	abscld	|- ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) e. RR )
55	53	absge0d	|- ( ph -> 0 <_ ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
56	42	simprd	|- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
57		2fveq3	|- ( y = x -> ( abs ` ( ( RR _D F ) ` y ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
58	25	a1i	|- ( y = x -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
59	57 58	breq12d	|- ( y = x -> ( ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) )
60	59	cbvralvw	|- ( A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
61	56 60	sylibr	|- ( ph -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
62		2fveq3	|- ( y = ( ( A + B ) / 2 ) -> ( abs ` ( ( RR _D F ) ` y ) ) = ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
63	62	breq1d	|- ( y = ( ( A + B ) / 2 ) -> ( ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) ) )
64	63	rspcva	|- ( ( ( ( A + B ) / 2 ) e. ( A (,) B ) /\ A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) ) -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
65	27 61 64	syl2anc	|- ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
66	48 54 44 55 65	letrd	|- ( ph -> 0 <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
67	48 44 49 66	leadd1dd	|- ( ph -> ( 0 + 1 ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
68	48 50 51 52 67	ltletrd	|- ( ph -> 0 < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
69	68	gt0ne0d	|- ( ph -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) =/= 0 )
70	69	adantr	|- ( ( ph /\ x e. RR+ ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) =/= 0 )
71	21 47 70	redivcld	|- ( ( ph /\ x e. RR+ ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR )
72		rpgt0	|- ( x e. RR+ -> 0 < x )
73	72	adantl	|- ( ( ph /\ x e. RR+ ) -> 0 < x )
74	68	adantr	|- ( ( ph /\ x e. RR+ ) -> 0 < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
75	21 47 73 74	divgt0d	|- ( ( ph /\ x e. RR+ ) -> 0 < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
76	71 75	elrpd	|- ( ( ph /\ x e. RR+ ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR+ )
77	7	adantr	|- ( ( ph /\ x e. RR+ ) -> M e. ZZ )
78	10	adantr	|- ( ( ph /\ x e. RR+ ) -> R e. dom ~~> )
79	12	climcau	|- ( ( M e. ZZ /\ R e. dom ~~> ) -> A. w e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w )
80	77 78 79	syl2anc	|- ( ( ph /\ x e. RR+ ) -> A. w e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w )
81		breq2	|- ( w = ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) -> ( ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w <-> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
82	81	rexralbidv	|- ( w = ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) -> ( E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w <-> E. 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 ) ) ) )
83	82	rspcva	|- ( ( ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR+ /\ A. w e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w ) -> E. 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 ) ) )
84	76 80 83	syl2anc	|- ( ( ph /\ x e. RR+ ) -> E. 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 ) ) )
85		rabn0	|- ( { 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 ) ) } =/= (/) <-> E. 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 ) ) )
86	84 85	sylibr	|- ( ( ph /\ x e. RR+ ) -> { 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 ) ) } =/= (/) )
87		infssuzcl	|- ( ( { 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 ) ) } C_ ( ZZ>= ` M ) /\ { 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 ) ) } =/= (/) ) -> 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 , < ) e. { 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 ) ) } )
88	19 86 87	sylancr	|- ( ( ph /\ x e. 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 , < ) e. { 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 ) ) } )
89	11 88	eqeltrid	|- ( ( ph /\ x e. RR+ ) -> K e. { 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 ) ) } )
90	19 89	sseldi	|- ( ( ph /\ x e. RR+ ) -> K e. ( ZZ>= ` M ) )
91		2fveq3	|- ( j = i -> ( F ` ( R ` j ) ) = ( F ` ( R ` i ) ) )
92		uzss	|- ( K e. ( ZZ>= ` M ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
93	90 92	syl	|- ( ( ph /\ x e. RR+ ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
94	93	sselda	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> i e. ( ZZ>= ` M ) )
95	14	ad2antrr	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> F : ( A (,) B ) --> RR )
96	8	ad2antrr	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
97	96 94	ffvelrnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. ( A (,) B ) )
98	95 97	ffvelrnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` i ) ) e. RR )
99	9 91 94 98	fvmptd3	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( S ` i ) = ( F ` ( R ` i ) ) )
100		2fveq3	|- ( j = K -> ( F ` ( R ` j ) ) = ( F ` ( R ` K ) ) )
101	90	adantr	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> K e. ( ZZ>= ` M ) )
102	96 101	ffvelrnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` K ) e. ( A (,) B ) )
103	95 102	ffvelrnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` K ) ) e. RR )
104	9 100 101 103	fvmptd3	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( S ` K ) = ( F ` ( R ` K ) ) )
105	99 104	oveq12d	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( S ` i ) - ( S ` K ) ) = ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) )
106	105	fveq2d	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( S ` i ) - ( S ` K ) ) ) = ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) )
107	98	recnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` i ) ) e. CC )
108	103	recnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` K ) ) e. CC )
109	107 108	subcld	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) e. CC )
110	109	abscld	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) e. RR )
111	110	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) e. RR )
112	44	ad2antrr	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
113	112	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
114	8	adantr	|- ( ( ph /\ x e. RR+ ) -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
115	114 90	ffvelrnd	|- ( ( ph /\ x e. RR+ ) -> ( R ` K ) e. ( A (,) B ) )
116	29 115	sseldi	|- ( ( ph /\ x e. RR+ ) -> ( R ` K ) e. RR )
117	116	ad2antrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) e. RR )
118	29 97	sseldi	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. RR )
119	118	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. RR )
120	117 119	resubcld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) e. RR )
121	113 120	remulcld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) e. RR )
122	20	ad3antlr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> x e. RR )
123	107	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( F ` ( R ` i ) ) e. CC )
124	108	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( F ` ( R ` K ) ) e. CC )
125	123 124	abssubd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) = ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) )
126	1	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> A e. RR )
127	2	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> B e. RR )
128	95	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> F : ( A (,) B ) --> RR )
129	5	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> dom ( RR _D F ) = ( A (,) B ) )
130	61	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
131	97	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. ( A (,) B ) )
132	118	rexrd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. RR* )
133	132	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. RR* )
134	2	rexrd	|- ( ph -> B e. RR* )
135	134	ad2antrr	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> B e. RR* )
136	135	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> B e. RR* )
137		simpr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) < ( R ` K ) )
138	1	rexrd	|- ( ph -> A e. RR* )
139	138	adantr	|- ( ( ph /\ x e. RR+ ) -> A e. RR* )
140	134	adantr	|- ( ( ph /\ x e. RR+ ) -> B e. RR* )
141		iooltub	|- ( ( A e. RR* /\ B e. RR* /\ ( R ` K ) e. ( A (,) B ) ) -> ( R ` K ) < B )
142	139 140 115 141	syl3anc	|- ( ( ph /\ x e. RR+ ) -> ( R ` K ) < B )
143	142	ad2antrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) < B )
144	133 136 117 137 143	eliood	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) e. ( ( R ` i ) (,) B ) )
145	126 127 128 129 113 130 131 144	dvbdfbdioolem1	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) /\ ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( B - A ) ) ) )
146	145	simpld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) )
147	125 146	eqbrtrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) )
148	113 46	syl	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
149	148 120	remulcld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) e. RR )
150	119 117	posdifd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` i ) < ( R ` K ) <-> 0 < ( ( R ` K ) - ( R ` i ) ) ) )
151	137 150	mpbid	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> 0 < ( ( R ` K ) - ( R ` i ) ) )
152	120 151	elrpd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) e. RR+ )
153	113	ltp1d	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
154	113 148 152 153	ltmul1dd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) < ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) )
155	29 102	sseldi	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` K ) e. RR )
156	118 155	resubcld	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( R ` i ) - ( R ` K ) ) e. RR )
157	156	recnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( R ` i ) - ( R ` K ) ) e. CC )
158	157	abscld	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) e. RR )
159	158	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) e. RR )
160	71	ad2antrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR )
161	120	leabsd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) <_ ( abs ` ( ( R ` K ) - ( R ` i ) ) ) )
162	117	recnd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) e. CC )
163	118	recnd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. CC )
164	163	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. CC )
165	162 164	abssubd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( R ` K ) - ( R ` i ) ) ) = ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
166	161 165	breqtrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) <_ ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
167		fveq2	|- ( k = K -> ( ZZ>= ` k ) = ( ZZ>= ` K ) )
168		fveq2	|- ( k = K -> ( R ` k ) = ( R ` K ) )
169	168	oveq2d	|- ( k = K -> ( ( R ` i ) - ( R ` k ) ) = ( ( R ` i ) - ( R ` K ) ) )
170	169	fveq2d	|- ( k = K -> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) = ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
171	170	breq1d	|- ( k = K -> ( ( abs ` ( ( R ` i ) - ( 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 ) ) ) )
172	167 171	raleqbidv	|- ( k = K -> ( A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( 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 ) ) ) )
173	172	elrab	|- ( K e. { 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 ) ) } <-> ( 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 ) ) ) )
174	89 173	sylib	|- ( ( ph /\ x e. RR+ ) -> ( 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 ) ) ) )
175	174	simprd	|- ( ( ph /\ x e. RR+ ) -> A. i e. ( ZZ>= ` K ) ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
176	175	r19.21bi	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
177	176	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
178	120 159 160 166 177	lelttrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
179	51 68	elrpd	|- ( ph -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR+ )
180	179	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR+ )
181	120 122 180	ltmuldiv2d	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) < x <-> ( ( R ` K ) - ( R ` i ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
182	178 181	mpbird	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) < x )
183	121 149 122 154 182	lttrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) < x )
184	111 121 122 147 183	lelttrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
185		fveq2	|- ( ( R ` i ) = ( R ` K ) -> ( F ` ( R ` i ) ) = ( F ` ( R ` K ) ) )
186	185	oveq1d	|- ( ( R ` i ) = ( R ` K ) -> ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) = ( ( F ` ( R ` K ) ) - ( F ` ( R ` K ) ) ) )
187	108	subidd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( F ` ( R ` K ) ) - ( F ` ( R ` K ) ) ) = 0 )
188	186 187	sylan9eqr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) = 0 )
189	188	abs00bd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) = 0 )
190	72	ad3antlr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> 0 < x )
191	189 190	eqbrtrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
192	191	adantlr	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
193		simpll	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) )
194	155	ad2antrr	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` K ) e. RR )
195	118	ad2antrr	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` i ) e. RR )
196		id	|- ( ( R ` K ) = ( R ` i ) -> ( R ` K ) = ( R ` i ) )
197	196	eqcomd	|- ( ( R ` K ) = ( R ` i ) -> ( R ` i ) = ( R ` K ) )
198	197	necon3bi	|- ( -. ( R ` i ) = ( R ` K ) -> ( R ` K ) =/= ( R ` i ) )
199	198	adantl	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` K ) =/= ( R ` i ) )
200		simplr	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> -. ( R ` i ) < ( R ` K ) )
201	194 195 199 200	lttri5d	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` K ) < ( R ` i ) )
202	110	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) e. RR )
203	112 156	remulcld	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) e. RR )
204	203	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) e. RR )
205	20	ad3antlr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> x e. RR )
206	1	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> A e. RR )
207	2	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> B e. RR )
208	95	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> F : ( A (,) B ) --> RR )
209	5	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> dom ( RR _D F ) = ( A (,) B ) )
210	44	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
211	61	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
212	102	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) e. ( A (,) B ) )
213	116	rexrd	|- ( ( ph /\ x e. RR+ ) -> ( R ` K ) e. RR* )
214	213	ad2antrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) e. RR* )
215	207	rexrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> B e. RR* )
216	118	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` i ) e. RR )
217		simpr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) < ( R ` i ) )
218	138	ad2antrr	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> A e. RR* )
219		iooltub	|- ( ( A e. RR* /\ B e. RR* /\ ( R ` i ) e. ( A (,) B ) ) -> ( R ` i ) < B )
220	218 135 97 219	syl3anc	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) < B )
221	220	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` i ) < B )
222	214 215 216 217 221	eliood	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` i ) e. ( ( R ` K ) (,) B ) )
223	206 207 208 209 210 211 212 222	dvbdfbdioolem1	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) /\ ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( B - A ) ) ) )
224	223	simpld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) )
225		1red	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> 1 e. RR )
226	210 225	readdcld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
227	155	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) e. RR )
228	216 227	resubcld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) e. RR )
229	226 228	remulcld	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) e. RR )
230	210 46	syl	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
231	227 216	posdifd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` K ) < ( R ` i ) <-> 0 < ( ( R ` i ) - ( R ` K ) ) ) )
232	217 231	mpbid	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> 0 < ( ( R ` i ) - ( R ` K ) ) )
233	228 232	elrpd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) e. RR+ )
234	210	ltp1d	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
235	210 230 233 234	ltmul1dd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) < ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) )
236	158	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) e. RR )
237	71	ad2antrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR )
238	228	leabsd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) <_ ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
239	176	adantr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
240	228 236 237 238 239	lelttrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
241	179	ad3antrrr	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR+ )
242	228 205 241	ltmuldiv2d	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) < x <-> ( ( R ` i ) - ( R ` K ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
243	240 242	mpbird	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) < x )
244	204 229 205 235 243	lttrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) < x )
245	202 204 205 224 244	lelttrd	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
246	193 201 245	syl2anc	|- ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
247	192 246	pm2.61dan	|- ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
248	184 247	pm2.61dan	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
249	106 248	eqbrtrd	|- ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x )
250	249	ralrimiva	|- ( ( ph /\ x e. RR+ ) -> A. i e. ( ZZ>= ` K ) ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x )
251		fveq2	|- ( k = K -> ( S ` k ) = ( S ` K ) )
252	251	oveq2d	|- ( k = K -> ( ( S ` i ) - ( S ` k ) ) = ( ( S ` i ) - ( S ` K ) ) )
253	252	fveq2d	|- ( k = K -> ( abs ` ( ( S ` i ) - ( S ` k ) ) ) = ( abs ` ( ( S ` i ) - ( S ` K ) ) ) )
254	253	breq1d	|- ( k = K -> ( ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x <-> ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x ) )
255	167 254	raleqbidv	|- ( k = K -> ( A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x <-> A. i e. ( ZZ>= ` K ) ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x ) )
256	255	rspcev	|- ( ( K e. ( ZZ>= ` M ) /\ A. i e. ( ZZ>= ` K ) ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x ) -> E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x )
257	90 250 256	syl2anc	|- ( ( ph /\ x e. RR+ ) -> E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x )
258	257	ralrimiva	|- ( ph -> A. x e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x )
259	12 18 258	caurcvg	|- ( ph -> S ~~> ( limsup ` S ) )