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

Theorem ftc1cn 19390
 Description: Strengthen the assumptions of ftc1 19389 to when the function is continuous on the entire interval ; in this case we can calculate exactly. (Contributed by Mario Carneiro, 1-Sep-2014.)
Hypotheses
Ref Expression
ftc1cn.g
ftc1cn.a
ftc1cn.b
ftc1cn.le
ftc1cn.f
ftc1cn.i
Assertion
Ref Expression
ftc1cn
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem ftc1cn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dvf 19257 . . . . 5
21a1i 10 . . . 4
3 ffun 5391 . . . 4
42, 3syl 15 . . 3
5 ax-resscn 8794 . . . . . . 7
65a1i 10 . . . . . 6
7 ftc1cn.g . . . . . . 7
8 ftc1cn.a . . . . . . 7
9 ftc1cn.b . . . . . . 7
10 ftc1cn.le . . . . . . 7
11 ssid 3197 . . . . . . . 8
1211a1i 10 . . . . . . 7
13 ioossre 10712 . . . . . . . 8
1413a1i 10 . . . . . . 7
15 ftc1cn.i . . . . . . 7
16 ftc1cn.f . . . . . . . 8
17 cncff 18397 . . . . . . . 8
1816, 17syl 15 . . . . . . 7
197, 8, 9, 10, 12, 14, 15, 18ftc1lem2 19383 . . . . . 6
20 iccssre 10731 . . . . . . 7
218, 9, 20syl2anc 642 . . . . . 6
22 eqid 2283 . . . . . . 7 fld fld
2322tgioo2 18309 . . . . . 6 fldt
246, 19, 21, 23, 22dvbssntr 19250 . . . . 5
25 iccntr 18326 . . . . . 6
268, 9, 25syl2anc 642 . . . . 5
2724, 26sseqtrd 3214 . . . 4
288adantr 451 . . . . . . . 8
299adantr 451 . . . . . . . 8
3010adantr 451 . . . . . . . 8
3111a1i 10 . . . . . . . 8
3213a1i 10 . . . . . . . 8
3315adantr 451 . . . . . . . 8
34 simpr 447 . . . . . . . 8
3513, 5sstri 3188 . . . . . . . . . . . 12
36 ssid 3197 . . . . . . . . . . . 12
37 eqid 2283 . . . . . . . . . . . . 13 fldt fldt
3822cnfldtop 18293 . . . . . . . . . . . . . . 15 fld
3922cnfldtopon 18292 . . . . . . . . . . . . . . . . 17 fld TopOn
4039toponunii 16670 . . . . . . . . . . . . . . . 16 fld
4140restid 13338 . . . . . . . . . . . . . . 15 fld fldt fld
4238, 41ax-mp 8 . . . . . . . . . . . . . 14 fldt fld
4342eqcomi 2287 . . . . . . . . . . . . 13 fld fldt
4422, 37, 43cncfcn 18413 . . . . . . . . . . . 12 fldt fld
4535, 36, 44mp2an 653 . . . . . . . . . . 11 fldt fld
4616, 45syl6eleq 2373 . . . . . . . . . 10 fldt fld
4746adantr 451 . . . . . . . . 9 fldt fld
4835a1i 10 . . . . . . . . . . . . 13
49 resttopon 16892 . . . . . . . . . . . . 13 fld TopOn fldt TopOn
5039, 48, 49sylancr 644 . . . . . . . . . . . 12 fldt TopOn
51 toponuni 16665 . . . . . . . . . . . 12 fldt TopOn fldt
5250, 51syl 15 . . . . . . . . . . 11 fldt
5352eleq2d 2350 . . . . . . . . . 10 fldt
5453biimpa 470 . . . . . . . . 9 fldt
55 eqid 2283 . . . . . . . . . 10 fldt fldt
5655cncnpi 17007 . . . . . . . . 9 fldt fld fldt fldt fld
5747, 54, 56syl2anc 642 . . . . . . . 8 fldt fld
587, 28, 29, 30, 31, 32, 33, 34, 57, 23, 37, 22ftc1 19389 . . . . . . 7
59 vex 2791 . . . . . . . 8
60 fvex 5539 . . . . . . . 8
6159, 60breldm 4883 . . . . . . 7
6258, 61syl 15 . . . . . 6
6362ex 423 . . . . 5
6463ssrdv 3185 . . . 4
6527, 64eqssd 3196 . . 3
66 df-fn 5258 . . 3
674, 65, 66sylanbrc 645 . 2
68 ffn 5389 . . 3
6918, 68syl 15 . 2