Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π β dom
β«1) |
2 | | itg1cl 25065 |
. . . . . 6
β’ (π β dom β«1
β (β«1βπ) β β) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1βπ)
β β) |
4 | | itg2split.a |
. . . . . . . . 9
β’ (π β π΄ β dom vol) |
5 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π΄ β dom vol) |
6 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) = (π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) |
7 | 6 | i1fres 25086 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π΄ β dom vol)
β (π₯ β β
β¦ if(π₯ β π΄, (πβπ₯), 0)) β dom
β«1) |
8 | 1, 5, 7 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) β dom
β«1) |
9 | | itg1cl 25065 |
. . . . . . 7
β’ ((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) β dom β«1 β
(β«1β(π₯
β β β¦ if(π₯
β π΄, (πβπ₯), 0))) β β) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β(π₯
β β β¦ if(π₯
β π΄, (πβπ₯), 0))) β β) |
11 | | itg2split.b |
. . . . . . . . 9
β’ (π β π΅ β dom vol) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π΅ β dom vol) |
13 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) = (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) |
14 | 13 | i1fres 25086 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π΅ β dom vol)
β (π₯ β β
β¦ if(π₯ β π΅, (πβπ₯), 0)) β dom
β«1) |
15 | 1, 12, 14 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) β dom
β«1) |
16 | | itg1cl 25065 |
. . . . . . 7
β’ ((π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) β dom β«1 β
(β«1β(π₯
β β β¦ if(π₯
β π΅, (πβπ₯), 0))) β β) |
17 | 15, 16 | syl 17 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β(π₯
β β β¦ if(π₯
β π΅, (πβπ₯), 0))) β β) |
18 | 10, 17 | readdcld 11191 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
((β«1β(π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0))) + (β«1β(π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)))) β β) |
19 | | itg2split.sf |
. . . . . . 7
β’ (π β
(β«2βπΉ)
β β) |
20 | | itg2split.sg |
. . . . . . 7
β’ (π β
(β«2βπΊ)
β β) |
21 | 19, 20 | readdcld 11191 |
. . . . . 6
β’ (π β
((β«2βπΉ) + (β«2βπΊ)) β
β) |
22 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
((β«2βπΉ) + (β«2βπΊ)) β
β) |
23 | | inss1 4193 |
. . . . . . . . 9
β’ (π΄ β© π΅) β π΄ |
24 | | mblss 24911 |
. . . . . . . . . 10
β’ (π΄ β dom vol β π΄ β
β) |
25 | 4, 24 | syl 17 |
. . . . . . . . 9
β’ (π β π΄ β β) |
26 | 23, 25 | sstrid 3960 |
. . . . . . . 8
β’ (π β (π΄ β© π΅) β β) |
27 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π΄ β© π΅) β β) |
28 | | itg2split.i |
. . . . . . . 8
β’ (π β (vol*β(π΄ β© π΅)) = 0) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (vol*β(π΄ β© π΅)) = 0) |
30 | | reex 11149 |
. . . . . . . . . . 11
β’ β
β V |
31 | 30 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
V) |
32 | | fvex 6860 |
. . . . . . . . . . . 12
β’ (πβπ₯) β V |
33 | | c0ex 11156 |
. . . . . . . . . . . 12
β’ 0 β
V |
34 | 32, 33 | ifex 4541 |
. . . . . . . . . . 11
β’ if(π₯ β π΄, (πβπ₯), 0) β V |
35 | 34 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β if(π₯ β π΄, (πβπ₯), 0) β V) |
36 | 32, 33 | ifex 4541 |
. . . . . . . . . . 11
β’ if(π₯ β π΅, (πβπ₯), 0) β V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β if(π₯ β π΅, (πβπ₯), 0) β V) |
38 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) = (π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0))) |
39 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π β (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) = (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))) |
40 | 31, 35, 37, 38, 39 | offval2 7642 |
. . . . . . . . 9
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βf + (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))) = (π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)))) |
41 | 40 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β ((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βf + (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))) = (π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)))) |
42 | 8, 15 | i1fadd 25075 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β ((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βf + (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))) β dom
β«1) |
43 | 41, 42 | eqeltrrd 2839 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0))) β dom
β«1) |
44 | | i1ff 25056 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β π:ββΆβ) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π:ββΆβ) |
46 | | eldifi 4091 |
. . . . . . . . . . . . 13
β’ (π¦ β (β β (π΄ β© π΅)) β π¦ β β) |
47 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((π:ββΆβ β§
π¦ β β) β
(πβπ¦) β β) |
48 | 45, 46, 47 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (πβπ¦) β β) |
49 | 48 | leidd 11728 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (πβπ¦) β€ (πβπ¦)) |
50 | 49 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β (πβπ¦) β€ (πβπ¦)) |
51 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π¦ β π΄ β if(π¦ β π΄, (πβπ¦), 0) = (πβπ¦)) |
52 | 51 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β if(π¦ β π΄, (πβπ¦), 0) = (πβπ¦)) |
53 | | eldifn 4092 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (β β (π΄ β© π΅)) β Β¬ π¦ β (π΄ β© π΅)) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β Β¬ π¦ β (π΄ β© π΅)) |
55 | | elin 3931 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (π΄ β© π΅) β (π¦ β π΄ β§ π¦ β π΅)) |
56 | 54, 55 | sylnib 328 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β Β¬ (π¦ β π΄ β§ π¦ β π΅)) |
57 | | imnan 401 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π΄ β Β¬ π¦ β π΅) β Β¬ (π¦ β π΄ β§ π¦ β π΅)) |
58 | 56, 57 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (π¦ β π΄ β Β¬ π¦ β π΅)) |
59 | 58 | imp 408 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β Β¬ π¦ β π΅) |
60 | | iffalse 4500 |
. . . . . . . . . . . . 13
β’ (Β¬
π¦ β π΅ β if(π¦ β π΅, (πβπ¦), 0) = 0) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β if(π¦ β π΅, (πβπ¦), 0) = 0) |
62 | 52, 61 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0)) = ((πβπ¦) + 0)) |
63 | 48 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (πβπ¦) β β) |
64 | 63 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β (πβπ¦) β β) |
65 | 64 | addid1d 11362 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β ((πβπ¦) + 0) = (πβπ¦)) |
66 | 62, 65 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0)) = (πβπ¦)) |
67 | 50, 66 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ π¦ β π΄) β (πβπ¦) β€ (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0))) |
68 | 49 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β dom β«1
β§ π βr
β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β§ π¦ β π΅) β (πβπ¦) β€ (πβπ¦)) |
69 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π¦ β π΅ β if(π¦ β π΅, (πβπ¦), 0) = (πβπ¦)) |
70 | 69 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β dom β«1
β§ π βr
β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β§ π¦ β π΅) β if(π¦ β π΅, (πβπ¦), 0) = (πβπ¦)) |
71 | 68, 70 | breqtrrd 5138 |
. . . . . . . . . . 11
β’
(((((π β§ (π β dom β«1
β§ π βr
β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β§ π¦ β π΅) β (πβπ¦) β€ if(π¦ β π΅, (πβπ¦), 0)) |
72 | | itg2split.u |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π = (π΄ βͺ π΅)) |
73 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β π = (π΄ βͺ π΅)) |
74 | 73 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (π¦ β π β π¦ β (π΄ βͺ π΅))) |
75 | | elun 4113 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (π΄ βͺ π΅) β (π¦ β π΄ β¨ π¦ β π΅)) |
76 | 74, 75 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (π¦ β π β (π¦ β π΄ β¨ π¦ β π΅))) |
77 | 76 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (Β¬ π¦ β π β Β¬ (π¦ β π΄ β¨ π¦ β π΅))) |
78 | | ioran 983 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(π¦ β π΄ β¨ π¦ β π΅) β (Β¬ π¦ β π΄ β§ Β¬ π¦ β π΅)) |
79 | 77, 78 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (Β¬ π¦ β π β (Β¬ π¦ β π΄ β§ Β¬ π¦ β π΅))) |
80 | 79 | biimpar 479 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ (Β¬ π¦ β π΄ β§ Β¬ π¦ β π΅)) β Β¬ π¦ β π) |
81 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π βr β€ π») |
82 | 45 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π Fn β) |
83 | | itg2split.c |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β π) β πΆ β (0[,]+β)) |
84 | 83 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β β) β§ π₯ β π) β πΆ β (0[,]+β)) |
85 | | 0e0iccpnf 13383 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
(0[,]+β) |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π) β 0 β
(0[,]+β)) |
87 | 84, 86 | ifclda 4526 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β β) β if(π₯ β π, πΆ, 0) β (0[,]+β)) |
88 | | itg2split.h |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π» = (π₯ β β β¦ if(π₯ β π, πΆ, 0)) |
89 | 87, 88 | fmptd 7067 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π»:ββΆ(0[,]+β)) |
90 | 89 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π» Fn β) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π» Fn β) |
92 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β β β
V) |
93 | | inidm 4183 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β
β© β) = β |
94 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β β) β (πβπ¦) = (πβπ¦)) |
95 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β β) β (π»βπ¦) = (π»βπ¦)) |
96 | 82, 91, 92, 92, 93, 94, 95 | ofrfval 7632 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π βr β€ π» β βπ¦ β β (πβπ¦) β€ (π»βπ¦))) |
97 | 81, 96 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β βπ¦ β β (πβπ¦) β€ (π»βπ¦)) |
98 | 97 | r19.21bi 3237 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β β) β (πβπ¦) β€ (π»βπ¦)) |
99 | 46, 98 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (πβπ¦) β€ (π»βπ¦)) |
100 | 99 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π) β (πβπ¦) β€ (π»βπ¦)) |
101 | 46 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β π¦ β β) |
102 | | eldif 3925 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (β β π) β (π¦ β β β§ Β¬ π¦ β π)) |
103 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯π¦ |
104 | | nfmpt1 5218 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯(π₯ β β β¦ if(π₯ β π, πΆ, 0)) |
105 | 88, 104 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯π» |
106 | 105, 103 | nffv 6857 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(π»βπ¦) |
107 | 106 | nfeq1 2923 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯(π»βπ¦) = 0 |
108 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β ((π»βπ₯) = 0 β (π»βπ¦) = 0)) |
109 | | eldif 3925 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (β β π) β (π₯ β β β§ Β¬ π₯ β π)) |
110 | 88 | fvmpt2i 6963 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β (π»βπ₯) = ( I βif(π₯ β π, πΆ, 0))) |
111 | | iffalse 4500 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π₯ β π β if(π₯ β π, πΆ, 0) = 0) |
112 | 111 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
π₯ β π β ( I βif(π₯ β π, πΆ, 0)) = ( I β0)) |
113 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β |
114 | | fvi 6922 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 β
β β ( I β0) = 0) |
115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ( I
β0) = 0 |
116 | 112, 115 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π₯ β π β ( I βif(π₯ β π, πΆ, 0)) = 0) |
117 | 110, 116 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β β β§ Β¬
π₯ β π) β (π»βπ₯) = 0) |
118 | 109, 117 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (β β π) β (π»βπ₯) = 0) |
119 | 103, 107,
108, 118 | vtoclgaf 3536 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (β β π) β (π»βπ¦) = 0) |
120 | 102, 119 | sylbir 234 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β β β§ Β¬
π¦ β π) β (π»βπ¦) = 0) |
121 | 101, 120 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π) β (π»βπ¦) = 0) |
122 | 100, 121 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π) β (πβπ¦) β€ 0) |
123 | 80, 122 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ (Β¬ π¦ β π΄ β§ Β¬ π¦ β π΅)) β (πβπ¦) β€ 0) |
124 | 123 | anassrs 469 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β dom β«1
β§ π βr
β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β§ Β¬ π¦ β π΅) β (πβπ¦) β€ 0) |
125 | 60 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β dom β«1
β§ π βr
β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β§ Β¬ π¦ β π΅) β if(π¦ β π΅, (πβπ¦), 0) = 0) |
126 | 124, 125 | breqtrrd 5138 |
. . . . . . . . . . 11
β’
(((((π β§ (π β dom β«1
β§ π βr
β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β§ Β¬ π¦ β π΅) β (πβπ¦) β€ if(π¦ β π΅, (πβπ¦), 0)) |
127 | 71, 126 | pm2.61dan 812 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β (πβπ¦) β€ if(π¦ β π΅, (πβπ¦), 0)) |
128 | | iffalse 4500 |
. . . . . . . . . . . . 13
β’ (Β¬
π¦ β π΄ β if(π¦ β π΄, (πβπ¦), 0) = 0) |
129 | 128 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β if(π¦ β π΄, (πβπ¦), 0) = 0) |
130 | 129 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0)) = (0 + if(π¦ β π΅, (πβπ¦), 0))) |
131 | | 0re 11164 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
132 | | ifcl 4536 |
. . . . . . . . . . . . . . 15
β’ (((πβπ¦) β β β§ 0 β β)
β if(π¦ β π΅, (πβπ¦), 0) β β) |
133 | 48, 131, 132 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β if(π¦ β π΅, (πβπ¦), 0) β β) |
134 | 133 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β if(π¦ β π΅, (πβπ¦), 0) β β) |
135 | 134 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β if(π¦ β π΅, (πβπ¦), 0) β β) |
136 | 135 | addid2d 11363 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β (0 + if(π¦ β π΅, (πβπ¦), 0)) = if(π¦ β π΅, (πβπ¦), 0)) |
137 | 130, 136 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0)) = if(π¦ β π΅, (πβπ¦), 0)) |
138 | 127, 137 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β§ Β¬ π¦ β π΄) β (πβπ¦) β€ (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0))) |
139 | 67, 138 | pm2.61dan 812 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (πβπ¦) β€ (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0))) |
140 | | eleq1w 2821 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (π₯ β π΄ β π¦ β π΄)) |
141 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
142 | 140, 141 | ifbieq1d 4515 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β if(π₯ β π΄, (πβπ₯), 0) = if(π¦ β π΄, (πβπ¦), 0)) |
143 | | eleq1w 2821 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (π₯ β π΅ β π¦ β π΅)) |
144 | 143, 141 | ifbieq1d 4515 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β if(π₯ β π΅, (πβπ₯), 0) = if(π¦ β π΅, (πβπ¦), 0)) |
145 | 142, 144 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)) = (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0))) |
146 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β β β¦
(if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0))) = (π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0))) |
147 | | ovex 7395 |
. . . . . . . . . 10
β’ (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0)) β V |
148 | 145, 146,
147 | fvmpt 6953 |
. . . . . . . . 9
β’ (π¦ β β β ((π₯ β β β¦
(if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)))βπ¦) = (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0))) |
149 | 101, 148 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β ((π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)))βπ¦) = (if(π¦ β π΄, (πβπ¦), 0) + if(π¦ β π΅, (πβπ¦), 0))) |
150 | 139, 149 | breqtrrd 5138 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π¦ β (β β (π΄ β© π΅))) β (πβπ¦) β€ ((π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)))βπ¦)) |
151 | 1, 27, 29, 43, 150 | itg1lea 25093 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1βπ)
β€ (β«1β(π₯ β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0))))) |
152 | 41 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βf + (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)))) = (β«1β(π₯ β β β¦
(if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0))))) |
153 | 8, 15 | itg1add 25082 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βf + (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)))) = ((β«1β(π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0))) + (β«1β(π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))))) |
154 | 152, 153 | eqtr3d 2779 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β(π₯
β β β¦ (if(π₯ β π΄, (πβπ₯), 0) + if(π₯ β π΅, (πβπ₯), 0)))) = ((β«1β(π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0))) + (β«1β(π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))))) |
155 | 151, 154 | breqtrd 5136 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1βπ)
β€ ((β«1β(π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0))) + (β«1β(π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0))))) |
156 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«2βπΉ)
β β) |
157 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«2βπΊ)
β β) |
158 | | ssun1 4137 |
. . . . . . . . . . . . . 14
β’ π΄ β (π΄ βͺ π΅) |
159 | 158, 72 | sseqtrrid 4002 |
. . . . . . . . . . . . 13
β’ (π β π΄ β π) |
160 | 159 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β π₯ β π) |
161 | 160 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β π₯ β π) |
162 | 161, 84 | syldan 592 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β πΆ β (0[,]+β)) |
163 | 85 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΄) β 0 β
(0[,]+β)) |
164 | 162, 163 | ifclda 4526 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β if(π₯ β π΄, πΆ, 0) β (0[,]+β)) |
165 | | itg2split.f |
. . . . . . . . 9
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, πΆ, 0)) |
166 | 164, 165 | fmptd 7067 |
. . . . . . . 8
β’ (π β πΉ:ββΆ(0[,]+β)) |
167 | 166 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β πΉ:ββΆ(0[,]+β)) |
168 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π₯π |
169 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π₯ π β dom
β«1 |
170 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π₯π |
171 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π₯
βr β€ |
172 | 170, 171,
105 | nfbr 5157 |
. . . . . . . . . . 11
β’
β²π₯ π βr β€ π» |
173 | 169, 172 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯(π β dom β«1
β§ π βr
β€ π») |
174 | 168, 173 | nfan 1903 |
. . . . . . . . 9
β’
β²π₯(π β§ (π β dom β«1 β§ π βr β€ π»)) |
175 | 5, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π΄ β β) |
176 | 175 | sselda 3949 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β π₯ β β) |
177 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β dom β«1) β β
β V) |
178 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β dom β«1) β§ π₯ β β) β (πβπ₯) β V) |
179 | 87 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β dom β«1) β§ π₯ β β) β if(π₯ β π, πΆ, 0) β (0[,]+β)) |
180 | 44 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β dom β«1) β π:ββΆβ) |
181 | 180 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β dom β«1) β π = (π₯ β β β¦ (πβπ₯))) |
182 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β dom β«1) β π» = (π₯ β β β¦ if(π₯ β π, πΆ, 0))) |
183 | 177, 178,
179, 181, 182 | ofrfval2 7643 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom β«1) β (π βr β€ π» β βπ₯ β β (πβπ₯) β€ if(π₯ β π, πΆ, 0))) |
184 | 183 | biimpd 228 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom β«1) β (π βr β€ π» β βπ₯ β β (πβπ₯) β€ if(π₯ β π, πΆ, 0))) |
185 | 184 | impr 456 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β βπ₯ β β (πβπ₯) β€ if(π₯ β π, πΆ, 0)) |
186 | 185 | r19.21bi 3237 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β β) β (πβπ₯) β€ if(π₯ β π, πΆ, 0)) |
187 | 176, 186 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β (πβπ₯) β€ if(π₯ β π, πΆ, 0)) |
188 | 160 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β π₯ β π) |
189 | 188 | iftrued 4499 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β if(π₯ β π, πΆ, 0) = πΆ) |
190 | 187, 189 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β (πβπ₯) β€ πΆ) |
191 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β if(π₯ β π΄, (πβπ₯), 0) = (πβπ₯)) |
192 | 191 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β if(π₯ β π΄, (πβπ₯), 0) = (πβπ₯)) |
193 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β if(π₯ β π΄, πΆ, 0) = πΆ) |
194 | 193 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β if(π₯ β π΄, πΆ, 0) = πΆ) |
195 | 190, 192,
194 | 3brtr4d 5142 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΄) β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0)) |
196 | | 0le0 12261 |
. . . . . . . . . . . . . 14
β’ 0 β€
0 |
197 | 196 | a1i 11 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π΄ β 0 β€ 0) |
198 | | iffalse 4500 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (πβπ₯), 0) = 0) |
199 | | iffalse 4500 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, πΆ, 0) = 0) |
200 | 197, 198,
199 | 3brtr4d 5142 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0)) |
201 | 200 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ Β¬ π₯ β π΄) β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0)) |
202 | 195, 201 | pm2.61dan 812 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0)) |
203 | 202 | a1d 25 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0))) |
204 | 174, 203 | ralrimi 3243 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β βπ₯ β β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0)) |
205 | 165 | a1i 11 |
. . . . . . . . . 10
β’ (π β πΉ = (π₯ β β β¦ if(π₯ β π΄, πΆ, 0))) |
206 | 31, 35, 164, 38, 205 | ofrfval2 7643 |
. . . . . . . . 9
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0))) |
207 | 206 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β ((π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β π΄, (πβπ₯), 0) β€ if(π₯ β π΄, πΆ, 0))) |
208 | 204, 207 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0)) βr β€ πΉ) |
209 | | itg2ub 25114 |
. . . . . . 7
β’ ((πΉ:ββΆ(0[,]+β)
β§ (π₯ β β
β¦ if(π₯ β π΄, (πβπ₯), 0)) β dom β«1 β§
(π₯ β β β¦
if(π₯ β π΄, (πβπ₯), 0)) βr β€ πΉ) β
(β«1β(π₯
β β β¦ if(π₯
β π΄, (πβπ₯), 0))) β€ (β«2βπΉ)) |
210 | 167, 8, 208, 209 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β(π₯
β β β¦ if(π₯
β π΄, (πβπ₯), 0))) β€ (β«2βπΉ)) |
211 | | ssun2 4138 |
. . . . . . . . . . . . . 14
β’ π΅ β (π΄ βͺ π΅) |
212 | 211, 72 | sseqtrrid 4002 |
. . . . . . . . . . . . 13
β’ (π β π΅ β π) |
213 | 212 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅) β π₯ β π) |
214 | 213 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π₯ β π΅) β π₯ β π) |
215 | 214, 84 | syldan 592 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π₯ β π΅) β πΆ β (0[,]+β)) |
216 | 85 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΅) β 0 β
(0[,]+β)) |
217 | 215, 216 | ifclda 4526 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β if(π₯ β π΅, πΆ, 0) β (0[,]+β)) |
218 | | itg2split.g |
. . . . . . . . 9
β’ πΊ = (π₯ β β β¦ if(π₯ β π΅, πΆ, 0)) |
219 | 217, 218 | fmptd 7067 |
. . . . . . . 8
β’ (π β πΊ:ββΆ(0[,]+β)) |
220 | 219 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β πΊ:ββΆ(0[,]+β)) |
221 | | mblss 24911 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β dom vol β π΅ β
β) |
222 | 12, 221 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β π΅ β β) |
223 | 222 | sselda 3949 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β π₯ β β) |
224 | 223, 186 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β (πβπ₯) β€ if(π₯ β π, πΆ, 0)) |
225 | 213 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β π₯ β π) |
226 | 225 | iftrued 4499 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β if(π₯ β π, πΆ, 0) = πΆ) |
227 | 224, 226 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β (πβπ₯) β€ πΆ) |
228 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π₯ β π΅ β if(π₯ β π΅, (πβπ₯), 0) = (πβπ₯)) |
229 | 228 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β if(π₯ β π΅, (πβπ₯), 0) = (πβπ₯)) |
230 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π₯ β π΅ β if(π₯ β π΅, πΆ, 0) = πΆ) |
231 | 230 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β if(π₯ β π΅, πΆ, 0) = πΆ) |
232 | 227, 229,
231 | 3brtr4d 5142 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ π₯ β π΅) β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0)) |
233 | 196 | a1i 11 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π΅ β 0 β€ 0) |
234 | | iffalse 4500 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π΅ β if(π₯ β π΅, (πβπ₯), 0) = 0) |
235 | | iffalse 4500 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π΅ β if(π₯ β π΅, πΆ, 0) = 0) |
236 | 233, 234,
235 | 3brtr4d 5142 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π΅ β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0)) |
237 | 236 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π βr β€ π»)) β§ Β¬ π₯ β π΅) β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0)) |
238 | 232, 237 | pm2.61dan 812 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0)) |
239 | 238 | a1d 25 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0))) |
240 | 174, 239 | ralrimi 3243 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β βπ₯ β β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0)) |
241 | 218 | a1i 11 |
. . . . . . . . . 10
β’ (π β πΊ = (π₯ β β β¦ if(π₯ β π΅, πΆ, 0))) |
242 | 31, 37, 217, 39, 241 | ofrfval2 7643 |
. . . . . . . . 9
β’ (π β ((π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) βr β€ πΊ β βπ₯ β β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0))) |
243 | 242 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β ((π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) βr β€ πΊ β βπ₯ β β if(π₯ β π΅, (πβπ₯), 0) β€ if(π₯ β π΅, πΆ, 0))) |
244 | 240, 243 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β (π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)) βr β€ πΊ) |
245 | | itg2ub 25114 |
. . . . . . 7
β’ ((πΊ:ββΆ(0[,]+β)
β§ (π₯ β β
β¦ if(π₯ β π΅, (πβπ₯), 0)) β dom β«1 β§
(π₯ β β β¦
if(π₯ β π΅, (πβπ₯), 0)) βr β€ πΊ) β
(β«1β(π₯
β β β¦ if(π₯
β π΅, (πβπ₯), 0))) β€ (β«2βπΊ)) |
246 | 220, 15, 244, 245 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1β(π₯
β β β¦ if(π₯
β π΅, (πβπ₯), 0))) β€ (β«2βπΊ)) |
247 | 10, 17, 156, 157, 210, 246 | le2addd 11781 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
((β«1β(π₯ β β β¦ if(π₯ β π΄, (πβπ₯), 0))) + (β«1β(π₯ β β β¦ if(π₯ β π΅, (πβπ₯), 0)))) β€ ((β«2βπΉ) +
(β«2βπΊ))) |
248 | 3, 18, 22, 155, 247 | letrd 11319 |
. . . 4
β’ ((π β§ (π β dom β«1 β§ π βr β€ π»)) β
(β«1βπ)
β€ ((β«2βπΉ) + (β«2βπΊ))) |
249 | 248 | expr 458 |
. . 3
β’ ((π β§ π β dom β«1) β (π βr β€ π» β
(β«1βπ)
β€ ((β«2βπΉ) + (β«2βπΊ)))) |
250 | 249 | ralrimiva 3144 |
. 2
β’ (π β βπ β dom β«1(π βr β€ π» β
(β«1βπ)
β€ ((β«2βπΉ) + (β«2βπΊ)))) |
251 | 21 | rexrd 11212 |
. . 3
β’ (π β
((β«2βπΉ) + (β«2βπΊ)) β
β*) |
252 | | itg2leub 25115 |
. . 3
β’ ((π»:ββΆ(0[,]+β)
β§ ((β«2βπΉ) + (β«2βπΊ)) β β*)
β ((β«2βπ») β€ ((β«2βπΉ) +
(β«2βπΊ)) β βπ β dom β«1(π βr β€ π» β
(β«1βπ)
β€ ((β«2βπΉ) + (β«2βπΊ))))) |
253 | 89, 251, 252 | syl2anc 585 |
. 2
β’ (π β
((β«2βπ») β€ ((β«2βπΉ) +
(β«2βπΊ)) β βπ β dom β«1(π βr β€ π» β
(β«1βπ)
β€ ((β«2βπΉ) + (β«2βπΊ))))) |
254 | 250, 253 | mpbird 257 |
1
β’ (π β
(β«2βπ»)
β€ ((β«2βπΉ) + (β«2βπΊ))) |