ulmcn

Description: A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015)

	Ref	Expression
Hypotheses	ulmcn.z	\|- Z = ( ZZ>= ` M )
	ulmcn.m	\|- ( ph -> M e. ZZ )
	ulmcn.f	\|- ( ph -> F : Z --> ( S -cn-> CC ) )
	ulmcn.u	\|- ( ph -> F ( ~~>u ` S ) G )
Assertion	ulmcn	\|- ( ph -> G e. ( S -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		ulmcn.z	\|- Z = ( ZZ>= ` M )
2		ulmcn.m	\|- ( ph -> M e. ZZ )
3		ulmcn.f	\|- ( ph -> F : Z --> ( S -cn-> CC ) )
4		ulmcn.u	\|- ( ph -> F ( ~~>u ` S ) G )
5		ulmcl	\|- ( F ( ~~>u ` S ) G -> G : S --> CC )
6	4 5	syl	\|- ( ph -> G : S --> CC )
7	2	adantr	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> M e. ZZ )
8		cncff	\|- ( x e. ( S -cn-> CC ) -> x : S --> CC )
9		cnex	\|- CC e. _V
10		cncfrss	\|- ( x e. ( S -cn-> CC ) -> S C_ CC )
11		ssexg	\|- ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
12	10 9 11	sylancl	\|- ( x e. ( S -cn-> CC ) -> S e. _V )
13		elmapg	\|- ( ( CC e. _V /\ S e. _V ) -> ( x e. ( CC ^m S ) <-> x : S --> CC ) )
14	9 12 13	sylancr	\|- ( x e. ( S -cn-> CC ) -> ( x e. ( CC ^m S ) <-> x : S --> CC ) )
15	8 14	mpbird	\|- ( x e. ( S -cn-> CC ) -> x e. ( CC ^m S ) )
16	15	ssriv	\|- ( S -cn-> CC ) C_ ( CC ^m S )
17		fss	\|- ( ( F : Z --> ( S -cn-> CC ) /\ ( S -cn-> CC ) C_ ( CC ^m S ) ) -> F : Z --> ( CC ^m S ) )
18	3 16 17	sylancl	\|- ( ph -> F : Z --> ( CC ^m S ) )
19	18	adantr	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> F : Z --> ( CC ^m S ) )
20		eqidd	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ ( k e. Z /\ w e. S ) ) -> ( ( F ` k ) ` w ) = ( ( F ` k ) ` w ) )
21		eqidd	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ w e. S ) -> ( G ` w ) = ( G ` w ) )
22	4	adantr	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> F ( ~~>u ` S ) G )
23		rphalfcl	\|- ( y e. RR+ -> ( y / 2 ) e. RR+ )
24	23	ad2antll	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> ( y / 2 ) e. RR+ )
25	24	rphalfcld	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> ( ( y / 2 ) / 2 ) e. RR+ )
26	1 7 19 20 21 22 25	ulmi	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) )
27	1	r19.2uz	\|- ( E. j e. Z A. k e. ( ZZ>= ` j ) A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> E. k e. Z A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) )
28		simplrl	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> x e. S )
29		fveq2	\|- ( w = x -> ( ( F ` k ) ` w ) = ( ( F ` k ) ` x ) )
30		fveq2	\|- ( w = x -> ( G ` w ) = ( G ` x ) )
31	29 30	oveq12d	\|- ( w = x -> ( ( ( F ` k ) ` w ) - ( G ` w ) ) = ( ( ( F ` k ) ` x ) - ( G ` x ) ) )
32	31	fveq2d	\|- ( w = x -> ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) = ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) )
33	32	breq1d	\|- ( w = x -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) <-> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) )
34	33	rspcv	\|- ( x e. S -> ( A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) )
35	28 34	syl	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> ( A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) )
36	3	adantr	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> F : Z --> ( S -cn-> CC ) )
37	36	ffvelcdmda	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> ( F ` k ) e. ( S -cn-> CC ) )
38	24	adantr	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> ( y / 2 ) e. RR+ )
39		cncfi	\|- ( ( ( F ` k ) e. ( S -cn-> CC ) /\ x e. S /\ ( y / 2 ) e. RR+ ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) )
40	37 28 38 39	syl3anc	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) )
41	40	ad2antrr	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) )
42		r19.26	\|- ( A. w e. S ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) ) <-> ( A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) /\ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) ) )
43	19	ad2antrr	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> F : Z --> ( CC ^m S ) )
44		simplr	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> k e. Z )
45	43 44	ffvelcdmd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( F ` k ) e. ( CC ^m S ) )
46		elmapi	\|- ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
47	45 46	syl	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( F ` k ) : S --> CC )
48	28	adantr	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> x e. S )
49	47 48	ffvelcdmd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( F ` k ) ` x ) e. CC )
50	6	ad3antrrr	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> G : S --> CC )
51	50 48	ffvelcdmd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( G ` x ) e. CC )
52	49 51	subcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( F ` k ) ` x ) - ( G ` x ) ) e. CC )
53	52	abscld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) e. RR )
54		ffvelcdm	\|- ( ( ( F ` k ) : S --> CC /\ w e. S ) -> ( ( F ` k ) ` w ) e. CC )
55	47 54	sylancom	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( F ` k ) ` w ) e. CC )
56		ffvelcdm	\|- ( ( G : S --> CC /\ w e. S ) -> ( G ` w ) e. CC )
57	50 56	sylancom	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( G ` w ) e. CC )
58	55 57	subcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( F ` k ) ` w ) - ( G ` w ) ) e. CC )
59	58	abscld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) e. RR )
60	38	adantr	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( y / 2 ) e. RR+ )
61	60	rphalfcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( y / 2 ) / 2 ) e. RR+ )
62	61	rpred	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( y / 2 ) / 2 ) e. RR )
63		lt2add	\|- ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) e. RR /\ ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) e. RR ) /\ ( ( ( y / 2 ) / 2 ) e. RR /\ ( ( y / 2 ) / 2 ) e. RR ) ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( ( ( y / 2 ) / 2 ) + ( ( y / 2 ) / 2 ) ) ) )
64	53 59 62 62 63	syl22anc	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( ( ( y / 2 ) / 2 ) + ( ( y / 2 ) / 2 ) ) ) )
65	60	rpred	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( y / 2 ) e. RR )
66	65	recnd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( y / 2 ) e. CC )
67	66	2halvesd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( y / 2 ) / 2 ) + ( ( y / 2 ) / 2 ) ) = ( y / 2 ) )
68	67	breq2d	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( ( ( y / 2 ) / 2 ) + ( ( y / 2 ) / 2 ) ) <-> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( y / 2 ) ) )
69	53 59	readdcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) e. RR )
70	55 49	subcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) e. CC )
71	70	abscld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) e. RR )
72		lt2add	\|- ( ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) e. RR /\ ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) e. RR ) /\ ( ( y / 2 ) e. RR /\ ( y / 2 ) e. RR ) ) -> ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( y / 2 ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < ( ( y / 2 ) + ( y / 2 ) ) ) )
73	69 71 65 65 72	syl22anc	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( y / 2 ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < ( ( y / 2 ) + ( y / 2 ) ) ) )
74		rpre	\|- ( y e. RR+ -> y e. RR )
75	74	ad2antll	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> y e. RR )
76	75	ad2antrr	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> y e. RR )
77	76	recnd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> y e. CC )
78	77	2halvesd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( y / 2 ) + ( y / 2 ) ) = y )
79	78	breq2d	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < ( ( y / 2 ) + ( y / 2 ) ) <-> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < y ) )
80	57 51	subcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( G ` w ) - ( G ` x ) ) e. CC )
81	80	abscld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) e. RR )
82	57 49	subcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( G ` w ) - ( ( F ` k ) ` x ) ) e. CC )
83	82	abscld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) e. RR )
84	53 83	readdcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) ) e. RR )
85	69 71	readdcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) e. RR )
86	57 51 49	abs3difd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) <_ ( ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) ) )
87	83	recnd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) e. CC )
88	53	recnd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) e. CC )
89	87 88	addcomd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) ) = ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) ) )
90	86 89	breqtrd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) <_ ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) ) )
91	59 71	readdcld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) e. RR )
92	57 49 55	abs3difd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) <_ ( ( abs ` ( ( G ` w ) - ( ( F ` k ) ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) )
93	57 55	abssubd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( ( F ` k ) ` w ) ) ) = ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) )
94	93	oveq1d	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( G ` w ) - ( ( F ` k ) ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) = ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) )
95	92 94	breqtrd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) <_ ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) )
96	83 91 53 95	leadd2dd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) ) <_ ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) ) )
97	59	recnd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) e. CC )
98	71	recnd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) e. CC )
99	88 97 98	addassd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) = ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) ) )
100	96 99	breqtrrd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( G ` w ) - ( ( F ` k ) ` x ) ) ) ) <_ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) )
101	81 84 85 90 100	letrd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) <_ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) )
102		lelttr	\|- ( ( ( abs ` ( ( G ` w ) - ( G ` x ) ) ) e. RR /\ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) e. RR /\ y e. RR ) -> ( ( ( abs ` ( ( G ` w ) - ( G ` x ) ) ) <_ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) /\ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < y ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
103	81 85 76 102	syl3anc	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( G ` w ) - ( G ` x ) ) ) <_ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) /\ ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < y ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
104	101 103	mpand	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < y -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
105	79 104	sylbid	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) ) < ( ( y / 2 ) + ( y / 2 ) ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
106	73 105	syld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( y / 2 ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
107	106	expd	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( y / 2 ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
108	68 107	sylbid	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) + ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) ) < ( ( ( y / 2 ) / 2 ) + ( ( y / 2 ) / 2 ) ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
109	64 108	syld	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
110	109	expdimp	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ w e. S ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
111	110	an32s	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) /\ w e. S ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
112	111	imp	\|- ( ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) /\ w e. S ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
113	112	imim2d	\|- ( ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) /\ w e. S ) /\ ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
114	113	expimpd	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) /\ w e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
115	114	ralimdva	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( A. w e. S ( ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) /\ ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) ) -> A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
116	42 115	biimtrrid	\|- ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( ( A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) /\ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) ) -> A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
117	116	expdimp	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) /\ A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
118	117	an32s	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
119	118	reximdv	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> ( E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( F ` k ) ` w ) - ( ( F ` k ) ` x ) ) ) < ( y / 2 ) ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
120	41 119	mpd	\|- ( ( ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) /\ A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) ) /\ ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
121	120	exp31	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> ( A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < ( ( y / 2 ) / 2 ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) ) )
122	35 121	mpdd	\|- ( ( ( ph /\ ( x e. S /\ y e. RR+ ) ) /\ k e. Z ) -> ( A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
123	122	rexlimdva	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> ( E. k e. Z A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
124	27 123	syl5	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. w e. S ( abs ` ( ( ( F ` k ) ` w ) - ( G ` w ) ) ) < ( ( y / 2 ) / 2 ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) )
125	26 124	mpd	\|- ( ( ph /\ ( x e. S /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
126	125	ralrimivva	\|- ( ph -> A. x e. S A. y e. RR+ E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) )
127		uzid	\|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
128	2 127	syl	\|- ( ph -> M e. ( ZZ>= ` M ) )
129	128 1	eleqtrrdi	\|- ( ph -> M e. Z )
130	3 129	ffvelcdmd	\|- ( ph -> ( F ` M ) e. ( S -cn-> CC ) )
131		cncfrss	\|- ( ( F ` M ) e. ( S -cn-> CC ) -> S C_ CC )
132	130 131	syl	\|- ( ph -> S C_ CC )
133		ssid	\|- CC C_ CC
134		elcncf2	\|- ( ( S C_ CC /\ CC C_ CC ) -> ( G e. ( S -cn-> CC ) <-> ( G : S --> CC /\ A. x e. S A. y e. RR+ E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) ) )
135	132 133 134	sylancl	\|- ( ph -> ( G e. ( S -cn-> CC ) <-> ( G : S --> CC /\ A. x e. S A. y e. RR+ E. z e. RR+ A. w e. S ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` x ) ) ) < y ) ) ) )
136	6 126 135	mpbir2and	\|- ( ph -> G e. ( S -cn-> CC ) )

Metamath Proof Explorer

Theorem ulmcn

Proof