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

Theorem ulmdv 20311
 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 19785 . . . . 5
31, 2syl 16 . . . 4
4 recnprss 19783 . . . . . . . 8
51, 4syl 16 . . . . . . 7
6 ulmdv.g . . . . . . 7
7 ulmdv.m . . . . . . . . . 10
8 uzid 10492 . . . . . . . . . 10
97, 8syl 16 . . . . . . . . 9
10 ulmdv.z . . . . . . . . 9
119, 10syl6eleqr 2526 . . . . . . . 8
12 ulmdv.f . . . . . . . . . . 11
13 ulmdv.l . . . . . . . . . . 11
14 ulmdv.u . . . . . . . . . . 11
1510, 1, 7, 12, 6, 13, 14ulmdvlem2 20309 . . . . . . . . . 10
16 dvbsss 19781 . . . . . . . . . 10
1715, 16syl6eqssr 3391 . . . . . . . . 9
1817ralrimiva 2781 . . . . . . . 8
19 biidd 229 . . . . . . . . 9
2019rspcv 3040 . . . . . . . 8
2111, 18, 20sylc 58 . . . . . . 7
225, 6, 21dvbss 19780 . . . . . 6
2310, 1, 7, 12, 6, 13, 14ulmdvlem3 20310 . . . . . . . . 9
24 vex 2951 . . . . . . . . . 10
25 fvex 5734 . . . . . . . . . 10
2624, 25breldm 5066 . . . . . . . . 9
2723, 26syl 16 . . . . . . . 8
2827ex 424 . . . . . . 7
2928ssrdv 3346 . . . . . 6
3022, 29eqssd 3357 . . . . 5
3130feq2d 5573 . . . 4
323, 31mpbid 202 . . 3
33 ffn 5583 . . 3
3432, 33syl 16 . 2
35 ulmcl 20289 . . . 4
3614, 35syl 16 . . 3
37 ffn 5583 . . 3
3836, 37syl 16 . 2
39 ffun 5585 . . . . 5
403, 39syl 16 . . . 4