Metamath Proof Explorer


Theorem ulmcn

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

Ref Expression
Hypotheses ulmcn.z Z = M
ulmcn.m φ M
ulmcn.f φ F : Z S cn
ulmcn.u φ F u S G
Assertion ulmcn φ G : S cn

Proof

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