Step | Hyp | Ref
| Expression |
1 | | itgparts.b |
. . . . . . 7
β’ (π β (π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ)) |
2 | | cncff 24279 |
. . . . . . 7
β’ ((π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ) β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
4 | 3 | fvmptelcdm 7065 |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β π΅ β β) |
5 | | ioossicc 13359 |
. . . . . . 7
β’ (π(,)π) β (π[,]π) |
6 | 5 | sseli 3944 |
. . . . . 6
β’ (π₯ β (π(,)π) β π₯ β (π[,]π)) |
7 | | itgparts.c |
. . . . . . . 8
β’ (π β (π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ)) |
8 | | cncff 24279 |
. . . . . . . 8
β’ ((π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ πΆ):(π[,]π)βΆβ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β (π₯ β (π[,]π) β¦ πΆ):(π[,]π)βΆβ) |
10 | 9 | fvmptelcdm 7065 |
. . . . . 6
β’ ((π β§ π₯ β (π[,]π)) β πΆ β β) |
11 | 6, 10 | sylan2 594 |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β πΆ β β) |
12 | 4, 11 | mulcld 11183 |
. . . 4
β’ ((π β§ π₯ β (π(,)π)) β (π΅ Β· πΆ) β β) |
13 | | itgparts.bc |
. . . 4
β’ (π β (π₯ β (π(,)π) β¦ (π΅ Β· πΆ)) β
πΏ1) |
14 | 12, 13 | itgcl 25171 |
. . 3
β’ (π β β«(π(,)π)(π΅ Β· πΆ) dπ₯ β β) |
15 | | itgparts.a |
. . . . . . . 8
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
16 | | cncff 24279 |
. . . . . . . 8
β’ ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
18 | 17 | fvmptelcdm 7065 |
. . . . . 6
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
19 | 6, 18 | sylan2 594 |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β π΄ β β) |
20 | | itgparts.d |
. . . . . . 7
β’ (π β (π₯ β (π(,)π) β¦ π·) β ((π(,)π)βcnββ)) |
21 | | cncff 24279 |
. . . . . . 7
β’ ((π₯ β (π(,)π) β¦ π·) β ((π(,)π)βcnββ) β (π₯ β (π(,)π) β¦ π·):(π(,)π)βΆβ) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ (π β (π₯ β (π(,)π) β¦ π·):(π(,)π)βΆβ) |
23 | 22 | fvmptelcdm 7065 |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β π· β β) |
24 | 19, 23 | mulcld 11183 |
. . . 4
β’ ((π β§ π₯ β (π(,)π)) β (π΄ Β· π·) β β) |
25 | | itgparts.ad |
. . . 4
β’ (π β (π₯ β (π(,)π) β¦ (π΄ Β· π·)) β
πΏ1) |
26 | 24, 25 | itgcl 25171 |
. . 3
β’ (π β β«(π(,)π)(π΄ Β· π·) dπ₯ β β) |
27 | 14, 26 | pncan2d 11522 |
. 2
β’ (π β ((β«(π(,)π)(π΅ Β· πΆ) dπ₯ + β«(π(,)π)(π΄ Β· π·) dπ₯) β β«(π(,)π)(π΅ Β· πΆ) dπ₯) = β«(π(,)π)(π΄ Β· π·) dπ₯) |
28 | 12, 13, 24, 25 | itgadd 25212 |
. . . 4
β’ (π β β«(π(,)π)((π΅ Β· πΆ) + (π΄ Β· π·)) dπ₯ = (β«(π(,)π)(π΅ Β· πΆ) dπ₯ + β«(π(,)π)(π΄ Β· π·) dπ₯)) |
29 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = π‘ β ((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) = ((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ‘)) |
30 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) |
31 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯β |
32 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯
D |
33 | | nfmpt1 5217 |
. . . . . . . . 9
β’
β²π₯(π₯ β (π[,]π) β¦ (π΄ Β· πΆ)) |
34 | 31, 32, 33 | nfov 7391 |
. . . . . . . 8
β’
β²π₯(β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ))) |
35 | | nfcv 2904 |
. . . . . . . 8
β’
β²π₯π‘ |
36 | 34, 35 | nffv 6856 |
. . . . . . 7
β’
β²π₯((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ‘) |
37 | 29, 30, 36 | cbvitg 25163 |
. . . . . 6
β’
β«(π(,)π)((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) dπ₯ = β«(π(,)π)((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ‘) dπ‘ |
38 | | itgparts.x |
. . . . . . 7
β’ (π β π β β) |
39 | | itgparts.y |
. . . . . . 7
β’ (π β π β β) |
40 | | itgparts.le |
. . . . . . 7
β’ (π β π β€ π) |
41 | | ax-resscn 11116 |
. . . . . . . . . . 11
β’ β
β β |
42 | 41 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
β) |
43 | | iccssre 13355 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β (π[,]π) β β) |
44 | 38, 39, 43 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π[,]π) β β) |
45 | 18, 10 | mulcld 11183 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π[,]π)) β (π΄ Β· πΆ) β β) |
46 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
47 | 46 | tgioo2 24189 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
48 | | iccntr 24207 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
49 | 38, 39, 48 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
50 | 42, 44, 45, 47, 46, 49 | dvmptntr 25358 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ))) = (β D (π₯ β (π(,)π) β¦ (π΄ Β· πΆ)))) |
51 | | reelprrecn 11151 |
. . . . . . . . . . 11
β’ β
β {β, β} |
52 | 51 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β {β,
β}) |
53 | 42, 44, 18, 47, 46, 49 | dvmptntr 25358 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (β D (π₯ β (π(,)π) β¦ π΄))) |
54 | | itgparts.da |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
55 | 53, 54 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
56 | 42, 44, 10, 47, 46, 49 | dvmptntr 25358 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π[,]π) β¦ πΆ)) = (β D (π₯ β (π(,)π) β¦ πΆ))) |
57 | | itgparts.dc |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π[,]π) β¦ πΆ)) = (π₯ β (π(,)π) β¦ π·)) |
58 | 56, 57 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β (π(,)π) β¦ πΆ)) = (π₯ β (π(,)π) β¦ π·)) |
59 | 52, 19, 4, 55, 11, 23, 58 | dvmptmul 25348 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π(,)π) β¦ (π΄ Β· πΆ))) = (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) |
60 | 23, 19 | mulcomd 11184 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π(,)π)) β (π· Β· π΄) = (π΄ Β· π·)) |
61 | 60 | oveq2d 7377 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(,)π)) β ((π΅ Β· πΆ) + (π· Β· π΄)) = ((π΅ Β· πΆ) + (π΄ Β· π·))) |
62 | 61 | mpteq2dva 5209 |
. . . . . . . . 9
β’ (π β (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π· Β· π΄))) = (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·)))) |
63 | 50, 59, 62 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ))) = (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·)))) |
64 | 46 | addcn 24251 |
. . . . . . . . . 10
β’ + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
65 | 64 | a1i 11 |
. . . . . . . . 9
β’ (π β + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
66 | | resmpt 5995 |
. . . . . . . . . . . 12
β’ ((π(,)π) β (π[,]π) β ((π₯ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) = (π₯ β (π(,)π) β¦ πΆ)) |
67 | 5, 66 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π₯ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) = (π₯ β (π(,)π) β¦ πΆ) |
68 | | rescncf 24283 |
. . . . . . . . . . . 12
β’ ((π(,)π) β (π[,]π) β ((π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ) β ((π₯ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) β ((π(,)π)βcnββ))) |
69 | 5, 7, 68 | mpsyl 68 |
. . . . . . . . . . 11
β’ (π β ((π₯ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) β ((π(,)π)βcnββ)) |
70 | 67, 69 | eqeltrrid 2839 |
. . . . . . . . . 10
β’ (π β (π₯ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ)) |
71 | 1, 70 | mulcncf 24833 |
. . . . . . . . 9
β’ (π β (π₯ β (π(,)π) β¦ (π΅ Β· πΆ)) β ((π(,)π)βcnββ)) |
72 | | resmpt 5995 |
. . . . . . . . . . . 12
β’ ((π(,)π) β (π[,]π) β ((π₯ β (π[,]π) β¦ π΄) βΎ (π(,)π)) = (π₯ β (π(,)π) β¦ π΄)) |
73 | 5, 72 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π₯ β (π[,]π) β¦ π΄) βΎ (π(,)π)) = (π₯ β (π(,)π) β¦ π΄) |
74 | | rescncf 24283 |
. . . . . . . . . . . 12
β’ ((π(,)π) β (π[,]π) β ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β ((π₯ β (π[,]π) β¦ π΄) βΎ (π(,)π)) β ((π(,)π)βcnββ))) |
75 | 5, 15, 74 | mpsyl 68 |
. . . . . . . . . . 11
β’ (π β ((π₯ β (π[,]π) β¦ π΄) βΎ (π(,)π)) β ((π(,)π)βcnββ)) |
76 | 73, 75 | eqeltrrid 2839 |
. . . . . . . . . 10
β’ (π β (π₯ β (π(,)π) β¦ π΄) β ((π(,)π)βcnββ)) |
77 | 76, 20 | mulcncf 24833 |
. . . . . . . . 9
β’ (π β (π₯ β (π(,)π) β¦ (π΄ Β· π·)) β ((π(,)π)βcnββ)) |
78 | 46, 65, 71, 77 | cncfmpt2f 24301 |
. . . . . . . 8
β’ (π β (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·))) β ((π(,)π)βcnββ)) |
79 | 63, 78 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ))) β ((π(,)π)βcnββ)) |
80 | 12, 13, 24, 25 | ibladd 25208 |
. . . . . . . 8
β’ (π β (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·))) β
πΏ1) |
81 | 63, 80 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ))) β
πΏ1) |
82 | 15, 7 | mulcncf 24833 |
. . . . . . 7
β’ (π β (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)) β ((π[,]π)βcnββ)) |
83 | 38, 39, 40, 79, 81, 82 | ftc2 25431 |
. . . . . 6
β’ (π β β«(π(,)π)((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ‘) dπ‘ = (((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ))) |
84 | 37, 83 | eqtrid 2785 |
. . . . 5
β’ (π β β«(π(,)π)((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) dπ₯ = (((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ))) |
85 | 63 | fveq1d 6848 |
. . . . . . . 8
β’ (π β ((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) = ((π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·)))βπ₯)) |
86 | 85 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β ((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) = ((π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·)))βπ₯)) |
87 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(,)π)) β π₯ β (π(,)π)) |
88 | | ovex 7394 |
. . . . . . . 8
β’ ((π΅ Β· πΆ) + (π΄ Β· π·)) β V |
89 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·))) = (π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·))) |
90 | 89 | fvmpt2 6963 |
. . . . . . . 8
β’ ((π₯ β (π(,)π) β§ ((π΅ Β· πΆ) + (π΄ Β· π·)) β V) β ((π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·)))βπ₯) = ((π΅ Β· πΆ) + (π΄ Β· π·))) |
91 | 87, 88, 90 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β ((π₯ β (π(,)π) β¦ ((π΅ Β· πΆ) + (π΄ Β· π·)))βπ₯) = ((π΅ Β· πΆ) + (π΄ Β· π·))) |
92 | 86, 91 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π₯ β (π(,)π)) β ((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) = ((π΅ Β· πΆ) + (π΄ Β· π·))) |
93 | 92 | itgeq2dv 25169 |
. . . . 5
β’ (π β β«(π(,)π)((β D (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)))βπ₯) dπ₯ = β«(π(,)π)((π΅ Β· πΆ) + (π΄ Β· π·)) dπ₯) |
94 | 38 | rexrd 11213 |
. . . . . . . . 9
β’ (π β π β
β*) |
95 | 39 | rexrd 11213 |
. . . . . . . . 9
β’ (π β π β
β*) |
96 | | ubicc2 13391 |
. . . . . . . . 9
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
97 | 94, 95, 40, 96 | syl3anc 1372 |
. . . . . . . 8
β’ (π β π β (π[,]π)) |
98 | | ovex 7394 |
. . . . . . . . 9
β’ (π΄ Β· πΆ) β V |
99 | 98 | csbex 5272 |
. . . . . . . 8
β’
β¦π /
π₯β¦(π΄ Β· πΆ) β V |
100 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)) = (π₯ β (π[,]π) β¦ (π΄ Β· πΆ)) |
101 | 100 | fvmpts 6955 |
. . . . . . . 8
β’ ((π β (π[,]π) β§ β¦π / π₯β¦(π΄ Β· πΆ) β V) β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) = β¦π / π₯β¦(π΄ Β· πΆ)) |
102 | 97, 99, 101 | sylancl 587 |
. . . . . . 7
β’ (π β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) = β¦π / π₯β¦(π΄ Β· πΆ)) |
103 | | itgparts.f |
. . . . . . . 8
β’ ((π β§ π₯ = π) β (π΄ Β· πΆ) = πΉ) |
104 | 39, 103 | csbied 3897 |
. . . . . . 7
β’ (π β β¦π / π₯β¦(π΄ Β· πΆ) = πΉ) |
105 | 102, 104 | eqtrd 2773 |
. . . . . 6
β’ (π β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) = πΉ) |
106 | | lbicc2 13390 |
. . . . . . . . 9
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
107 | 94, 95, 40, 106 | syl3anc 1372 |
. . . . . . . 8
β’ (π β π β (π[,]π)) |
108 | 98 | csbex 5272 |
. . . . . . . 8
β’
β¦π /
π₯β¦(π΄ Β· πΆ) β V |
109 | 100 | fvmpts 6955 |
. . . . . . . 8
β’ ((π β (π[,]π) β§ β¦π / π₯β¦(π΄ Β· πΆ) β V) β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) = β¦π / π₯β¦(π΄ Β· πΆ)) |
110 | 107, 108,
109 | sylancl 587 |
. . . . . . 7
β’ (π β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) = β¦π / π₯β¦(π΄ Β· πΆ)) |
111 | | itgparts.e |
. . . . . . . 8
β’ ((π β§ π₯ = π) β (π΄ Β· πΆ) = πΈ) |
112 | 38, 111 | csbied 3897 |
. . . . . . 7
β’ (π β β¦π / π₯β¦(π΄ Β· πΆ) = πΈ) |
113 | 110, 112 | eqtrd 2773 |
. . . . . 6
β’ (π β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) = πΈ) |
114 | 105, 113 | oveq12d 7379 |
. . . . 5
β’ (π β (((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ) β ((π₯ β (π[,]π) β¦ (π΄ Β· πΆ))βπ)) = (πΉ β πΈ)) |
115 | 84, 93, 114 | 3eqtr3d 2781 |
. . . 4
β’ (π β β«(π(,)π)((π΅ Β· πΆ) + (π΄ Β· π·)) dπ₯ = (πΉ β πΈ)) |
116 | 28, 115 | eqtr3d 2775 |
. . 3
β’ (π β (β«(π(,)π)(π΅ Β· πΆ) dπ₯ + β«(π(,)π)(π΄ Β· π·) dπ₯) = (πΉ β πΈ)) |
117 | 116 | oveq1d 7376 |
. 2
β’ (π β ((β«(π(,)π)(π΅ Β· πΆ) dπ₯ + β«(π(,)π)(π΄ Β· π·) dπ₯) β β«(π(,)π)(π΅ Β· πΆ) dπ₯) = ((πΉ β πΈ) β β«(π(,)π)(π΅ Β· πΆ) dπ₯)) |
118 | 27, 117 | eqtr3d 2775 |
1
β’ (π β β«(π(,)π)(π΄ Β· π·) dπ₯ = ((πΉ β πΈ) β β«(π(,)π)(π΅ Β· πΆ) dπ₯)) |