Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . . 6
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β π΄ β dom
vol) |
2 | | iccmbl 24953 |
. . . . . . 7
β’ ((π΅ β β β§ π₯ β β) β (π΅[,]π₯) β dom vol) |
3 | 2 | adantll 713 |
. . . . . 6
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β (π΅[,]π₯) β dom vol) |
4 | | inmbl 24929 |
. . . . . 6
β’ ((π΄ β dom vol β§ (π΅[,]π₯) β dom vol) β (π΄ β© (π΅[,]π₯)) β dom vol) |
5 | 1, 3, 4 | syl2anc 585 |
. . . . 5
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β (π΄ β© (π΅[,]π₯)) β dom vol) |
6 | | mblvol 24917 |
. . . . 5
β’ ((π΄ β© (π΅[,]π₯)) β dom vol β (volβ(π΄ β© (π΅[,]π₯))) = (vol*β(π΄ β© (π΅[,]π₯)))) |
7 | 5, 6 | syl 17 |
. . . 4
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β
(volβ(π΄ β© (π΅[,]π₯))) = (vol*β(π΄ β© (π΅[,]π₯)))) |
8 | | inss2 4193 |
. . . . 5
β’ (π΄ β© (π΅[,]π₯)) β (π΅[,]π₯) |
9 | | mblss 24918 |
. . . . . 6
β’ ((π΅[,]π₯) β dom vol β (π΅[,]π₯) β β) |
10 | 3, 9 | syl 17 |
. . . . 5
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β (π΅[,]π₯) β β) |
11 | | mblvol 24917 |
. . . . . . 7
β’ ((π΅[,]π₯) β dom vol β (volβ(π΅[,]π₯)) = (vol*β(π΅[,]π₯))) |
12 | 3, 11 | syl 17 |
. . . . . 6
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β
(volβ(π΅[,]π₯)) = (vol*β(π΅[,]π₯))) |
13 | | iccvolcl 24954 |
. . . . . . 7
β’ ((π΅ β β β§ π₯ β β) β
(volβ(π΅[,]π₯)) β
β) |
14 | 13 | adantll 713 |
. . . . . 6
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β
(volβ(π΅[,]π₯)) β
β) |
15 | 12, 14 | eqeltrrd 2835 |
. . . . 5
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β
(vol*β(π΅[,]π₯)) β
β) |
16 | | ovolsscl 24873 |
. . . . 5
β’ (((π΄ β© (π΅[,]π₯)) β (π΅[,]π₯) β§ (π΅[,]π₯) β β β§ (vol*β(π΅[,]π₯)) β β) β (vol*β(π΄ β© (π΅[,]π₯))) β β) |
17 | 8, 10, 15, 16 | mp3an2i 1467 |
. . . 4
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β
(vol*β(π΄ β© (π΅[,]π₯))) β β) |
18 | 7, 17 | eqeltrd 2834 |
. . 3
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β β) β
(volβ(π΄ β© (π΅[,]π₯))) β β) |
19 | | volcn.1 |
. . 3
β’ πΉ = (π₯ β β β¦ (volβ(π΄ β© (π΅[,]π₯)))) |
20 | 18, 19 | fmptd 7066 |
. 2
β’ ((π΄ β dom vol β§ π΅ β β) β πΉ:ββΆβ) |
21 | | simprr 772 |
. . . 4
β’ (((π΄ β dom vol β§ π΅ β β) β§ (π¦ β β β§ π β β+))
β π β
β+) |
22 | | oveq12 7370 |
. . . . . . . . . . . . 13
β’ ((π£ = π§ β§ π’ = π¦) β (π£ β π’) = (π§ β π¦)) |
23 | 22 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π’ = π¦ β§ π£ = π§) β (π£ β π’) = (π§ β π¦)) |
24 | 23 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π’ = π¦ β§ π£ = π§) β (absβ(π£ β π’)) = (absβ(π§ β π¦))) |
25 | 24 | breq1d 5119 |
. . . . . . . . . 10
β’ ((π’ = π¦ β§ π£ = π§) β ((absβ(π£ β π’)) < π β (absβ(π§ β π¦)) < π)) |
26 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π£ = π§ β (πΉβπ£) = (πΉβπ§)) |
27 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π’ = π¦ β (πΉβπ’) = (πΉβπ¦)) |
28 | 26, 27 | oveqan12rd 7381 |
. . . . . . . . . . . 12
β’ ((π’ = π¦ β§ π£ = π§) β ((πΉβπ£) β (πΉβπ’)) = ((πΉβπ§) β (πΉβπ¦))) |
29 | 28 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π’ = π¦ β§ π£ = π§) β (absβ((πΉβπ£) β (πΉβπ’))) = (absβ((πΉβπ§) β (πΉβπ¦)))) |
30 | 29 | breq1d 5119 |
. . . . . . . . . 10
β’ ((π’ = π¦ β§ π£ = π§) β ((absβ((πΉβπ£) β (πΉβπ’))) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
31 | 25, 30 | imbi12d 345 |
. . . . . . . . 9
β’ ((π’ = π¦ β§ π£ = π§) β (((absβ(π£ β π’)) < π β (absβ((πΉβπ£) β (πΉβπ’))) < π) β ((absβ(π§ β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π))) |
32 | | oveq12 7370 |
. . . . . . . . . . . . 13
β’ ((π£ = π¦ β§ π’ = π§) β (π£ β π’) = (π¦ β π§)) |
33 | 32 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π’ = π§ β§ π£ = π¦) β (π£ β π’) = (π¦ β π§)) |
34 | 33 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π’ = π§ β§ π£ = π¦) β (absβ(π£ β π’)) = (absβ(π¦ β π§))) |
35 | 34 | breq1d 5119 |
. . . . . . . . . 10
β’ ((π’ = π§ β§ π£ = π¦) β ((absβ(π£ β π’)) < π β (absβ(π¦ β π§)) < π)) |
36 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π£ = π¦ β (πΉβπ£) = (πΉβπ¦)) |
37 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β (πΉβπ’) = (πΉβπ§)) |
38 | 36, 37 | oveqan12rd 7381 |
. . . . . . . . . . . 12
β’ ((π’ = π§ β§ π£ = π¦) β ((πΉβπ£) β (πΉβπ’)) = ((πΉβπ¦) β (πΉβπ§))) |
39 | 38 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π’ = π§ β§ π£ = π¦) β (absβ((πΉβπ£) β (πΉβπ’))) = (absβ((πΉβπ¦) β (πΉβπ§)))) |
40 | 39 | breq1d 5119 |
. . . . . . . . . 10
β’ ((π’ = π§ β§ π£ = π¦) β ((absβ((πΉβπ£) β (πΉβπ’))) < π β (absβ((πΉβπ¦) β (πΉβπ§))) < π)) |
41 | 35, 40 | imbi12d 345 |
. . . . . . . . 9
β’ ((π’ = π§ β§ π£ = π¦) β (((absβ(π£ β π’)) < π β (absβ((πΉβπ£) β (πΉβπ’))) < π) β ((absβ(π¦ β π§)) < π β (absβ((πΉβπ¦) β (πΉβπ§))) < π))) |
42 | | ssidd 3971 |
. . . . . . . . 9
β’ (((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β β β β) |
43 | | recn 11149 |
. . . . . . . . . . . . 13
β’ (π§ β β β π§ β
β) |
44 | | recn 11149 |
. . . . . . . . . . . . 13
β’ (π¦ β β β π¦ β
β) |
45 | | abssub 15220 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π¦ β β) β
(absβ(π§ β π¦)) = (absβ(π¦ β π§))) |
46 | 43, 44, 45 | syl2anr 598 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π§ β β) β
(absβ(π§ β π¦)) = (absβ(π¦ β π§))) |
47 | 46 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β (absβ(π§
β π¦)) =
(absβ(π¦ β π§))) |
48 | 47 | breq1d 5119 |
. . . . . . . . . 10
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β ((absβ(π§
β π¦)) < π β (absβ(π¦ β π§)) < π)) |
49 | 20 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β πΉ:ββΆβ) |
50 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
π¦ β β) β
(πΉβπ¦) β β) |
51 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
π§ β β) β
(πΉβπ§) β β) |
52 | 50, 51 | anim12dan 620 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆβ β§
(π¦ β β β§
π§ β β)) β
((πΉβπ¦) β β β§ (πΉβπ§) β β)) |
53 | 49, 52 | sylan 581 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β ((πΉβπ¦) β β β§ (πΉβπ§) β β)) |
54 | | recn 11149 |
. . . . . . . . . . . . 13
β’ ((πΉβπ§) β β β (πΉβπ§) β β) |
55 | | recn 11149 |
. . . . . . . . . . . . 13
β’ ((πΉβπ¦) β β β (πΉβπ¦) β β) |
56 | | abssub 15220 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β β β§ (πΉβπ¦) β β) β (absβ((πΉβπ§) β (πΉβπ¦))) = (absβ((πΉβπ¦) β (πΉβπ§)))) |
57 | 54, 55, 56 | syl2anr 598 |
. . . . . . . . . . . 12
β’ (((πΉβπ¦) β β β§ (πΉβπ§) β β) β (absβ((πΉβπ§) β (πΉβπ¦))) = (absβ((πΉβπ¦) β (πΉβπ§)))) |
58 | 53, 57 | syl 17 |
. . . . . . . . . . 11
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β (absβ((πΉβπ§) β (πΉβπ¦))) = (absβ((πΉβπ¦) β (πΉβπ§)))) |
59 | 58 | breq1d 5119 |
. . . . . . . . . 10
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β ((absβ((πΉβπ§) β (πΉβπ¦))) < π β (absβ((πΉβπ¦) β (πΉβπ§))) < π)) |
60 | 48, 59 | imbi12d 345 |
. . . . . . . . 9
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β (((absβ(π§
β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π) β ((absβ(π¦ β π§)) < π β (absβ((πΉβπ¦) β (πΉβπ§))) < π))) |
61 | | simpr2 1196 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π§ β β) |
62 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π§ β (π΅[,]π₯) = (π΅[,]π§)) |
63 | 62 | ineq2d 4176 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β (π΄ β© (π΅[,]π₯)) = (π΄ β© (π΅[,]π§))) |
64 | 63 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (volβ(π΄ β© (π΅[,]π₯))) = (volβ(π΄ β© (π΅[,]π§)))) |
65 | | fvex 6859 |
. . . . . . . . . . . . . . . 16
β’
(volβ(π΄ β©
(π΅[,]π§))) β V |
66 | 64, 19, 65 | fvmpt 6952 |
. . . . . . . . . . . . . . 15
β’ (π§ β β β (πΉβπ§) = (volβ(π΄ β© (π΅[,]π§)))) |
67 | 61, 66 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ§) = (volβ(π΄ β© (π΅[,]π§)))) |
68 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π΄ β dom vol) |
69 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β π΅ β
β) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π΅ β β) |
71 | | iccmbl 24953 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅ β β β§ π§ β β) β (π΅[,]π§) β dom vol) |
72 | 70, 61, 71 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΅[,]π§) β dom vol) |
73 | | inmbl 24929 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β dom vol β§ (π΅[,]π§) β dom vol) β (π΄ β© (π΅[,]π§)) β dom vol) |
74 | 68, 72, 73 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π§)) β dom vol) |
75 | | mblvol 24917 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β© (π΅[,]π§)) β dom vol β (volβ(π΄ β© (π΅[,]π§))) = (vol*β(π΄ β© (π΅[,]π§)))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (volβ(π΄ β© (π΅[,]π§))) = (vol*β(π΄ β© (π΅[,]π§)))) |
77 | 67, 76 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ§) = (vol*β(π΄ β© (π΅[,]π§)))) |
78 | | simpr1 1195 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π¦ β β) |
79 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π΅[,]π₯) = (π΅[,]π¦)) |
80 | 79 | ineq2d 4176 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (π΄ β© (π΅[,]π₯)) = (π΄ β© (π΅[,]π¦))) |
81 | 80 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (volβ(π΄ β© (π΅[,]π₯))) = (volβ(π΄ β© (π΅[,]π¦)))) |
82 | | fvex 6859 |
. . . . . . . . . . . . . . . 16
β’
(volβ(π΄ β©
(π΅[,]π¦))) β V |
83 | 81, 19, 82 | fvmpt 6952 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (πΉβπ¦) = (volβ(π΄ β© (π΅[,]π¦)))) |
84 | 78, 83 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ¦) = (volβ(π΄ β© (π΅[,]π¦)))) |
85 | | simp1 1137 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β β β§ π§ β β β§ π¦ β€ π§) β π¦ β β) |
86 | | iccmbl 24953 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅ β β β§ π¦ β β) β (π΅[,]π¦) β dom vol) |
87 | 69, 85, 86 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΅[,]π¦) β dom vol) |
88 | | inmbl 24929 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β dom vol β§ (π΅[,]π¦) β dom vol) β (π΄ β© (π΅[,]π¦)) β dom vol) |
89 | 68, 87, 88 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π¦)) β dom vol) |
90 | | mblvol 24917 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β© (π΅[,]π¦)) β dom vol β (volβ(π΄ β© (π΅[,]π¦))) = (vol*β(π΄ β© (π΅[,]π¦)))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (volβ(π΄ β© (π΅[,]π¦))) = (vol*β(π΄ β© (π΅[,]π¦)))) |
92 | 84, 91 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ¦) = (vol*β(π΄ β© (π΅[,]π¦)))) |
93 | 77, 92 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((πΉβπ§) β (πΉβπ¦)) = ((vol*β(π΄ β© (π΅[,]π§))) β (vol*β(π΄ β© (π΅[,]π¦))))) |
94 | 49 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β πΉ:ββΆβ) |
95 | 94, 61 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ§) β β) |
96 | 77, 95 | eqeltrrd 2835 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π΄ β© (π΅[,]π§))) β β) |
97 | 70 | leidd 11729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π΅ β€ π΅) |
98 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π¦ β€ π§) |
99 | | iccss 13341 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΅ β β β§ π§ β β) β§ (π΅ β€ π΅ β§ π¦ β€ π§)) β (π΅[,]π¦) β (π΅[,]π§)) |
100 | 70, 61, 97, 98, 99 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΅[,]π¦) β (π΅[,]π§)) |
101 | | sslin 4198 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅[,]π¦) β (π΅[,]π§) β (π΄ β© (π΅[,]π¦)) β (π΄ β© (π΅[,]π§))) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π¦)) β (π΄ β© (π΅[,]π§))) |
103 | | mblss 24918 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β© (π΅[,]π§)) β dom vol β (π΄ β© (π΅[,]π§)) β β) |
104 | 74, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π§)) β β) |
105 | 102, 104 | sstrd 3958 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π¦)) β β) |
106 | | iccssre 13355 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β β β§ π§ β β) β (π¦[,]π§) β β) |
107 | 78, 61, 106 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π¦[,]π§) β β) |
108 | 105, 107 | unssd 4150 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)) β β) |
109 | 94, 78 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ¦) β β) |
110 | 92, 109 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π΄ β© (π΅[,]π¦))) β β) |
111 | 61, 78 | resubcld 11591 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π§ β π¦) β β) |
112 | 110, 111 | readdcld 11192 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦)) β β) |
113 | | ovolicc 24910 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β β β§ π§ β β β§ π¦ β€ π§) β (vol*β(π¦[,]π§)) = (π§ β π¦)) |
114 | 113 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π¦[,]π§)) = (π§ β π¦)) |
115 | 114, 111 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π¦[,]π§)) β β) |
116 | | ovolun 24886 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β© (π΅[,]π¦)) β β β§ (vol*β(π΄ β© (π΅[,]π¦))) β β) β§ ((π¦[,]π§) β β β§ (vol*β(π¦[,]π§)) β β)) β
(vol*β((π΄ β©
(π΅[,]π¦)) βͺ (π¦[,]π§))) β€ ((vol*β(π΄ β© (π΅[,]π¦))) + (vol*β(π¦[,]π§)))) |
117 | 105, 110,
107, 115, 116 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) β€ ((vol*β(π΄ β© (π΅[,]π¦))) + (vol*β(π¦[,]π§)))) |
118 | 114 | oveq2d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((vol*β(π΄ β© (π΅[,]π¦))) + (vol*β(π¦[,]π§))) = ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦))) |
119 | 117, 118 | breqtrd 5135 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) β€ ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦))) |
120 | | ovollecl 24870 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)) β β β§ ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦)) β β β§ (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) β€ ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦))) β (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) β β) |
121 | 108, 112,
119, 120 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) β β) |
122 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β π΅ β β) |
123 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β π§ β β) |
124 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β π¦ β β) |
125 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β π΅ β€ π¦) |
126 | 98 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β π¦ β€ π§) |
127 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β β β§ π§ β β β§ π¦ β€ π§) β π§ β β) |
128 | | elicc2 13338 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΅ β β β§ π§ β β) β (π¦ β (π΅[,]π§) β (π¦ β β β§ π΅ β€ π¦ β§ π¦ β€ π§))) |
129 | 69, 127, 128 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π¦ β (π΅[,]π§) β (π¦ β β β§ π΅ β€ π¦ β§ π¦ β€ π§))) |
130 | 129 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β (π¦ β (π΅[,]π§) β (π¦ β β β§ π΅ β€ π¦ β§ π¦ β€ π§))) |
131 | 124, 125,
126, 130 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β π¦ β (π΅[,]π§)) |
132 | | iccsplit 13411 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β β β§ π§ β β β§ π¦ β (π΅[,]π§)) β (π΅[,]π§) = ((π΅[,]π¦) βͺ (π¦[,]π§))) |
133 | 122, 123,
131, 132 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β (π΅[,]π§) = ((π΅[,]π¦) βͺ (π¦[,]π§))) |
134 | | eqimss 4004 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅[,]π§) = ((π΅[,]π¦) βͺ (π¦[,]π§)) β (π΅[,]π§) β ((π΅[,]π¦) βͺ (π¦[,]π§))) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π΅ β€ π¦) β (π΅[,]π§) β ((π΅[,]π¦) βͺ (π¦[,]π§))) |
136 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π¦ β€ π΅) β π¦ β β) |
137 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π¦ β€ π΅) β π§ β β) |
138 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π¦ β€ π΅) β π¦ β€ π΅) |
139 | 137 | leidd 11729 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π¦ β€ π΅) β π§ β€ π§) |
140 | | iccss 13341 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β β β§ π§ β β) β§ (π¦ β€ π΅ β§ π§ β€ π§)) β (π΅[,]π§) β (π¦[,]π§)) |
141 | 136, 137,
138, 139, 140 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π¦ β€ π΅) β (π΅[,]π§) β (π¦[,]π§)) |
142 | | ssun4 4139 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅[,]π§) β (π¦[,]π§) β (π΅[,]π§) β ((π΅[,]π¦) βͺ (π¦[,]π§))) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ (π¦ β β β§ π§ β β β§ π¦ β€ π§)) β§ π¦ β€ π΅) β (π΅[,]π§) β ((π΅[,]π¦) βͺ (π¦[,]π§))) |
144 | 70, 78, 135, 143 | lecasei 11269 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΅[,]π§) β ((π΅[,]π¦) βͺ (π¦[,]π§))) |
145 | | sslin 4198 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅[,]π§) β ((π΅[,]π¦) βͺ (π¦[,]π§)) β (π΄ β© (π΅[,]π§)) β (π΄ β© ((π΅[,]π¦) βͺ (π¦[,]π§)))) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π§)) β (π΄ β© ((π΅[,]π¦) βͺ (π¦[,]π§)))) |
147 | | indi 4237 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β© ((π΅[,]π¦) βͺ (π¦[,]π§))) = ((π΄ β© (π΅[,]π¦)) βͺ (π΄ β© (π¦[,]π§))) |
148 | | inss2 4193 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β© (π¦[,]π§)) β (π¦[,]π§) |
149 | | unss2 4145 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β© (π¦[,]π§)) β (π¦[,]π§) β ((π΄ β© (π΅[,]π¦)) βͺ (π΄ β© (π¦[,]π§))) β ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β© (π΅[,]π¦)) βͺ (π΄ β© (π¦[,]π§))) β ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)) |
151 | 147, 150 | eqsstri 3982 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β© ((π΅[,]π¦) βͺ (π¦[,]π§))) β ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)) |
152 | 146, 151 | sstrdi 3960 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (π΄ β© (π΅[,]π§)) β ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§))) |
153 | | ovolss 24872 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β© (π΅[,]π§)) β ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)) β§ ((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)) β β) β (vol*β(π΄ β© (π΅[,]π§))) β€ (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)))) |
154 | 152, 108,
153 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π΄ β© (π΅[,]π§))) β€ (vol*β((π΄ β© (π΅[,]π¦)) βͺ (π¦[,]π§)))) |
155 | 96, 121, 112, 154, 119 | letrd 11320 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π΄ β© (π΅[,]π§))) β€ ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦))) |
156 | 96, 110, 111 | lesubadd2d 11762 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (((vol*β(π΄ β© (π΅[,]π§))) β (vol*β(π΄ β© (π΅[,]π¦)))) β€ (π§ β π¦) β (vol*β(π΄ β© (π΅[,]π§))) β€ ((vol*β(π΄ β© (π΅[,]π¦))) + (π§ β π¦)))) |
157 | 155, 156 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((vol*β(π΄ β© (π΅[,]π§))) β (vol*β(π΄ β© (π΅[,]π¦)))) β€ (π§ β π¦)) |
158 | 93, 157 | eqbrtrd 5131 |
. . . . . . . . . . 11
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((πΉβπ§) β (πΉβπ¦)) β€ (π§ β π¦)) |
159 | 95, 109 | resubcld 11591 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((πΉβπ§) β (πΉβπ¦)) β β) |
160 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π β β+) |
161 | 160 | rpred 12965 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β π β β) |
162 | | lelttr 11253 |
. . . . . . . . . . . 12
β’ ((((πΉβπ§) β (πΉβπ¦)) β β β§ (π§ β π¦) β β β§ π β β) β ((((πΉβπ§) β (πΉβπ¦)) β€ (π§ β π¦) β§ (π§ β π¦) < π) β ((πΉβπ§) β (πΉβπ¦)) < π)) |
163 | 159, 111,
161, 162 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((((πΉβπ§) β (πΉβπ¦)) β€ (π§ β π¦) β§ (π§ β π¦) < π) β ((πΉβπ§) β (πΉβπ¦)) < π)) |
164 | 158, 163 | mpand 694 |
. . . . . . . . . 10
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((π§ β π¦) < π β ((πΉβπ§) β (πΉβπ¦)) < π)) |
165 | | abssubge0 15221 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π§ β β β§ π¦ β€ π§) β (absβ(π§ β π¦)) = (π§ β π¦)) |
166 | 165 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (absβ(π§ β π¦)) = (π§ β π¦)) |
167 | 166 | breq1d 5119 |
. . . . . . . . . 10
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((absβ(π§ β π¦)) < π β (π§ β π¦) < π)) |
168 | | ovolss 24872 |
. . . . . . . . . . . . . 14
β’ (((π΄ β© (π΅[,]π¦)) β (π΄ β© (π΅[,]π§)) β§ (π΄ β© (π΅[,]π§)) β β) β (vol*β(π΄ β© (π΅[,]π¦))) β€ (vol*β(π΄ β© (π΅[,]π§)))) |
169 | 102, 104,
168 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (vol*β(π΄ β© (π΅[,]π¦))) β€ (vol*β(π΄ β© (π΅[,]π§)))) |
170 | 169, 92, 77 | 3brtr4d 5141 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (πΉβπ¦) β€ (πΉβπ§)) |
171 | 109, 95, 170 | abssubge0d 15325 |
. . . . . . . . . . 11
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β (absβ((πΉβπ§) β (πΉβπ¦))) = ((πΉβπ§) β (πΉβπ¦))) |
172 | 171 | breq1d 5119 |
. . . . . . . . . 10
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((absβ((πΉβπ§) β (πΉβπ¦))) < π β ((πΉβπ§) β (πΉβπ¦)) < π)) |
173 | 164, 167,
172 | 3imtr4d 294 |
. . . . . . . . 9
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β
β§ π¦ β€ π§)) β ((absβ(π§ β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
174 | 31, 41, 42, 60, 173 | wlogle 11696 |
. . . . . . . 8
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ (π¦ β β
β§ π§ β β))
β ((absβ(π§
β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
175 | 174 | anassrs 469 |
. . . . . . 7
β’
(((((π΄ β dom
vol β§ π΅ β β)
β§ π β
β+) β§ π¦ β β) β§ π§ β β) β ((absβ(π§ β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
176 | 175 | ralrimiva 3140 |
. . . . . 6
β’ ((((π΄ β dom vol β§ π΅ β β) β§ π β β+)
β§ π¦ β β)
β βπ§ β
β ((absβ(π§
β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
177 | 176 | anasss 468 |
. . . . 5
β’ (((π΄ β dom vol β§ π΅ β β) β§ (π β β+
β§ π¦ β β))
β βπ§ β
β ((absβ(π§
β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
178 | 177 | ancom2s 649 |
. . . 4
β’ (((π΄ β dom vol β§ π΅ β β) β§ (π¦ β β β§ π β β+))
β βπ§ β
β ((absβ(π§
β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
179 | | breq2 5113 |
. . . . 5
β’ (π = π β ((absβ(π§ β π¦)) < π β (absβ(π§ β π¦)) < π)) |
180 | 179 | rspceaimv 3587 |
. . . 4
β’ ((π β β+
β§ βπ§ β
β ((absβ(π§
β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) β βπ β β+ βπ§ β β
((absβ(π§ β
π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
181 | 21, 178, 180 | syl2anc 585 |
. . 3
β’ (((π΄ β dom vol β§ π΅ β β) β§ (π¦ β β β§ π β β+))
β βπ β
β+ βπ§ β β ((absβ(π§ β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
182 | 181 | ralrimivva 3194 |
. 2
β’ ((π΄ β dom vol β§ π΅ β β) β
βπ¦ β β
βπ β
β+ βπ β β+ βπ§ β β
((absβ(π§ β
π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)) |
183 | | ax-resscn 11116 |
. . 3
β’ β
β β |
184 | | elcncf2 24276 |
. . 3
β’ ((β
β β β§ β β β) β (πΉ β (ββcnββ) β (πΉ:ββΆβ β§ βπ¦ β β βπ β β+
βπ β
β+ βπ§ β β ((absβ(π§ β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π)))) |
185 | 183, 183,
184 | mp2an 691 |
. 2
β’ (πΉ β (ββcnββ) β (πΉ:ββΆβ β§ βπ¦ β β βπ β β+
βπ β
β+ βπ§ β β ((absβ(π§ β π¦)) < π β (absβ((πΉβπ§) β (πΉβπ¦))) < π))) |
186 | 20, 182, 185 | sylanbrc 584 |
1
β’ ((π΄ β dom vol β§ π΅ β β) β πΉ β (ββcnββ)) |