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

Theorem ftc2 19386
 Description: The Fundamental Theorem of Calculus, part two. If is a function continuous on and continuously differentiable on , then the integral of the derivative of is equal to . (Contributed by Mario Carneiro, 2-Sep-2014.)
Hypotheses
Ref Expression
ftc2.a
ftc2.b
ftc2.le
ftc2.c
ftc2.i
ftc2.f
Assertion
Ref Expression
ftc2
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem ftc2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ftc2.a . . . . . . 7
21rexrd 8876 . . . . . 6
3 ftc2.b . . . . . . 7
43rexrd 8876 . . . . . 6
5 ftc2.le . . . . . 6
6 ubicc2 10748 . . . . . 6
72, 4, 5, 6syl3anc 1182 . . . . 5
8 fvex 5499 . . . . . 6
98fvconst2 5690 . . . . 5
107, 9syl 15 . . . 4
11 eqid 2283 . . . . . . . 8 fld fld
1211subcn 18365 . . . . . . . . 9 fld fld fld
1312a1i 10 . . . . . . . 8 fld fld fld
14 eqid 2283 . . . . . . . . 9
15 ssid 3197 . . . . . . . . . 10
1615a1i 10 . . . . . . . . 9
17 ioossre 10707 . . . . . . . . . 10
1817a1i 10 . . . . . . . . 9
19 ftc2.i . . . . . . . . 9
20 ftc2.c . . . . . . . . . 10
21 cncff 18392 . . . . . . . . . 10
2220, 21syl 15 . . . . . . . . 9
2314, 1, 3, 5, 16, 18, 19, 22ftc1a 19379 . . . . . . . 8
24 ftc2.f . . . . . . . . . . 11
25 cncff 18392 . . . . . . . . . . 11
2624, 25syl 15 . . . . . . . . . 10
2726feqmptd 5536 . . . . . . . . 9
2827, 24eqeltrrd 2358 . . . . . . . 8
2911, 13, 23, 28cncfmpt2f 18413 . . . . . . 7
30 ax-resscn 8789 . . . . . . . . . . 11
3130a1i 10 . . . . . . . . . 10
32 iccssre 10726 . . . . . . . . . . 11
331, 3, 32syl2anc 642 . . . . . . . . . 10
34 fvex 5499 . . . . . . . . . . . . 13
3534a1i 10 . . . . . . . . . . . 12
363adantr 451 . . . . . . . . . . . . . . 15
3736rexrd 8876 . . . . . . . . . . . . . 14
38 elicc2 10710 . . . . . . . . . . . . . . . . 17
391, 3, 38syl2anc 642 . . . . . . . . . . . . . . . 16
4039biimpa 470 . . . . . . . . . . . . . . 15
4140simp3d 969 . . . . . . . . . . . . . 14
42 iooss2 10687 . . . . . . . . . . . . . 14
4337, 41, 42syl2anc 642 . . . . . . . . . . . . 13
44 ioombl 18917 . . . . . . . . . . . . . 14
4544a1i 10 . . . . . . . . . . . . 13
4634a1i 10 . . . . . . . . . . . . 13
4722feqmptd 5536 . . . . . . . . . . . . . . 15
4847, 19eqeltrrd 2358 . . . . . . . . . . . . . 14
4948adantr 451 . . . . . . . . . . . . 13
5043, 45, 46, 49iblss 19154 . . . . . . . . . . . 12
5135, 50itgcl 19133 . . . . . . . . . . 11
52 ffvelrn 5624 . . . . . . . . . . . 12
5326, 52sylan 457 . . . . . . . . . . 11
5451, 53subcld 9152 . . . . . . . . . 10
5511tgioo2 18304 . . . . . . . . . 10 fldt
56 iccntr 18321 . . . . . . . . . . 11
571, 3, 56syl2anc 642 . . . . . . . . . 10
5831, 33, 54, 55, 11, 57dvmptntr 19315 . . . . . . . . 9
59 reex 8823 . . . . . . . . . . . 12
6059prid1 3734 . . . . . . . . . . 11
6160a1i 10 . . . . . . . . . 10
62 ioossicc 10730 . . . . . . . . . . . 12
6362sseli 3176 . . . . . . . . . . 11
6463, 51sylan2 460 . . . . . . . . . 10
65 ffvelrn 5624 . . . . . . . . . . 11
6622, 65sylan 457 . . . . . . . . . 10
6714, 1, 3, 5, 20, 19ftc1cn 19385 . . . . . . . . . . 11
6831, 33, 51, 55, 11, 57dvmptntr 19315 . . . . . . . . . . 11
6922feqmptd 5536 . . . . . . . . . . 11
7067, 68, 693eqtr3d 2323 . . . . . . . . . 10
7163, 53sylan2 460 . . . . . . . . . 10
7231, 33, 53, 55, 11, 57dvmptntr 19315 . . . . . . . . . . 11
7327oveq2d 5835 . . . . . . . . . . . 12
7473, 69eqtr3d 2317 . . . . . . . . . . 11
7572, 74eqtr3d 2317 . . . . . . . . . 10
7661, 64, 66, 70, 71, 66, 75dvmptsub 19311 . . . . . . . . 9
7766subidd 9140 . . . . . . . . . 10
7877mpteq2dva 4106 . . . . . . . . 9
7958, 76, 783eqtrd 2319 . . . . . . . 8
80 fconstmpt 4730 . . . . . . . 8
8179, 80syl6eqr 2333 . . . . . . 7
821, 3, 29, 81dveq0 19342 . . . . . 6
8382fveq1d 5487 . . . . 5
84 oveq2 5827 . . . . . . . . 9
85 itgeq1 19122 . . . . . . . . 9
8684, 85syl 15 . . . . . . . 8
87 fveq2 5485 . . . . . . . 8
8886, 87oveq12d 5837 . . . . . . 7
89 eqid 2283 . . . . . . 7
90 ovex 5844 . . . . . . 7
9188, 89, 90fvmpt 5563 . . . . . 6
927, 91syl 15 . . . . 5
9383, 92eqtr3d 2317 . . . 4
94 lbicc2 10747 . . . . . 6
952, 4, 5, 94syl3anc 1182 . . . . 5
96 oveq2 5827 . . . . . . . . . . 11
97 iooid 10679 . . . . . . . . . . 11
9896, 97syl6eq 2331 . . . . . . . . . 10
99 itgeq1 19122 . . . . . . . . . 10
10098, 99syl 15 . . . . . . . . 9
101 itg0 19129 . . . . . . . . 9
102100, 101syl6eq 2331 . . . . . . . 8
103 fveq2 5485 . . . . . . . 8
104102, 103oveq12d 5837 . . . . . . 7
105 df-neg 9035 . . . . . . 7
106104, 105syl6eqr 2333 . . . . . 6
107 negex 9045 . . . . . 6
108106, 89, 107fvmpt 5563 . . . . 5
10995, 108syl 15 . . . 4
11010, 93, 1093eqtr3d 2323 . . 3
111110oveq2d 5835 . 2
112 ffvelrn 5624 . . . 4
11326, 7, 112syl2anc 642 . . 3
11434a1i 10 . . . 4
115114, 48itgcl 19133 . . 3
116113, 115pncan3d 9155 . 2
117 ffvelrn 5624 . . . 4
11826, 95, 117syl2anc 642 . . 3
119113, 118negsubd 9158 . 2
120111, 116, 1193eqtr3d 2323 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1623   wcel 1684  cvv 2788   wss 3152  c0 3455  csn 3640  cpr 3641   class class class wbr 4023   cmpt 4077   cxp 4685   cdm 4687   crn 4688  wf 5216  cfv 5220  (class class class)co 5819  cc 8730  cr 8731  cc0 8732   caddc 8735  cxr 8861   cle 8863   cmin 9032  cneg 9033  cioo 10651  cicc 10654  ctopn 13321  ctg 13337  ℂfldccnfld 16372  cnt 16749   ccn 16949   ctx 17250  ccncf 18375  cvol 18818  cibl 18967  citg 18968   cdv 19208 This theorem is referenced by:  ftc2ditglem  19387  itgparts  19389  itgsubstlem  19390  areacirc  24341  lhe4.4ex1a  26957  itgsin0pilem1  27155 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4186  ax-pr 4212  ax-un 4510  ax-inf2 7337  ax-cc 8056  ax-cnex 8788  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-mulcom 8796  ax-addass 8797  ax-mulass 8798  ax-distr 8799  ax-i2m1 8800  ax-1ne0 8801  ax-1rid 8802  ax-rnegex 8803  ax-rrecex 8804  ax-cnre 8805  ax-pre-lttri 8806  ax-pre-lttrn 8807  ax-pre-ltadd 8808  ax-pre-mulgt0 8809  ax-pre-sup 8810  ax-addf 8811  ax-mulf 8812 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-disj 3994  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4303  df-id 4307  df-po 4312  df-so 4313  df-fr 4350  df-se 4351  df-we 4352  df-ord 4393  df-on 4394  df-lim 4395  df-suc 4396  df-om 4655  df-xp 4693  df-rel 4694  df-cnv 4695  df-co 4696  df-dm 4697  df-rn 4698  df-res 4699  df-ima 4700  df-fun 5222  df-fn 5223  df-f 5224  df-f1 5225  df-fo 5226  df-f1o 5227  df-fv 5228  df-isom 5229  df-ov 5822  df-oprab 5823  df-mpt2 5824  df-of 6039  df-ofr 6040  df-1st 6083  df-2nd 6084  df-iota 6252  df-riota 6299  df-recs 6383  df-rdg 6418  df-1o 6474  df-2o 6475  df-oadd 6478  df-omul 6479  df-er 6655  df-map 6769  df-pm 6770  df-ixp 6813  df-en 6859  df-dom 6860  df-sdom 6861  df-fin 6862  df-fi 7160  df-sup 7189  df-oi 7220  df-card 7567  df-acn 7570  df-cda 7789  df-pnf 8864  df-mnf 8865  df-xr 8866  df-ltxr 8867  df-le 8868  df-sub 9034  df-neg 9035  df-div 9419  df-nn 9742  df-2 9799  df-3 9800  df-4 9801  df-5 9802  df-6 9803  df-7 9804  df-8 9805  df-9 9806  df-10 9807  df-n0 9961  df-z 10020  df-dec 10120  df-uz 10226  df-q 10312  df-rp 10350  df-xneg 10447  df-xadd 10448  df-xmul 10449  df-ioo 10655  df-ioc 10656  df-ico 10657  df-icc 10658  df-fz 10778  df-fzo 10866  df-fl 10920  df-mod 10969  df-seq 11042  df-exp 11100  df-hash 11333  df-cj 11579  df-re 11580  df-im 11581  df-sqr 11715  df-abs 11716  df-clim 11957  df-rlim 11958  df-sum 12154  df-struct 13145  df-ndx 13146  df-slot 13147  df-base 13148  df-sets 13149  df-ress 13150  df-plusg 13216  df-mulr 13217  df-starv 13218  df-sca 13219  df-vsca 13220  df-tset 13222  df-ple 13223  df-ds 13225  df-hom 13227  df-cco 13228  df-rest 13322  df-topn 13323  df-topgen 13339  df-pt 13340  df-prds 13343  df-xrs 13398  df-0g 13399  df-gsum 13400  df-qtop 13405  df-imas 13406  df-xps 13408  df-mre 13483  df-mrc 13484  df-acs 13486  df-mnd 14362  df-submnd 14411  df-mulg 14487  df-cntz 14788  df-cmn 15086  df-xmet 16368  df-met 16369  df-bl 16370  df-mopn 16371  df-cnfld 16373  df-top 16631  df-bases 16633  df-topon 16634  df-topsp 16635  df-cld 16751  df-ntr 16752  df-cls 16753  df-nei 16830  df-lp 16863  df-perf 16864  df-cn 16952  df-cnp 16953  df-haus 17038  df-cmp 17109  df-tx 17252  df-hmeo 17441  df-fbas 17515  df-fg 17516  df-fil 17536  df-fm 17628  df-flim 17629  df-flf 17630  df-xms 17880  df-ms 17881  df-tms 17882  df-cncf 18377  df-ovol 18819  df-vol 18820  df-mbf 18970  df-itg1 18971  df-itg2 18972  df-ibl 18973  df-itg 18974  df-0p 19020  df-limc 19211  df-dv 19212
 Copyright terms: Public domain W3C validator