Step | Hyp | Ref
| Expression |
1 | | itg2split.c |
. . . . . 6
β’ ((π β§ π₯ β π) β πΆ β (0[,]+β)) |
2 | 1 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β) β§ π₯ β π) β πΆ β (0[,]+β)) |
3 | | 0e0iccpnf 13377 |
. . . . . 6
β’ 0 β
(0[,]+β) |
4 | 3 | a1i 11 |
. . . . 5
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π) β 0 β
(0[,]+β)) |
5 | 2, 4 | ifclda 4522 |
. . . 4
β’ ((π β§ π₯ β β) β if(π₯ β π, πΆ, 0) β (0[,]+β)) |
6 | | itg2split.h |
. . . 4
β’ π» = (π₯ β β β¦ if(π₯ β π, πΆ, 0)) |
7 | 5, 6 | fmptd 7063 |
. . 3
β’ (π β π»:ββΆ(0[,]+β)) |
8 | | itg2cl 25100 |
. . 3
β’ (π»:ββΆ(0[,]+β)
β (β«2βπ») β
β*) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β
(β«2βπ»)
β β*) |
10 | | itg2split.sf |
. . . 4
β’ (π β
(β«2βπΉ)
β β) |
11 | | itg2split.sg |
. . . 4
β’ (π β
(β«2βπΊ)
β β) |
12 | 10, 11 | readdcld 11185 |
. . 3
β’ (π β
((β«2βπΉ) + (β«2βπΊ)) β
β) |
13 | 12 | rexrd 11206 |
. 2
β’ (π β
((β«2βπΉ) + (β«2βπΊ)) β
β*) |
14 | | itg2split.a |
. . 3
β’ (π β π΄ β dom vol) |
15 | | itg2split.b |
. . 3
β’ (π β π΅ β dom vol) |
16 | | itg2split.i |
. . 3
β’ (π β (vol*β(π΄ β© π΅)) = 0) |
17 | | itg2split.u |
. . 3
β’ (π β π = (π΄ βͺ π΅)) |
18 | | itg2split.f |
. . 3
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, πΆ, 0)) |
19 | | itg2split.g |
. . 3
β’ πΊ = (π₯ β β β¦ if(π₯ β π΅, πΆ, 0)) |
20 | 14, 15, 16, 17, 1, 18, 19, 6, 10, 11 | itg2splitlem 25116 |
. 2
β’ (π β
(β«2βπ»)
β€ ((β«2βπΉ) + (β«2βπΊ))) |
21 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
(β«2βπΊ)
β β) |
22 | | itg2lecl 25106 |
. . . . . . . . 9
β’ ((π»:ββΆ(0[,]+β)
β§ ((β«2βπΉ) + (β«2βπΊ)) β β β§
(β«2βπ»)
β€ ((β«2βπΉ) + (β«2βπΊ))) β
(β«2βπ»)
β β) |
23 | 7, 12, 20, 22 | syl3anc 1372 |
. . . . . . . 8
β’ (π β
(β«2βπ»)
β β) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
(β«2βπ»)
β β) |
25 | | itg1cl 25052 |
. . . . . . . 8
β’ (π β dom β«1
β (β«1βπ) β β) |
26 | 25 | ad2antrl 727 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
(β«1βπ)
β β) |
27 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π β dom
β«1) |
28 | | simprrl 780 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π β dom
β«1) |
29 | 27, 28 | itg1add 25069 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(β«1β(π
βf + π)) =
((β«1βπ) + (β«1βπ))) |
30 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π»:ββΆ(0[,]+β)) |
31 | 27, 28 | i1fadd 25062 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β (π βf + π) β dom
β«1) |
32 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β© π΅) β π΄ |
33 | | mblss 24898 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β dom vol β π΄ β
β) |
34 | 14, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β β) |
35 | 32, 34 | sstrid 3956 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ β© π΅) β β) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β (π΄ β© π΅) β β) |
37 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β (vol*β(π΄ β© π΅)) = 0) |
38 | | nfv 1918 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯π |
39 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯ π β dom
β«1 |
40 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯π |
41 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯
βr β€ |
42 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π₯(π₯ β β β¦ if(π₯ β π΄, πΆ, 0)) |
43 | 18, 42 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯πΉ |
44 | 40, 41, 43 | nfbr 5153 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯ π βr β€ πΉ |
45 | 39, 44 | nfan 1903 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(π β dom β«1
β§ π βr
β€ πΉ) |
46 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯ π β dom
β«1 |
47 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯π |
48 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π₯(π₯ β β β¦ if(π₯ β π΅, πΆ, 0)) |
49 | 19, 48 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯πΊ |
50 | 47, 41, 49 | nfbr 5153 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯ π βr β€ πΊ |
51 | 46, 50 | nfan 1903 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(π β dom β«1
β§ π βr
β€ πΊ) |
52 | 45, 51 | nfan 1903 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯((π β dom β«1
β§ π βr
β€ πΉ) β§ (π β dom β«1
β§ π βr
β€ πΊ)) |
53 | 38, 52 | nfan 1903 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯(π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) |
54 | | eldifi 4087 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (β β (π΄ β© π΅)) β π₯ β β) |
55 | | i1ff 25043 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β dom β«1
β π:ββΆβ) |
56 | 27, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π:ββΆβ) |
57 | 56 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π Fn β) |
58 | | i1ff 25043 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β dom β«1
β π:ββΆβ) |
59 | 28, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π:ββΆβ) |
60 | 59 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π Fn β) |
61 | | reex 11143 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ β
β V |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β β β
V) |
63 | | inidm 4179 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
β© β) = β |
64 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β (πβπ₯) = (πβπ₯)) |
65 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β (πβπ₯) = (πβπ₯)) |
66 | 57, 60, 62, 62, 63, 64, 65 | ofval 7629 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β ((π βf + π)βπ₯) = ((πβπ₯) + (πβπ₯))) |
67 | 54, 66 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β ((π βf + π)βπ₯) = ((πβπ₯) + (πβπ₯))) |
68 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π:ββΆβ β§
π₯ β β) β
(πβπ₯) β β) |
69 | 56, 54, 68 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (πβπ₯) β β) |
70 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π:ββΆβ β§
π₯ β β) β
(πβπ₯) β β) |
71 | 59, 54, 70 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (πβπ₯) β β) |
72 | 69, 71 | readdcld 11185 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β ((πβπ₯) + (πβπ₯)) β β) |
73 | 72 | rexrd 11206 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β ((πβπ₯) + (πβπ₯)) β
β*) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β
β*) |
75 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β β) |
76 | 75 | rexrd 11206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β
β*) |
77 | | iccssxr 13348 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(0[,]+β) β β* |
78 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π»:ββΆ(0[,]+β)
β§ π₯ β β)
β (π»βπ₯) β
(0[,]+β)) |
79 | 30, 54, 78 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (π»βπ₯) β (0[,]+β)) |
80 | 77, 79 | sselid 3943 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (π»βπ₯) β
β*) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (π»βπ₯) β
β*) |
82 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β β) |
83 | | 0red 11159 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β 0 β β) |
84 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π βr β€ πΊ) |
85 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π Fn β) β β β
V) |
86 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π Fn β) β§ π₯ β β) β (πβπ₯) β V) |
87 | | ssun2 4134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ π΅ β (π΄ βͺ π΅) |
88 | 87, 17 | sseqtrrid 3998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β π΅ β π) |
89 | 88 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π₯ β π΅) β π₯ β π) |
90 | 89 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π₯ β β) β§ π₯ β π΅) β π₯ β π) |
91 | 90, 2 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π₯ β β) β§ π₯ β π΅) β πΆ β (0[,]+β)) |
92 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΅) β 0 β
(0[,]+β)) |
93 | 91, 92 | ifclda 4522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π₯ β β) β if(π₯ β π΅, πΆ, 0) β (0[,]+β)) |
94 | 93 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π Fn β) β§ π₯ β β) β if(π₯ β π΅, πΆ, 0) β (0[,]+β)) |
95 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π Fn β) β π Fn β) |
96 | | dffn5 6902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π Fn β β π = (π₯ β β β¦ (πβπ₯))) |
97 | 95, 96 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π Fn β) β π = (π₯ β β β¦ (πβπ₯))) |
98 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π Fn β) β πΊ = (π₯ β β β¦ if(π₯ β π΅, πΆ, 0))) |
99 | 85, 86, 94, 97, 98 | ofrfval2 7639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π Fn β) β (π βr β€ πΊ β βπ₯ β β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0))) |
100 | 60, 99 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β (π βr β€ πΊ β βπ₯ β β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0))) |
101 | 84, 100 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β βπ₯ β β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0)) |
102 | 101 | r19.21bi 3235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0)) |
103 | 54, 102 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0)) |
104 | 103 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0)) |
105 | | eldifn 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π₯ β (β β (π΄ β© π΅)) β Β¬ π₯ β (π΄ β© π΅)) |
106 | 105 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β Β¬ π₯ β (π΄ β© π΅)) |
107 | | elin 3927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ β (π΄ β© π΅) β (π₯ β π΄ β§ π₯ β π΅)) |
108 | 106, 107 | sylnib 328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β Β¬ (π₯ β π΄ β§ π₯ β π΅)) |
109 | | imnan 401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ β π΄ β Β¬ π₯ β π΅) β Β¬ (π₯ β π΄ β§ π₯ β π΅)) |
110 | 108, 109 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (π₯ β π΄ β Β¬ π₯ β π΅)) |
111 | 110 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β Β¬ π₯ β π΅) |
112 | 111 | iffalsed 4498 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β if(π₯ β π΅, πΆ, 0) = 0) |
113 | 104, 112 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β€ 0) |
114 | 82, 83, 75, 113 | leadd2dd 11771 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β€ ((πβπ₯) + 0)) |
115 | 75 | recnd 11184 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β β) |
116 | 115 | addid1d 11356 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β ((πβπ₯) + 0) = (πβπ₯)) |
117 | 114, 116 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β€ (πβπ₯)) |
118 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β π βr β€ πΉ) |
119 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π Fn β) β β β
V) |
120 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π Fn β) β§ π₯ β β) β (πβπ₯) β V) |
121 | | ssun1 4133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ π΄ β (π΄ βͺ π΅) |
122 | 121, 17 | sseqtrrid 3998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π΄ β π) |
123 | 122 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π₯ β π΄) β π₯ β π) |
124 | 123 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β π₯ β π) |
125 | 124, 2 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β πΆ β (0[,]+β)) |
126 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΄) β 0 β
(0[,]+β)) |
127 | 125, 126 | ifclda 4522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π₯ β β) β if(π₯ β π΄, πΆ, 0) β (0[,]+β)) |
128 | 127 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π Fn β) β§ π₯ β β) β if(π₯ β π΄, πΆ, 0) β (0[,]+β)) |
129 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π Fn β) β π Fn β) |
130 | | dffn5 6902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π Fn β β π = (π₯ β β β¦ (πβπ₯))) |
131 | 129, 130 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π Fn β) β π = (π₯ β β β¦ (πβπ₯))) |
132 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π Fn β) β πΉ = (π₯ β β β¦ if(π₯ β π΄, πΆ, 0))) |
133 | 119, 120,
128, 131, 132 | ofrfval2 7639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π Fn β) β (π βr β€ πΉ β βπ₯ β β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0))) |
134 | 57, 133 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β (π βr β€ πΉ β βπ₯ β β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0))) |
135 | 118, 134 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β βπ₯ β β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0)) |
136 | 135 | r19.21bi 3235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0)) |
137 | 54, 136 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0)) |
138 | 137 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0)) |
139 | 122 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β π΄ β π) |
140 | 139 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β π₯ β π) |
141 | 140 | iftrued 4495 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β if(π₯ β π, πΆ, 0) = πΆ) |
142 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β π₯ β β) |
143 | 5 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β if(π₯ β π, πΆ, 0) β (0[,]+β)) |
144 | 6 | fvmpt2 6960 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ β β β§ if(π₯ β π, πΆ, 0) β (0[,]+β)) β (π»βπ₯) = if(π₯ β π, πΆ, 0)) |
145 | 142, 143,
144 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β β) β (π»βπ₯) = if(π₯ β π, πΆ, 0)) |
146 | 54, 145 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β (π»βπ₯) = if(π₯ β π, πΆ, 0)) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (π»βπ₯) = if(π₯ β π, πΆ, 0)) |
148 | | iftrue 4493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β π΄ β if(π₯ β π΄, πΆ, 0) = πΆ) |
149 | 148 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β if(π₯ β π΄, πΆ, 0) = πΆ) |
150 | 141, 147,
149 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (π»βπ₯) = if(π₯ β π΄, πΆ, 0)) |
151 | 138, 150 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β (πβπ₯) β€ (π»βπ₯)) |
152 | 74, 76, 81, 117, 151 | xrletrd 13082 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β€ (π»βπ₯)) |
153 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β
β*) |
154 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β β) |
155 | 154 | rexrd 11206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β
β*) |
156 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (π»βπ₯) β
β*) |
157 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β β) |
158 | | 0red 11159 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β 0 β β) |
159 | 137 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β€ if(π₯ β π΄, πΆ, 0)) |
160 | | iffalse 4496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, πΆ, 0) = 0) |
161 | 160 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β if(π₯ β π΄, πΆ, 0) = 0) |
162 | 159, 161 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β€ 0) |
163 | 157, 158,
154, 162 | leadd1dd 11770 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β€ (0 + (πβπ₯))) |
164 | 154 | recnd 11184 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β β) |
165 | 164 | addid2d 11357 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (0 + (πβπ₯)) = (πβπ₯)) |
166 | 163, 165 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β€ (πβπ₯)) |
167 | 103 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β€ if(π₯ β π΅, πΆ, 0)) |
168 | 146 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (π»βπ₯) = if(π₯ β π, πΆ, 0)) |
169 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β π = (π΄ βͺ π΅)) |
170 | 169 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (π₯ β π β π₯ β (π΄ βͺ π΅))) |
171 | | elun 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β (π΄ βͺ π΅) β (π₯ β π΄ β¨ π₯ β π΅)) |
172 | | biorf 936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Β¬
π₯ β π΄ β (π₯ β π΅ β (π₯ β π΄ β¨ π₯ β π΅))) |
173 | 171, 172 | bitr4id 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
π₯ β π΄ β (π₯ β (π΄ βͺ π΅) β π₯ β π΅)) |
174 | 173 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (π₯ β (π΄ βͺ π΅) β π₯ β π΅)) |
175 | 170, 174 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (π₯ β π β π₯ β π΅)) |
176 | 175 | ifbid 4510 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β if(π₯ β π, πΆ, 0) = if(π₯ β π΅, πΆ, 0)) |
177 | 168, 176 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (π»βπ₯) = if(π₯ β π΅, πΆ, 0)) |
178 | 167, 177 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β (πβπ₯) β€ (π»βπ₯)) |
179 | 153, 155,
156, 166, 178 | xrletrd 13082 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β§ Β¬ π₯ β π΄) β ((πβπ₯) + (πβπ₯)) β€ (π»βπ₯)) |
180 | 152, 179 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β ((πβπ₯) + (πβπ₯)) β€ (π»βπ₯)) |
181 | 67, 180 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π₯ β (β β (π΄ β© π΅))) β ((π βf + π)βπ₯) β€ (π»βπ₯)) |
182 | 181 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β (π₯ β (β β (π΄ β© π΅)) β ((π βf + π)βπ₯) β€ (π»βπ₯))) |
183 | 53, 182 | ralrimi 3241 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β βπ₯ β (β β (π΄ β© π΅))((π βf + π)βπ₯) β€ (π»βπ₯)) |
184 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π¦((π βf + π)βπ₯) β€ (π»βπ₯) |
185 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯((π βf + π)βπ¦) |
186 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯
β€ |
187 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯(π₯ β β β¦ if(π₯ β π, πΆ, 0)) |
188 | 6, 187 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯π» |
189 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯π¦ |
190 | 188, 189 | nffv 6853 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯(π»βπ¦) |
191 | 185, 186,
190 | nfbr 5153 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯((π βf + π)βπ¦) β€ (π»βπ¦) |
192 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β ((π βf + π)βπ₯) = ((π βf + π)βπ¦)) |
193 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π»βπ₯) = (π»βπ¦)) |
194 | 192, 193 | breq12d 5119 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (((π βf + π)βπ₯) β€ (π»βπ₯) β ((π βf + π)βπ¦) β€ (π»βπ¦))) |
195 | 184, 191,
194 | cbvralw 3290 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯ β
(β β (π΄ β©
π΅))((π βf + π)βπ₯) β€ (π»βπ₯) β βπ¦ β (β β (π΄ β© π΅))((π βf + π)βπ¦) β€ (π»βπ¦)) |
196 | 183, 195 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β βπ¦ β (β β (π΄ β© π΅))((π βf + π)βπ¦) β€ (π»βπ¦)) |
197 | 196 | r19.21bi 3235 |
. . . . . . . . . . . . . 14
β’ (((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β§ π¦ β (β β (π΄ β© π΅))) β ((π βf + π)βπ¦) β€ (π»βπ¦)) |
198 | 30, 31, 36, 37, 197 | itg2uba 25111 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(β«1β(π
βf + π))
β€ (β«2βπ»)) |
199 | 29, 198 | eqbrtrrd 5130 |
. . . . . . . . . . . 12
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
((β«1βπ) + (β«1βπ)) β€
(β«2βπ»)) |
200 | 26 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(β«1βπ)
β β) |
201 | | itg1cl 25052 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β (β«1βπ) β β) |
202 | 28, 201 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(β«1βπ)
β β) |
203 | 23 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(β«2βπ»)
β β) |
204 | 200, 202,
203 | leaddsub2d 11758 |
. . . . . . . . . . . 12
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(((β«1βπ) + (β«1βπ)) β€
(β«2βπ»)
β (β«1βπ) β€ ((β«2βπ») β
(β«1βπ)))) |
205 | 199, 204 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ ((π β dom β«1 β§ π βr β€ πΉ) β§ (π β dom β«1 β§ π βr β€ πΊ))) β
(β«1βπ)
β€ ((β«2βπ») β (β«1βπ))) |
206 | 205 | anassrs 469 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ (π β dom β«1 β§ π βr β€ πΊ)) β
(β«1βπ)
β€ ((β«2βπ») β (β«1βπ))) |
207 | 206 | expr 458 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π β dom β«1) β (π βr β€ πΊ β
(β«1βπ)
β€ ((β«2βπ») β (β«1βπ)))) |
208 | 207 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β βπ β dom
β«1(π
βr β€ πΊ
β (β«1βπ) β€ ((β«2βπ») β
(β«1βπ)))) |
209 | 93, 19 | fmptd 7063 |
. . . . . . . . . 10
β’ (π β πΊ:ββΆ(0[,]+β)) |
210 | 209 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β πΊ:ββΆ(0[,]+β)) |
211 | 24, 26 | resubcld 11584 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
((β«2βπ») β (β«1βπ)) β
β) |
212 | 211 | rexrd 11206 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
((β«2βπ») β (β«1βπ)) β
β*) |
213 | | itg2leub 25102 |
. . . . . . . . 9
β’ ((πΊ:ββΆ(0[,]+β)
β§ ((β«2βπ») β (β«1βπ)) β β*)
β ((β«2βπΊ) β€ ((β«2βπ») β
(β«1βπ)) β βπ β dom β«1(π βr β€ πΊ β
(β«1βπ)
β€ ((β«2βπ») β (β«1βπ))))) |
214 | 210, 212,
213 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
((β«2βπΊ) β€ ((β«2βπ») β
(β«1βπ)) β βπ β dom β«1(π βr β€ πΊ β
(β«1βπ)
β€ ((β«2βπ») β (β«1βπ))))) |
215 | 208, 214 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
(β«2βπΊ)
β€ ((β«2βπ») β (β«1βπ))) |
216 | 21, 24, 26, 215 | lesubd 11760 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
(β«1βπ)
β€ ((β«2βπ») β (β«2βπΊ))) |
217 | 216 | expr 458 |
. . . . 5
β’ ((π β§ π β dom β«1) β (π βr β€ πΉ β
(β«1βπ)
β€ ((β«2βπ») β (β«2βπΊ)))) |
218 | 217 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β dom β«1(π βr β€ πΉ β
(β«1βπ)
β€ ((β«2βπ») β (β«2βπΊ)))) |
219 | 127, 18 | fmptd 7063 |
. . . . 5
β’ (π β πΉ:ββΆ(0[,]+β)) |
220 | 23, 11 | resubcld 11584 |
. . . . . 6
β’ (π β
((β«2βπ») β (β«2βπΊ)) β
β) |
221 | 220 | rexrd 11206 |
. . . . 5
β’ (π β
((β«2βπ») β (β«2βπΊ)) β
β*) |
222 | | itg2leub 25102 |
. . . . 5
β’ ((πΉ:ββΆ(0[,]+β)
β§ ((β«2βπ») β (β«2βπΊ)) β β*)
β ((β«2βπΉ) β€ ((β«2βπ») β
(β«2βπΊ)) β βπ β dom β«1(π βr β€ πΉ β
(β«1βπ)
β€ ((β«2βπ») β (β«2βπΊ))))) |
223 | 219, 221,
222 | syl2anc 585 |
. . . 4
β’ (π β
((β«2βπΉ) β€ ((β«2βπ») β
(β«2βπΊ)) β βπ β dom β«1(π βr β€ πΉ β
(β«1βπ)
β€ ((β«2βπ») β (β«2βπΊ))))) |
224 | 218, 223 | mpbird 257 |
. . 3
β’ (π β
(β«2βπΉ)
β€ ((β«2βπ») β (β«2βπΊ))) |
225 | | leaddsub 11632 |
. . . 4
β’
(((β«2βπΉ) β β β§
(β«2βπΊ)
β β β§ (β«2βπ») β β) β
(((β«2βπΉ) + (β«2βπΊ)) β€
(β«2βπ»)
β (β«2βπΉ) β€ ((β«2βπ») β
(β«2βπΊ)))) |
226 | 10, 11, 23, 225 | syl3anc 1372 |
. . 3
β’ (π β
(((β«2βπΉ) + (β«2βπΊ)) β€
(β«2βπ»)
β (β«2βπΉ) β€ ((β«2βπ») β
(β«2βπΊ)))) |
227 | 224, 226 | mpbird 257 |
. 2
β’ (π β
((β«2βπΉ) + (β«2βπΊ)) β€
(β«2βπ»)) |
228 | 9, 13, 20, 227 | xrletrid 13075 |
1
β’ (π β
(β«2βπ»)
= ((β«2βπΉ) + (β«2βπΊ))) |