Step | Hyp | Ref
| Expression |
1 | | itg2cn.4 |
. . . 4
β’ (π β πΆ β
β+) |
2 | 1 | rphalfcld 12898 |
. . 3
β’ (π β (πΆ / 2) β
β+) |
3 | | itg2cn.5 |
. . . 4
β’ (π β π β β) |
4 | 3 | nnrpd 12884 |
. . 3
β’ (π β π β
β+) |
5 | 2, 4 | rpdivcld 12903 |
. 2
β’ (π β ((πΆ / 2) / π) β
β+) |
6 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π’ β dom vol) |
7 | | itg2cn.2 |
. . . . . . . . . 10
β’ (π β πΉ β MblFn) |
8 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ β MblFn) |
9 | | itg2cn.1 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆ(0[,)+β)) |
10 | | rge0ssre 13302 |
. . . . . . . . . . 11
β’
(0[,)+β) β β |
11 | | fss 6681 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ:ββΆβ) |
14 | | mbfima 24916 |
. . . . . . . . 9
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β (π(,)+β)) β dom
vol) |
15 | 8, 13, 14 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β‘πΉ β (π(,)+β)) β dom
vol) |
16 | | inmbl 24828 |
. . . . . . . 8
β’ ((π’ β dom vol β§ (β‘πΉ β (π(,)+β)) β dom vol) β (π’ β© (β‘πΉ β (π(,)+β))) β dom
vol) |
17 | 6, 15, 16 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π’ β© (β‘πΉ β (π(,)+β))) β dom
vol) |
18 | | difmbl 24829 |
. . . . . . . 8
β’ ((π’ β dom vol β§ (β‘πΉ β (π(,)+β)) β dom vol) β (π’ β (β‘πΉ β (π(,)+β))) β dom
vol) |
19 | 6, 15, 18 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π’ β (β‘πΉ β (π(,)+β))) β dom
vol) |
20 | | inass 4178 |
. . . . . . . . . . 11
β’ ((π’ β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β)))) = (π’ β© ((β‘πΉ β (π(,)+β)) β© (π’ β (β‘πΉ β (π(,)+β))))) |
21 | | disjdif 4430 |
. . . . . . . . . . . 12
β’ ((β‘πΉ β (π(,)+β)) β© (π’ β (β‘πΉ β (π(,)+β)))) = β
|
22 | 21 | ineq2i 4168 |
. . . . . . . . . . 11
β’ (π’ β© ((β‘πΉ β (π(,)+β)) β© (π’ β (β‘πΉ β (π(,)+β))))) = (π’ β© β
) |
23 | | in0 4350 |
. . . . . . . . . . 11
β’ (π’ β© β
) =
β
|
24 | 20, 22, 23 | 3eqtri 2770 |
. . . . . . . . . 10
β’ ((π’ β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β)))) = β
|
25 | 24 | fveq2i 6841 |
. . . . . . . . 9
β’
(vol*β((π’
β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β))))) =
(vol*ββ
) |
26 | | ovol0 24779 |
. . . . . . . . 9
β’
(vol*ββ
) = 0 |
27 | 25, 26 | eqtri 2766 |
. . . . . . . 8
β’
(vol*β((π’
β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β))))) = 0 |
28 | 27 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*β((π’ β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β))))) = 0) |
29 | | inundif 4437 |
. . . . . . . . 9
β’ ((π’ β© (β‘πΉ β (π(,)+β))) βͺ (π’ β (β‘πΉ β (π(,)+β)))) = π’ |
30 | 29 | eqcomi 2747 |
. . . . . . . 8
β’ π’ = ((π’ β© (β‘πΉ β (π(,)+β))) βͺ (π’ β (β‘πΉ β (π(,)+β)))) |
31 | 30 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π’ = ((π’ β© (β‘πΉ β (π(,)+β))) βͺ (π’ β (β‘πΉ β (π(,)+β))))) |
32 | | mblss 24817 |
. . . . . . . . . 10
β’ (π’ β dom vol β π’ β
β) |
33 | 6, 32 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π’ β β) |
34 | 33 | sselda 3943 |
. . . . . . . 8
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β π’) β π₯ β β) |
35 | 9 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ:ββΆ(0[,)+β)) |
36 | 35 | ffvelcdmda 7030 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β (0[,)+β)) |
37 | | elrege0 13300 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
38 | 36, 37 | sylib 217 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
39 | 38 | simpld 496 |
. . . . . . . . . 10
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β β) |
40 | 39 | rexrd 11139 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β
β*) |
41 | 38 | simprd 497 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
42 | | elxrge0 13303 |
. . . . . . . . 9
β’ ((πΉβπ₯) β (0[,]+β) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯))) |
43 | 40, 41, 42 | sylanbrc 584 |
. . . . . . . 8
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β (0[,]+β)) |
44 | 34, 43 | syldan 592 |
. . . . . . 7
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β π’) β (πΉβπ₯) β (0[,]+β)) |
45 | | eqid 2738 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) |
46 | | eqid 2738 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) |
47 | | eqid 2738 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0)) |
48 | | 0e0iccpnf 13305 |
. . . . . . . . . 10
β’ 0 β
(0[,]+β) |
49 | | ifcl 4530 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
50 | 43, 48, 49 | sylancl 587 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
51 | 50 | fmpttd 7058 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
52 | | itg2cn.3 |
. . . . . . . . 9
β’ (π β
(β«2βπΉ)
β β) |
53 | 52 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2βπΉ) β
β) |
54 | | icossicc 13282 |
. . . . . . . . . 10
β’
(0[,)+β) β (0[,]+β) |
55 | | fss 6681 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β πΉ:ββΆ(0[,]+β)) |
56 | 35, 54, 55 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ:ββΆ(0[,]+β)) |
57 | 39 | leidd 11655 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β€ (πΉβπ₯)) |
58 | | breq1 5107 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) = if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
59 | | breq1 5107 |
. . . . . . . . . . . . 13
β’ (0 =
if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
60 | 58, 59 | ifboth 4524 |
. . . . . . . . . . . 12
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
61 | 57, 41, 60 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
62 | 61 | ralrimiva 3142 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
63 | | reex 11076 |
. . . . . . . . . . . 12
β’ β
β V |
64 | 63 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β β β
V) |
65 | | eqidd 2739 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) |
66 | 35 | feqmptd 6906 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
67 | 64, 50, 39, 65, 66 | ofrfval2 7629 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
68 | 62, 67 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ) |
69 | | itg2le 25026 |
. . . . . . . . 9
β’ (((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
πΉ:ββΆ(0[,]+β) β§ (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ) β
(β«2β(π₯
β β β¦ if(π₯
β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
70 | 51, 56, 68, 69 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
71 | | itg2lecl 25025 |
. . . . . . . 8
β’ (((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(β«2βπΉ)
β β β§ (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) β
(β«2β(π₯
β β β¦ if(π₯
β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
72 | 51, 53, 70, 71 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
73 | | ifcl 4530 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
74 | 43, 48, 73 | sylancl 587 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
75 | 74 | fmpttd 7058 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
76 | | breq1 5107 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) = if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
77 | | breq1 5107 |
. . . . . . . . . . . . 13
β’ (0 =
if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
78 | 76, 77 | ifboth 4524 |
. . . . . . . . . . . 12
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
79 | 57, 41, 78 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
80 | 79 | ralrimiva 3142 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
81 | | eqidd 2739 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) |
82 | 64, 74, 39, 81, 66 | ofrfval2 7629 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
83 | 80, 82 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ) |
84 | | itg2le 25026 |
. . . . . . . . 9
β’ (((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
πΉ:ββΆ(0[,]+β) β§ (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ) β
(β«2β(π₯
β β β¦ if(π₯
β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
85 | 75, 56, 83, 84 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
86 | | itg2lecl 25025 |
. . . . . . . 8
β’ (((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(β«2βπΉ)
β β β§ (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) β
(β«2β(π₯
β β β¦ if(π₯
β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
87 | 75, 53, 85, 86 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
88 | 17, 19, 28, 31, 44, 45, 46, 47, 72, 87 | itg2split 25036 |
. . . . . 6
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) = ((β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
89 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΆ β
β+) |
90 | 89 | rphalfcld 12898 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (πΆ / 2) β
β+) |
91 | 90 | rpred 12886 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (πΆ / 2) β β) |
92 | | ifcl 4530 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β (0[,]+β)) |
93 | 43, 48, 92 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β (0[,]+β)) |
94 | 93 | fmpttd 7058 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
95 | | breq1 5107 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) = if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
96 | | breq1 5107 |
. . . . . . . . . . . . . 14
β’ (0 =
if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
97 | 95, 96 | ifboth 4524 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
98 | 57, 41, 97 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
99 | 98 | ralrimiva 3142 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
100 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) |
101 | 64, 93, 43, 100, 66 | ofrfval2 7629 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
102 | 99, 101 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) βr β€ πΉ) |
103 | | itg2le 25026 |
. . . . . . . . . 10
β’ (((π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
πΉ:ββΆ(0[,]+β) β§ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) βr β€ πΉ) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
104 | 94, 56, 102, 103 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
105 | | itg2lecl 25025 |
. . . . . . . . 9
β’ (((π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(β«2βπΉ)
β β β§ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β€ (β«2βπΉ)) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β β) |
106 | 94, 53, 104, 105 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β β) |
107 | | 0red 11092 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β 0 β
β) |
108 | | elinel2 4155 |
. . . . . . . . . . . . 13
β’ (π₯ β (π’ β© (β‘πΉ β (π(,)+β))) β π₯ β (β‘πΉ β (π(,)+β))) |
109 | 108 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (π’ β© (β‘πΉ β (π(,)+β))) β π₯ β (β‘πΉ β (π(,)+β)))) |
110 | | ifle 13045 |
. . . . . . . . . . . 12
β’ ((((πΉβπ₯) β β β§ 0 β β β§
0 β€ (πΉβπ₯)) β§ (π₯ β (π’ β© (β‘πΉ β (π(,)+β))) β π₯ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
111 | 39, 107, 41, 109, 110 | syl31anc 1374 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
112 | 111 | ralrimiva 3142 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
113 | 64, 50, 93, 65, 100 | ofrfval2 7629 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) |
114 | 112, 113 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) |
115 | | itg2le 25026 |
. . . . . . . . 9
β’ (((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(π₯ β β β¦
if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(π₯ β β β¦
if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β
(β«2β(π₯
β β β¦ if(π₯
β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)))) |
116 | 51, 94, 114, 115 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)))) |
117 | 66 | fveq2d 6842 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2βπΉ) =
(β«2β(π₯
β β β¦ (πΉβπ₯)))) |
118 | | cmmbl 24820 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β (π(,)+β)) β dom vol β (β
β (β‘πΉ β (π(,)+β))) β dom
vol) |
119 | 15, 118 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β β (β‘πΉ β (π(,)+β))) β dom
vol) |
120 | | disjdif 4430 |
. . . . . . . . . . . . . . 15
β’ ((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β)))) = β
|
121 | 120 | fveq2i 6841 |
. . . . . . . . . . . . . 14
β’
(vol*β((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β))))) =
(vol*ββ
) |
122 | 121, 26 | eqtri 2766 |
. . . . . . . . . . . . 13
β’
(vol*β((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β))))) = 0 |
123 | 122 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*β((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β))))) = 0) |
124 | | undif2 4435 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β (π(,)+β)) βͺ (β β (β‘πΉ β (π(,)+β)))) = ((β‘πΉ β (π(,)+β)) βͺ
β) |
125 | | mblss 24817 |
. . . . . . . . . . . . . . 15
β’ ((β‘πΉ β (π(,)+β)) β dom vol β (β‘πΉ β (π(,)+β)) β
β) |
126 | 15, 125 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β‘πΉ β (π(,)+β)) β
β) |
127 | | ssequn1 4139 |
. . . . . . . . . . . . . 14
β’ ((β‘πΉ β (π(,)+β)) β β β ((β‘πΉ β (π(,)+β)) βͺ β) =
β) |
128 | 126, 127 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β‘πΉ β (π(,)+β)) βͺ β) =
β) |
129 | 124, 128 | eqtr2id 2791 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β β = ((β‘πΉ β (π(,)+β)) βͺ (β β (β‘πΉ β (π(,)+β))))) |
130 | | eqid 2738 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
131 | | eqid 2738 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) |
132 | | iftrue 4491 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β if(π₯ β β, (πΉβπ₯), 0) = (πΉβπ₯)) |
133 | 132 | mpteq2ia 5207 |
. . . . . . . . . . . . 13
β’ (π₯ β β β¦ if(π₯ β β, (πΉβπ₯), 0)) = (π₯ β β β¦ (πΉβπ₯)) |
134 | 133 | eqcomi 2747 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦ (πΉβπ₯)) = (π₯ β β β¦ if(π₯ β β, (πΉβπ₯), 0)) |
135 | | ifcl 4530 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
136 | 43, 48, 135 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
137 | 136 | fmpttd 7058 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
138 | | breq1 5107 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ₯) = if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
139 | | breq1 5107 |
. . . . . . . . . . . . . . . . . 18
β’ (0 =
if(π₯ β (β
β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
140 | 138, 139 | ifboth 4524 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
141 | 57, 41, 140 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
142 | 141 | ralrimiva 3142 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
143 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) |
144 | 64, 136, 43, 143, 66 | ofrfval2 7629 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
145 | 142, 144 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ) |
146 | | itg2le 25026 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
πΉ:ββΆ(0[,]+β) β§ (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ) β
(β«2β(π₯
β β β¦ if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
147 | 137, 56, 145, 146 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) |
148 | | itg2lecl 25025 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(β«2βπΉ)
β β β§ (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2βπΉ)) β
(β«2β(π₯
β β β¦ if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
149 | 137, 53, 147, 148 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
150 | 15, 119, 123, 129, 43, 130, 131, 134, 106, 149 | itg2split 25036 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ (πΉβπ₯))) = ((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
151 | 117, 150 | eqtrd 2778 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2βπΉ) =
((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
152 | | eldif 3919 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (β β (β‘πΉ β (π(,)+β))) β (π₯ β β β§ Β¬ π₯ β (β‘πΉ β (π(,)+β)))) |
153 | 152 | baib 537 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (π₯ β (β β (β‘πΉ β (π(,)+β))) β Β¬ π₯ β (β‘πΉ β (π(,)+β)))) |
154 | 153 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (β β (β‘πΉ β (π(,)+β))) β Β¬ π₯ β (β‘πΉ β (π(,)+β)))) |
155 | 9 | ffnd 6665 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΉ Fn β) |
156 | 155 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β πΉ Fn β) |
157 | | elpreima 7004 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ Fn β β (π₯ β (β‘πΉ β (π(,)+β)) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (β‘πΉ β (π(,)+β)) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
159 | 39 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π < (πΉβπ₯) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
160 | 3 | nnred 12102 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β) |
161 | 160 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β π β β) |
162 | 161 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β π β
β*) |
163 | | elioopnf 13289 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β*
β ((πΉβπ₯) β (π(,)+β) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β ((πΉβπ₯) β (π(,)+β) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
165 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β π₯ β β) |
166 | 165 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β ((πΉβπ₯) β (π(,)+β) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
167 | 159, 164,
166 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π < (πΉβπ₯) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
168 | 161, 39 | ltnled 11236 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π < (πΉβπ₯) β Β¬ (πΉβπ₯) β€ π)) |
169 | 158, 167,
168 | 3bitr2rd 308 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (Β¬ (πΉβπ₯) β€ π β π₯ β (β‘πΉ β (π(,)+β)))) |
170 | 169 | con1bid 356 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (Β¬ π₯ β (β‘πΉ β (π(,)+β)) β (πΉβπ₯) β€ π)) |
171 | 154, 170 | bitrd 279 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (β β (β‘πΉ β (π(,)+β))) β (πΉβπ₯) β€ π)) |
172 | 171 | ifbid 4508 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
173 | 172 | mpteq2dva 5204 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
174 | 173 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) = (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
175 | | itg2cn.6 |
. . . . . . . . . . . . . 14
β’ (π β Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
176 | 175 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
177 | 174, 176 | eqnbrtrd 5122 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β Β¬
(β«2β(π₯
β β β¦ if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
178 | 53, 91 | resubcld 11517 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2βπΉ) β (πΆ / 2)) β β) |
179 | 178, 149 | ltnled 11236 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (((β«2βπΉ) β (πΆ / 2)) < (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β Β¬
(β«2β(π₯
β β β¦ if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) |
180 | 177, 179 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2βπΉ) β (πΆ / 2)) < (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) |
181 | 53, 91, 149 | ltsubadd2d 11687 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (((β«2βπΉ) β (πΆ / 2)) < (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β (β«2βπΉ) < ((πΆ / 2) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))))) |
182 | 180, 181 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2βπΉ) < ((πΆ / 2) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
183 | 151, 182 | eqbrtrrd 5128 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) < ((πΆ / 2) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
184 | 106, 91, 149 | ltadd1d 11682 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) < (πΆ / 2) β
((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) < ((πΆ / 2) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))))) |
185 | 183, 184 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) < (πΆ / 2)) |
186 | 72, 106, 91, 116, 185 | lelttrd 11247 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) < (πΆ / 2)) |
187 | 160 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β β) |
188 | | mblvol 24816 |
. . . . . . . . . . 11
β’ (π’ β dom vol β
(volβπ’) =
(vol*βπ’)) |
189 | 6, 188 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (volβπ’) = (vol*βπ’)) |
190 | 5 | rpred 12886 |
. . . . . . . . . . . 12
β’ (π β ((πΆ / 2) / π) β β) |
191 | 190 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((πΆ / 2) / π) β β) |
192 | | ovolcl 24764 |
. . . . . . . . . . . . 13
β’ (π’ β β β
(vol*βπ’) β
β*) |
193 | 33, 192 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) β
β*) |
194 | 191 | rexrd 11139 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((πΆ / 2) / π) β
β*) |
195 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (volβπ’) < ((πΆ / 2) / π)) |
196 | 189, 195 | eqbrtrrd 5128 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) < ((πΆ / 2) / π)) |
197 | 193, 194,
196 | xrltled 12998 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) β€ ((πΆ / 2) / π)) |
198 | | ovollecl 24769 |
. . . . . . . . . . 11
β’ ((π’ β β β§ ((πΆ / 2) / π) β β β§ (vol*βπ’) β€ ((πΆ / 2) / π)) β (vol*βπ’) β β) |
199 | 33, 191, 197, 198 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) β β) |
200 | 189, 199 | eqeltrd 2839 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (volβπ’) β β) |
201 | 187, 200 | remulcld 11119 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π Β· (volβπ’)) β β) |
202 | 187 | rexrd 11139 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β
β*) |
203 | 3 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β β) |
204 | 203 | nnnn0d 12407 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β
β0) |
205 | 204 | nn0ge0d 12410 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β 0 β€ π) |
206 | | elxrge0 13303 |
. . . . . . . . . . . . . 14
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
207 | 202, 205,
206 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β (0[,]+β)) |
208 | | ifcl 4530 |
. . . . . . . . . . . . 13
β’ ((π β (0[,]+β) β§ 0
β (0[,]+β)) β if(π₯ β π’, π, 0) β (0[,]+β)) |
209 | 207, 48, 208 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β if(π₯ β π’, π, 0) β (0[,]+β)) |
210 | 209 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β π’, π, 0) β (0[,]+β)) |
211 | 210 | fmpttd 7058 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β π’, π,
0)):ββΆ(0[,]+β)) |
212 | | eldifn 4086 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π’ β (β‘πΉ β (π(,)+β))) β Β¬ π₯ β (β‘πΉ β (π(,)+β))) |
213 | 212 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β Β¬ π₯ β (β‘πΉ β (π(,)+β))) |
214 | | difssd 4091 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π’ β (β‘πΉ β (π(,)+β))) β π’) |
215 | 214 | sselda 3943 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β π₯ β π’) |
216 | 34, 169 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β π’) β (Β¬ (πΉβπ₯) β€ π β π₯ β (β‘πΉ β (π(,)+β)))) |
217 | 215, 216 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β (Β¬ (πΉβπ₯) β€ π β π₯ β (β‘πΉ β (π(,)+β)))) |
218 | 217 | con1bid 356 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β (Β¬ π₯ β (β‘πΉ β (π(,)+β)) β (πΉβπ₯) β€ π)) |
219 | 213, 218 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β (πΉβπ₯) β€ π) |
220 | | iftrue 4491 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π’ β (β‘πΉ β (π(,)+β))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = (πΉβπ₯)) |
221 | 220 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = (πΉβπ₯)) |
222 | 215 | iftrued 4493 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β π’, π, 0) = π) |
223 | 219, 221,
222 | 3brtr4d 5136 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
224 | | iffalse 4494 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π₯ β (π’ β (β‘πΉ β (π(,)+β))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = 0) |
225 | 224 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ Β¬ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = 0) |
226 | | 0le0 12188 |
. . . . . . . . . . . . . . . 16
β’ 0 β€
0 |
227 | | breq2 5108 |
. . . . . . . . . . . . . . . . 17
β’ (π = if(π₯ β π’, π, 0) β (0 β€ π β 0 β€ if(π₯ β π’, π, 0))) |
228 | | breq2 5108 |
. . . . . . . . . . . . . . . . 17
β’ (0 =
if(π₯ β π’, π, 0) β (0 β€ 0 β 0 β€ if(π₯ β π’, π, 0))) |
229 | 227, 228 | ifboth 4524 |
. . . . . . . . . . . . . . . 16
β’ ((0 β€
π β§ 0 β€ 0) β 0
β€ if(π₯ β π’, π, 0)) |
230 | 205, 226,
229 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β 0 β€ if(π₯ β π’, π, 0)) |
231 | 230 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ Β¬ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β 0 β€ if(π₯ β π’, π, 0)) |
232 | 225, 231 | eqbrtrd 5126 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ Β¬ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
233 | 223, 232 | pm2.61dan 812 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
234 | 233 | ralrimivw 3146 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
235 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β π’, π, 0)) = (π₯ β β β¦ if(π₯ β π’, π, 0))) |
236 | 64, 74, 210, 81, 235 | ofrfval2 7629 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β π’, π, 0)) β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0))) |
237 | 234, 236 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β π’, π, 0))) |
238 | | itg2le 25026 |
. . . . . . . . . 10
β’ (((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)):ββΆ(0[,]+β) β§
(π₯ β β β¦
if(π₯ β π’, π, 0)):ββΆ(0[,]+β) β§
(π₯ β β β¦
if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β π’, π, 0))) β
(β«2β(π₯
β β β¦ if(π₯
β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0)))) |
239 | 75, 211, 237, 238 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0)))) |
240 | | elrege0 13300 |
. . . . . . . . . . 11
β’ (π β (0[,)+β) β
(π β β β§ 0
β€ π)) |
241 | 187, 205,
240 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β (0[,)+β)) |
242 | | itg2const 25027 |
. . . . . . . . . 10
β’ ((π’ β dom vol β§
(volβπ’) β
β β§ π β
(0[,)+β)) β (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0))) = (π Β· (volβπ’))) |
243 | 6, 200, 241, 242 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0))) = (π Β· (volβπ’))) |
244 | 239, 243 | breqtrd 5130 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (π Β· (volβπ’))) |
245 | 203 | nngt0d 12136 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β 0 < π) |
246 | | ltmuldiv2 11963 |
. . . . . . . . . 10
β’
(((volβπ’)
β β β§ (πΆ /
2) β β β§ (π
β β β§ 0 < π)) β ((π Β· (volβπ’)) < (πΆ / 2) β (volβπ’) < ((πΆ / 2) / π))) |
247 | 200, 91, 187, 245, 246 | syl112anc 1375 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π Β· (volβπ’)) < (πΆ / 2) β (volβπ’) < ((πΆ / 2) / π))) |
248 | 195, 247 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π Β· (volβπ’)) < (πΆ / 2)) |
249 | 87, 201, 91, 244, 248 | lelttrd 11247 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) < (πΆ / 2)) |
250 | 72, 87, 91, 91, 186, 249 | lt2addd 11712 |
. . . . . 6
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) < ((πΆ / 2) + (πΆ / 2))) |
251 | 88, 250 | eqbrtrd 5126 |
. . . . 5
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < ((πΆ / 2) + (πΆ / 2))) |
252 | 89 | rpcnd 12888 |
. . . . . 6
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΆ β β) |
253 | 252 | 2halvesd 12333 |
. . . . 5
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((πΆ / 2) + (πΆ / 2)) = πΆ) |
254 | 251, 253 | breqtrd 5130 |
. . . 4
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ) |
255 | 254 | expr 458 |
. . 3
β’ ((π β§ π’ β dom vol) β ((volβπ’) < ((πΆ / 2) / π) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
256 | 255 | ralrimiva 3142 |
. 2
β’ (π β βπ’ β dom vol((volβπ’) < ((πΆ / 2) / π) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
257 | | breq2 5108 |
. . 3
β’ (π = ((πΆ / 2) / π) β ((volβπ’) < π β (volβπ’) < ((πΆ / 2) / π))) |
258 | 257 | rspceaimv 3584 |
. 2
β’ ((((πΆ / 2) / π) β β+ β§
βπ’ β dom
vol((volβπ’) <
((πΆ / 2) / π) β
(β«2β(π₯
β β β¦ if(π₯
β π’, (πΉβπ₯), 0))) < πΆ)) β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
259 | 5, 256, 258 | syl2anc 585 |
1
β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |