Step | Hyp | Ref
| Expression |
1 | | ftc1lem1.y |
. . . . . 6
β’ (π β π β (π΄[,]π΅)) |
2 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = π β (π΄(,)π₯) = (π΄(,)π)) |
3 | | itgeq1 25153 |
. . . . . . . 8
β’ ((π΄(,)π₯) = (π΄(,)π) β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
4 | 2, 3 | syl 17 |
. . . . . . 7
β’ (π₯ = π β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
5 | | ftc1.g |
. . . . . . 7
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) |
6 | | itgex 25151 |
. . . . . . 7
β’
β«(π΄(,)π)(πΉβπ‘) dπ‘ β V |
7 | 4, 5, 6 | fvmpt 6953 |
. . . . . 6
β’ (π β (π΄[,]π΅) β (πΊβπ) = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
8 | 1, 7 | syl 17 |
. . . . 5
β’ (π β (πΊβπ) = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π β€ π) β (πΊβπ) = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
10 | | ftc1.a |
. . . . . 6
β’ (π β π΄ β β) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π β€ π) β π΄ β β) |
12 | | ftc1.b |
. . . . . . . 8
β’ (π β π΅ β β) |
13 | | iccssre 13353 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
14 | 10, 12, 13 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄[,]π΅) β β) |
15 | 14, 1 | sseldd 3950 |
. . . . . 6
β’ (π β π β β) |
16 | 15 | adantr 482 |
. . . . 5
β’ ((π β§ π β€ π) β π β β) |
17 | | ftc1lem1.x |
. . . . . . . 8
β’ (π β π β (π΄[,]π΅)) |
18 | 14, 17 | sseldd 3950 |
. . . . . . 7
β’ (π β π β β) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π β€ π) β π β β) |
20 | | elicc2 13336 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β (π β (π΄[,]π΅) β (π β β β§ π΄ β€ π β§ π β€ π΅))) |
21 | 10, 12, 20 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π β (π΄[,]π΅) β (π β β β§ π΄ β€ π β§ π β€ π΅))) |
22 | 17, 21 | mpbid 231 |
. . . . . . . 8
β’ (π β (π β β β§ π΄ β€ π β§ π β€ π΅)) |
23 | 22 | simp2d 1144 |
. . . . . . 7
β’ (π β π΄ β€ π) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((π β§ π β€ π) β π΄ β€ π) |
25 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β€ π) β π β€ π) |
26 | | elicc2 13336 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β) β (π β (π΄[,]π) β (π β β β§ π΄ β€ π β§ π β€ π))) |
27 | 10, 15, 26 | syl2anc 585 |
. . . . . . 7
β’ (π β (π β (π΄[,]π) β (π β β β§ π΄ β€ π β§ π β€ π))) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π β€ π) β (π β (π΄[,]π) β (π β β β§ π΄ β€ π β§ π β€ π))) |
29 | 19, 24, 25, 28 | mpbir3and 1343 |
. . . . 5
β’ ((π β§ π β€ π) β π β (π΄[,]π)) |
30 | 12 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β π΅ β
β*) |
31 | | elicc2 13336 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β) β (π β (π΄[,]π΅) β (π β β β§ π΄ β€ π β§ π β€ π΅))) |
32 | 10, 12, 31 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π β (π΄[,]π΅) β (π β β β§ π΄ β€ π β§ π β€ π΅))) |
33 | 1, 32 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β β β§ π΄ β€ π β§ π β€ π΅)) |
34 | 33 | simp3d 1145 |
. . . . . . . . . 10
β’ (π β π β€ π΅) |
35 | | iooss2 13307 |
. . . . . . . . . 10
β’ ((π΅ β β*
β§ π β€ π΅) β (π΄(,)π) β (π΄(,)π΅)) |
36 | 30, 34, 35 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π΄(,)π) β (π΄(,)π΅)) |
37 | | ftc1.s |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β π·) |
38 | 36, 37 | sstrd 3959 |
. . . . . . . 8
β’ (π β (π΄(,)π) β π·) |
39 | 38 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β€ π) β (π΄(,)π) β π·) |
40 | 39 | sselda 3949 |
. . . . . 6
β’ (((π β§ π β€ π) β§ π‘ β (π΄(,)π)) β π‘ β π·) |
41 | | ftc1a.f |
. . . . . . . 8
β’ (π β πΉ:π·βΆβ) |
42 | 41 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β (πΉβπ‘) β β) |
43 | 42 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β€ π) β§ π‘ β π·) β (πΉβπ‘) β β) |
44 | 40, 43 | syldan 592 |
. . . . 5
β’ (((π β§ π β€ π) β§ π‘ β (π΄(,)π)) β (πΉβπ‘) β β) |
45 | 22 | simp3d 1145 |
. . . . . . . . 9
β’ (π β π β€ π΅) |
46 | | iooss2 13307 |
. . . . . . . . 9
β’ ((π΅ β β*
β§ π β€ π΅) β (π΄(,)π) β (π΄(,)π΅)) |
47 | 30, 45, 46 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄(,)π) β (π΄(,)π΅)) |
48 | 47, 37 | sstrd 3959 |
. . . . . . 7
β’ (π β (π΄(,)π) β π·) |
49 | | ioombl 24945 |
. . . . . . . 8
β’ (π΄(,)π) β dom vol |
50 | 49 | a1i 11 |
. . . . . . 7
β’ (π β (π΄(,)π) β dom vol) |
51 | | fvexd 6862 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β (πΉβπ‘) β V) |
52 | 41 | feqmptd 6915 |
. . . . . . . 8
β’ (π β πΉ = (π‘ β π· β¦ (πΉβπ‘))) |
53 | | ftc1.i |
. . . . . . . 8
β’ (π β πΉ β
πΏ1) |
54 | 52, 53 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π‘ β π· β¦ (πΉβπ‘)) β
πΏ1) |
55 | 48, 50, 51, 54 | iblss 25185 |
. . . . . 6
β’ (π β (π‘ β (π΄(,)π) β¦ (πΉβπ‘)) β
πΏ1) |
56 | 55 | adantr 482 |
. . . . 5
β’ ((π β§ π β€ π) β (π‘ β (π΄(,)π) β¦ (πΉβπ‘)) β
πΏ1) |
57 | 10 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β π΄ β
β*) |
58 | | iooss1 13306 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ π΄ β€ π) β (π(,)π) β (π΄(,)π)) |
59 | 57, 23, 58 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π(,)π) β (π΄(,)π)) |
60 | 59, 36 | sstrd 3959 |
. . . . . . . 8
β’ (π β (π(,)π) β (π΄(,)π΅)) |
61 | 60, 37 | sstrd 3959 |
. . . . . . 7
β’ (π β (π(,)π) β π·) |
62 | | ioombl 24945 |
. . . . . . . 8
β’ (π(,)π) β dom vol |
63 | 62 | a1i 11 |
. . . . . . 7
β’ (π β (π(,)π) β dom vol) |
64 | 61, 63, 51, 54 | iblss 25185 |
. . . . . 6
β’ (π β (π‘ β (π(,)π) β¦ (πΉβπ‘)) β
πΏ1) |
65 | 64 | adantr 482 |
. . . . 5
β’ ((π β§ π β€ π) β (π‘ β (π(,)π) β¦ (πΉβπ‘)) β
πΏ1) |
66 | 11, 16, 29, 44, 56, 65 | itgsplitioo 25218 |
. . . 4
β’ ((π β§ π β€ π) β β«(π΄(,)π)(πΉβπ‘) dπ‘ = (β«(π΄(,)π)(πΉβπ‘) dπ‘ + β«(π(,)π)(πΉβπ‘) dπ‘)) |
67 | 9, 66 | eqtrd 2777 |
. . 3
β’ ((π β§ π β€ π) β (πΊβπ) = (β«(π΄(,)π)(πΉβπ‘) dπ‘ + β«(π(,)π)(πΉβπ‘) dπ‘)) |
68 | | oveq2 7370 |
. . . . . . 7
β’ (π₯ = π β (π΄(,)π₯) = (π΄(,)π)) |
69 | | itgeq1 25153 |
. . . . . . 7
β’ ((π΄(,)π₯) = (π΄(,)π) β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
70 | 68, 69 | syl 17 |
. . . . . 6
β’ (π₯ = π β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
71 | | itgex 25151 |
. . . . . 6
β’
β«(π΄(,)π)(πΉβπ‘) dπ‘ β V |
72 | 70, 5, 71 | fvmpt 6953 |
. . . . 5
β’ (π β (π΄[,]π΅) β (πΊβπ) = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
73 | 17, 72 | syl 17 |
. . . 4
β’ (π β (πΊβπ) = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
74 | 73 | adantr 482 |
. . 3
β’ ((π β§ π β€ π) β (πΊβπ) = β«(π΄(,)π)(πΉβπ‘) dπ‘) |
75 | 67, 74 | oveq12d 7380 |
. 2
β’ ((π β§ π β€ π) β ((πΊβπ) β (πΊβπ)) = ((β«(π΄(,)π)(πΉβπ‘) dπ‘ + β«(π(,)π)(πΉβπ‘) dπ‘) β β«(π΄(,)π)(πΉβπ‘) dπ‘)) |
76 | | fvexd 6862 |
. . . . 5
β’ ((π β§ π‘ β (π΄(,)π)) β (πΉβπ‘) β V) |
77 | 76, 55 | itgcl 25164 |
. . . 4
β’ (π β β«(π΄(,)π)(πΉβπ‘) dπ‘ β β) |
78 | 61 | sselda 3949 |
. . . . . 6
β’ ((π β§ π‘ β (π(,)π)) β π‘ β π·) |
79 | 78, 42 | syldan 592 |
. . . . 5
β’ ((π β§ π‘ β (π(,)π)) β (πΉβπ‘) β β) |
80 | 79, 64 | itgcl 25164 |
. . . 4
β’ (π β β«(π(,)π)(πΉβπ‘) dπ‘ β β) |
81 | 77, 80 | pncan2d 11521 |
. . 3
β’ (π β ((β«(π΄(,)π)(πΉβπ‘) dπ‘ + β«(π(,)π)(πΉβπ‘) dπ‘) β β«(π΄(,)π)(πΉβπ‘) dπ‘) = β«(π(,)π)(πΉβπ‘) dπ‘) |
82 | 81 | adantr 482 |
. 2
β’ ((π β§ π β€ π) β ((β«(π΄(,)π)(πΉβπ‘) dπ‘ + β«(π(,)π)(πΉβπ‘) dπ‘) β β«(π΄(,)π)(πΉβπ‘) dπ‘) = β«(π(,)π)(πΉβπ‘) dπ‘) |
83 | 75, 82 | eqtrd 2777 |
1
β’ ((π β§ π β€ π) β ((πΊβπ) β (πΊβπ)) = β«(π(,)π)(πΉβπ‘) dπ‘) |