Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ulmdv Unicode version

Theorem ulmdv 19796
 Description: If is a sequence of differentiable functions on which converge pointwise to , and the derivatives of converge uniformly to , then is differentiable with derivative . (Contributed by Mario Carneiro, 27-Feb-2015.)
Hypotheses
Ref Expression
ulmdv.z
ulmdv.s
ulmdv.m
ulmdv.f
ulmdv.g
ulmdv.l
ulmdv.u
Assertion
Ref Expression
ulmdv
Distinct variable groups:   ,,   ,   ,   ,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ulmdv
StepHypRef Expression
1 ulmdv.s . . . . 5
2 dvfg 19272 . . . . 5
31, 2syl 15 . . . 4
4 recnprss 19270 . . . . . . . 8
51, 4syl 15 . . . . . . 7
6 ulmdv.g . . . . . . 7
7 ulmdv.m . . . . . . . . . 10
8 uzid 10258 . . . . . . . . . 10
97, 8syl 15 . . . . . . . . 9
10 ulmdv.z . . . . . . . . 9
119, 10syl6eleqr 2387 . . . . . . . 8
12 ulmdv.f . . . . . . . . . . 11
13 ulmdv.l . . . . . . . . . . 11
14 ulmdv.u . . . . . . . . . . 11
1510, 1, 7, 12, 6, 13, 14ulmdvlem2 19794 . . . . . . . . . 10
16 dvbsss 19268 . . . . . . . . . . 11
1716a1i 10 . . . . . . . . . 10
1815, 17eqsstr3d 3226 . . . . . . . . 9
1918ralrimiva 2639 . . . . . . . 8
20 biidd 228 . . . . . . . . 9
2120rspcv 2893 . . . . . . . 8
2211, 19, 21sylc 56 . . . . . . 7
235, 6, 22dvbss 19267 . . . . . 6
2410, 1, 7, 12, 6, 13, 14ulmdvlem3 19795 . . . . . . . . 9
25 vex 2804 . . . . . . . . . 10
26 fvex 5555 . . . . . . . . . 10
2725, 26breldm 4899 . . . . . . . . 9
2824, 27syl 15 . . . . . . . 8
2928ex 423 . . . . . . 7
3029ssrdv 3198 . . . . . 6
3123, 30eqssd 3209 . . . . 5
3231feq2d 5396 . . . 4
333, 32mpbid 201 . . 3
34 ffn 5405 . . 3
3533, 34syl 15 . 2
36 ulmcl 19776 . . . 4
3714, 36syl 15 . . 3
38 ffn 5405 . . 3
3937, 38syl 15 . 2
40 ffun 5407 . . . . 5
413, 40syl 15 . . . 4