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

Theorem ftc1cn 22982
 Description: Strengthen the assumptions of ftc1 22981 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 22849 . . . . 5
21a1i 11 . . . 4
3 ffun 5745 . . . 4
42, 3syl 17 . . 3
5 ax-resscn 9597 . . . . . . 7
65a1i 11 . . . . . 6
7 ftc1cn.g . . . . . . 7
8 ftc1cn.a . . . . . . 7
9 ftc1cn.b . . . . . . 7
10 ftc1cn.le . . . . . . 7
11 ssid 3483 . . . . . . . 8
1211a1i 11 . . . . . . 7
13 ioossre 11697 . . . . . . . 8
1413a1i 11 . . . . . . 7
15 ftc1cn.i . . . . . . 7
16 ftc1cn.f . . . . . . . 8
17 cncff 21912 . . . . . . . 8
1816, 17syl 17 . . . . . . 7
197, 8, 9, 10, 12, 14, 15, 18ftc1lem2 22975 . . . . . 6
20 iccssre 11717 . . . . . . 7
218, 9, 20syl2anc 665 . . . . . 6
22 eqid 2422 . . . . . . 7 fld fld
2322tgioo2 21808 . . . . . 6 fldt
246, 19, 21, 23, 22dvbssntr 22842 . . . . 5
25 iccntr 21826 . . . . . 6
268, 9, 25syl2anc 665 . . . . 5
2724, 26sseqtrd 3500 . . . 4
288adantr 466 . . . . . . . 8
299adantr 466 . . . . . . . 8
3010adantr 466 . . . . . . . 8
3111a1i 11 . . . . . . . 8
3213a1i 11 . . . . . . . 8
3315adantr 466 . . . . . . . 8
34 simpr 462 . . . . . . . 8
3513, 5sstri 3473 . . . . . . . . . . . 12
36 ssid 3483 . . . . . . . . . . . 12
37 eqid 2422 . . . . . . . . . . . . 13 fldt fldt
3822cnfldtop 21791 . . . . . . . . . . . . . . 15 fld
3922cnfldtopon 21790 . . . . . . . . . . . . . . . . 17 fld TopOn
4039toponunii 19934 . . . . . . . . . . . . . . . 16 fld
4140restid 15320 . . . . . . . . . . . . . . 15 fld fldt fld
4238, 41ax-mp 5 . . . . . . . . . . . . . 14 fldt fld
4342eqcomi 2435 . . . . . . . . . . . . 13 fld fldt
4422, 37, 43cncfcn 21928 . . . . . . . . . . . 12 fldt fld
4535, 36, 44mp2an 676 . . . . . . . . . . 11 fldt fld
4616, 45syl6eleq 2520 . . . . . . . . . 10 fldt fld
4746adantr 466 . . . . . . . . 9 fldt fld
4835a1i 11 . . . . . . . . . . . . 13
49 resttopon 20164 . . . . . . . . . . . . 13 fld TopOn fldt TopOn
5039, 48, 49sylancr 667 . . . . . . . . . . . 12 fldt TopOn
51 toponuni 19929 . . . . . . . . . . . 12 fldt TopOn fldt
5250, 51syl 17 . . . . . . . . . . 11 fldt
5352eleq2d 2492 . . . . . . . . . 10 fldt
5453biimpa 486 . . . . . . . . 9 fldt
55 eqid 2422 . . . . . . . . . 10 fldt fldt
5655cncnpi 20281 . . . . . . . . 9 fldt fld fldt fldt fld
5747, 54, 56syl2anc 665 . . . . . . . 8 fldt fld
587, 28, 29, 30, 31, 32, 33, 34, 57, 23, 37, 22ftc1 22981 . . . . . . 7
59 vex 3084 . . . . . . . 8
60 fvex 5888 . . . . . . . 8
6159, 60breldm 5055 . . . . . . 7
6258, 61syl 17 . . . . . 6
6362ex 435 . . . . 5
6463ssrdv 3470 . . . 4
6527, 64eqssd 3481 . . 3
66 df-fn 5601 . . 3
674, 65, 66sylanbrc 668 . 2
68 ffn 5743 . . 3
6918, 68syl 17 . 2