Step | Hyp | Ref
| Expression |
1 | | itg2cn.4 |
. . . 4
β’ (π β πΆ β
β+) |
2 | 1 | rphalfcld 12897 |
. . 3
β’ (π β (πΆ / 2) β
β+) |
3 | | itg2cn.5 |
. . . 4
β’ (π β π β β) |
4 | 3 | nnrpd 12883 |
. . 3
β’ (π β π β
β+) |
5 | 2, 4 | rpdivcld 12902 |
. 2
β’ (π β ((πΆ / 2) / π) β
β+) |
6 | | simprl 769 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π’ β dom vol) |
7 | | itg2cn.2 |
. . . . . . . . . 10
β’ (π β πΉ β MblFn) |
8 | 7 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ β MblFn) |
9 | | itg2cn.1 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆ(0[,)+β)) |
10 | | rge0ssre 13301 |
. . . . . . . . . . 11
β’
(0[,)+β) β β |
11 | | fss 6680 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
12 | 9, 10, 11 | sylancl 586 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
13 | 12 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ:ββΆβ) |
14 | | mbfima 24916 |
. . . . . . . . 9
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β (π(,)+β)) β dom
vol) |
15 | 8, 13, 14 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β‘πΉ β (π(,)+β)) β dom
vol) |
16 | | inmbl 24828 |
. . . . . . . 8
β’ ((π’ β dom vol β§ (β‘πΉ β (π(,)+β)) β dom vol) β (π’ β© (β‘πΉ β (π(,)+β))) β dom
vol) |
17 | 6, 15, 16 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π’ β© (β‘πΉ β (π(,)+β))) β dom
vol) |
18 | | difmbl 24829 |
. . . . . . . 8
β’ ((π’ β dom vol β§ (β‘πΉ β (π(,)+β)) β dom vol) β (π’ β (β‘πΉ β (π(,)+β))) β dom
vol) |
19 | 6, 15, 18 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π’ β (β‘πΉ β (π(,)+β))) β dom
vol) |
20 | | inass 4177 |
. . . . . . . . . . 11
β’ ((π’ β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β)))) = (π’ β© ((β‘πΉ β (π(,)+β)) β© (π’ β (β‘πΉ β (π(,)+β))))) |
21 | | disjdif 4429 |
. . . . . . . . . . . 12
β’ ((β‘πΉ β (π(,)+β)) β© (π’ β (β‘πΉ β (π(,)+β)))) = β
|
22 | 21 | ineq2i 4167 |
. . . . . . . . . . 11
β’ (π’ β© ((β‘πΉ β (π(,)+β)) β© (π’ β (β‘πΉ β (π(,)+β))))) = (π’ β© β
) |
23 | | in0 4349 |
. . . . . . . . . . 11
β’ (π’ β© β
) =
β
|
24 | 20, 22, 23 | 3eqtri 2769 |
. . . . . . . . . 10
β’ ((π’ β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β)))) = β
|
25 | 24 | fveq2i 6840 |
. . . . . . . . 9
β’
(vol*β((π’
β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β))))) =
(vol*ββ
) |
26 | | ovol0 24779 |
. . . . . . . . 9
β’
(vol*ββ
) = 0 |
27 | 25, 26 | eqtri 2765 |
. . . . . . . 8
β’
(vol*β((π’
β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β))))) = 0 |
28 | 27 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*β((π’ β© (β‘πΉ β (π(,)+β))) β© (π’ β (β‘πΉ β (π(,)+β))))) = 0) |
29 | | inundif 4436 |
. . . . . . . . 9
β’ ((π’ β© (β‘πΉ β (π(,)+β))) βͺ (π’ β (β‘πΉ β (π(,)+β)))) = π’ |
30 | 29 | eqcomi 2746 |
. . . . . . . 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 3942 |
. . . . . . . 8
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β π’) β π₯ β β) |
35 | 9 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ:ββΆ(0[,)+β)) |
36 | 35 | ffvelcdmda 7029 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β (0[,)+β)) |
37 | | elrege0 13299 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
38 | 36, 37 | sylib 217 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
39 | 38 | simpld 495 |
. . . . . . . . . 10
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β β) |
40 | 39 | rexrd 11138 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β
β*) |
41 | 38 | simprd 496 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
42 | | elxrge0 13302 |
. . . . . . . . 9
β’ ((πΉβπ₯) β (0[,]+β) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯))) |
43 | 40, 41, 42 | sylanbrc 583 |
. . . . . . . 8
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β (0[,]+β)) |
44 | 34, 43 | syldan 591 |
. . . . . . 7
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β π’) β (πΉβπ₯) β (0[,]+β)) |
45 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) |
46 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) |
47 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0)) |
48 | | 0e0iccpnf 13304 |
. . . . . . . . . 10
β’ 0 β
(0[,]+β) |
49 | | ifcl 4529 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
50 | 43, 48, 49 | sylancl 586 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
51 | 50 | fmpttd 7057 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
52 | | itg2cn.3 |
. . . . . . . . 9
β’ (π β
(β«2βπΉ)
β β) |
53 | 52 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2βπΉ) β
β) |
54 | | icossicc 13281 |
. . . . . . . . . 10
β’
(0[,)+β) β (0[,]+β) |
55 | | fss 6680 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β πΉ:ββΆ(0[,]+β)) |
56 | 35, 54, 55 | sylancl 586 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ:ββΆ(0[,]+β)) |
57 | 39 | leidd 11654 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (πΉβπ₯) β€ (πΉβπ₯)) |
58 | | breq1 5106 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) = if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
59 | | breq1 5106 |
. . . . . . . . . . . . 13
β’ (0 =
if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
60 | 58, 59 | ifboth 4523 |
. . . . . . . . . . . 12
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
61 | 57, 41, 60 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
62 | 61 | ralrimiva 3141 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
63 | | reex 11075 |
. . . . . . . . . . . 12
β’ β
β V |
64 | 63 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β β β
V) |
65 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) |
66 | 35 | feqmptd 6905 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
67 | 64, 50, 39, 65, 66 | ofrfval2 7628 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
68 | 62, 67 | mpbird 256 |
. . . . . . . . 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 1371 |
. . . . . . . 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 1371 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β β) |
73 | | ifcl 4529 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
74 | 43, 48, 73 | sylancl 586 |
. . . . . . . . 9
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
75 | 74 | fmpttd 7057 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
76 | | breq1 5106 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) = if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
77 | | breq1 5106 |
. . . . . . . . . . . . 13
β’ (0 =
if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
78 | 76, 77 | ifboth 4523 |
. . . . . . . . . . . 12
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
79 | 57, 41, 78 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
80 | 79 | ralrimiva 3141 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
81 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) |
82 | 64, 74, 39, 81, 66 | ofrfval2 7628 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
83 | 80, 82 | mpbird 256 |
. . . . . . . . 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 1371 |
. . . . . . . 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 1371 |
. . . . . . 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 481 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΆ β
β+) |
90 | 89 | rphalfcld 12897 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (πΆ / 2) β
β+) |
91 | 90 | rpred 12885 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (πΆ / 2) β β) |
92 | | ifcl 4529 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β (0[,]+β)) |
93 | 43, 48, 92 | sylancl 586 |
. . . . . . . . . 10
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β (0[,]+β)) |
94 | 93 | fmpttd 7057 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
95 | | breq1 5106 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) = if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
96 | | breq1 5106 |
. . . . . . . . . . . . . 14
β’ (0 =
if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
97 | 95, 96 | ifboth 4523 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
98 | 57, 41, 97 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
99 | 98 | ralrimiva 3141 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
100 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) |
101 | 64, 93, 43, 100, 66 | ofrfval2 7628 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
102 | 99, 101 | mpbird 256 |
. . . . . . . . . 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 1371 |
. . . . . . . . 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 1371 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) β β) |
107 | | 0red 11091 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β 0 β
β) |
108 | | elinel2 4154 |
. . . . . . . . . . . . 13
β’ (π₯ β (π’ β© (β‘πΉ β (π(,)+β))) β π₯ β (β‘πΉ β (π(,)+β))) |
109 | 108 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (π’ β© (β‘πΉ β (π(,)+β))) β π₯ β (β‘πΉ β (π(,)+β)))) |
110 | | ifle 13044 |
. . . . . . . . . . . 12
β’ ((((πΉβπ₯) β β β§ 0 β β β§
0 β€ (πΉβπ₯)) β§ (π₯ β (π’ β© (β‘πΉ β (π(,)+β))) β π₯ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
111 | 39, 107, 41, 109, 110 | syl31anc 1373 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
112 | 111 | ralrimiva 3141 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
113 | 64, 50, 93, 65, 100 | ofrfval2 7628 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) β βπ₯ β β if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) |
114 | 112, 113 | mpbird 256 |
. . . . . . . . 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 1371 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)))) |
117 | 66 | fveq2d 6841 |
. . . . . . . . . . 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 4429 |
. . . . . . . . . . . . . . 15
β’ ((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β)))) = β
|
121 | 120 | fveq2i 6840 |
. . . . . . . . . . . . . 14
β’
(vol*β((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β))))) =
(vol*ββ
) |
122 | 121, 26 | eqtri 2765 |
. . . . . . . . . . . . 13
β’
(vol*β((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β))))) = 0 |
123 | 122 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*β((β‘πΉ β (π(,)+β)) β© (β β (β‘πΉ β (π(,)+β))))) = 0) |
124 | | undif2 4434 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β (π(,)+β)) βͺ (β β (β‘πΉ β (π(,)+β)))) = ((β‘πΉ β (π(,)+β)) βͺ
β) |
125 | | mblss 24817 |
. . . . . . . . . . . . . . 15
β’ ((β‘πΉ β (π(,)+β)) β dom vol β (β‘πΉ β (π(,)+β)) β
β) |
126 | 15, 125 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β‘πΉ β (π(,)+β)) β
β) |
127 | | ssequn1 4138 |
. . . . . . . . . . . . . 14
β’ ((β‘πΉ β (π(,)+β)) β β β ((β‘πΉ β (π(,)+β)) βͺ β) =
β) |
128 | 126, 127 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β‘πΉ β (π(,)+β)) βͺ β) =
β) |
129 | 124, 128 | eqtr2id 2790 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β β = ((β‘πΉ β (π(,)+β)) βͺ (β β (β‘πΉ β (π(,)+β))))) |
130 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0)) |
131 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) |
132 | | iftrue 4490 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β if(π₯ β β, (πΉβπ₯), 0) = (πΉβπ₯)) |
133 | 132 | mpteq2ia 5206 |
. . . . . . . . . . . . 13
β’ (π₯ β β β¦ if(π₯ β β, (πΉβπ₯), 0)) = (π₯ β β β¦ (πΉβπ₯)) |
134 | 133 | eqcomi 2746 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦ (πΉβπ₯)) = (π₯ β β β¦ if(π₯ β β, (πΉβπ₯), 0)) |
135 | | ifcl 4529 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
136 | 43, 48, 135 | sylancl 586 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0[,]+β)) |
137 | 136 | fmpttd 7057 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
138 | | breq1 5106 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ₯) = if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
139 | | breq1 5106 |
. . . . . . . . . . . . . . . . . 18
β’ (0 =
if(π₯ β (β
β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
140 | 138, 139 | ifboth 4523 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
141 | 57, 41, 140 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
142 | 141 | ralrimiva 3141 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯)) |
143 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) |
144 | 64, 136, 43, 143, 66 | ofrfval2 7628 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ (πΉβπ₯))) |
145 | 142, 144 | mpbird 256 |
. . . . . . . . . . . . . 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 1371 |
. . . . . . . . . . . . 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 1371 |
. . . . . . . . . . . 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 2777 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2βπΉ) =
((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
152 | | eldif 3918 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (β β (β‘πΉ β (π(,)+β))) β (π₯ β β β§ Β¬ π₯ β (β‘πΉ β (π(,)+β)))) |
153 | 152 | baib 536 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (π₯ β (β β (β‘πΉ β (π(,)+β))) β Β¬ π₯ β (β‘πΉ β (π(,)+β)))) |
154 | 153 | adantl 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (β β (β‘πΉ β (π(,)+β))) β Β¬ π₯ β (β‘πΉ β (π(,)+β)))) |
155 | 9 | ffnd 6664 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΉ Fn β) |
156 | 155 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β πΉ Fn β) |
157 | | elpreima 7003 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ Fn β β (π₯ β (β‘πΉ β (π(,)+β)) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (β‘πΉ β (π(,)+β)) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
159 | 39 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π < (πΉβπ₯) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
160 | 3 | nnred 12101 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β) |
161 | 160 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β π β β) |
162 | 161 | rexrd 11138 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β π β
β*) |
163 | | elioopnf 13288 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β*
β ((πΉβπ₯) β (π(,)+β) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β ((πΉβπ₯) β (π(,)+β) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
165 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β π₯ β β) |
166 | 165 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β ((πΉβπ₯) β (π(,)+β) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
167 | 159, 164,
166 | 3bitr2d 306 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π < (πΉβπ₯) β (π₯ β β β§ (πΉβπ₯) β (π(,)+β)))) |
168 | 161, 39 | ltnled 11235 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π < (πΉβπ₯) β Β¬ (πΉβπ₯) β€ π)) |
169 | 158, 167,
168 | 3bitr2rd 307 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (Β¬ (πΉβπ₯) β€ π β π₯ β (β‘πΉ β (π(,)+β)))) |
170 | 169 | con1bid 355 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (Β¬ π₯ β (β‘πΉ β (π(,)+β)) β (πΉβπ₯) β€ π)) |
171 | 154, 170 | bitrd 278 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β (π₯ β (β β (β‘πΉ β (π(,)+β))) β (πΉβπ₯) β€ π)) |
172 | 171 | ifbid 4507 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
173 | 172 | mpteq2dva 5203 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
174 | 173 | fveq2d 6841 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) = (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
175 | | itg2cn.6 |
. . . . . . . . . . . . . 14
β’ (π β Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
176 | 175 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
177 | 174, 176 | eqnbrtrd 5121 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β Β¬
(β«2β(π₯
β β β¦ if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
178 | 53, 91 | resubcld 11516 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2βπΉ) β (πΆ / 2)) β β) |
179 | 178, 149 | ltnled 11235 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (((β«2βπΉ) β (πΆ / 2)) < (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β Β¬
(β«2β(π₯
β β β¦ if(π₯
β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) |
180 | 177, 179 | mpbird 256 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2βπΉ) β (πΆ / 2)) < (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) |
181 | 53, 91, 149 | ltsubadd2d 11686 |
. . . . . . . . . . 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 5127 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) < ((πΆ / 2) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))))) |
184 | 106, 91, 149 | ltadd1d 11681 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) < (πΆ / 2) β
((β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) < ((πΆ / 2) + (β«2β(π₯ β β β¦ if(π₯ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))))) |
185 | 183, 184 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β (π(,)+β)), (πΉβπ₯), 0))) < (πΆ / 2)) |
186 | 72, 106, 91, 116, 185 | lelttrd 11246 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) < (πΆ / 2)) |
187 | 160 | adantr 481 |
. . . . . . . . 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 12885 |
. . . . . . . . . . . 12
β’ (π β ((πΆ / 2) / π) β β) |
191 | 190 | adantr 481 |
. . . . . . . . . . 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 11138 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((πΆ / 2) / π) β
β*) |
195 | | simprr 771 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (volβπ’) < ((πΆ / 2) / π)) |
196 | 189, 195 | eqbrtrrd 5127 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) < ((πΆ / 2) / π)) |
197 | 193, 194,
196 | xrltled 12997 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) β€ ((πΆ / 2) / π)) |
198 | | ovollecl 24769 |
. . . . . . . . . . 11
β’ ((π’ β β β§ ((πΆ / 2) / π) β β β§ (vol*βπ’) β€ ((πΆ / 2) / π)) β (vol*βπ’) β β) |
199 | 33, 191, 197, 198 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (vol*βπ’) β β) |
200 | 189, 199 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (volβπ’) β β) |
201 | 187, 200 | remulcld 11118 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π Β· (volβπ’)) β β) |
202 | 187 | rexrd 11138 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β
β*) |
203 | 3 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β β) |
204 | 203 | nnnn0d 12406 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β
β0) |
205 | 204 | nn0ge0d 12409 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β 0 β€ π) |
206 | | elxrge0 13302 |
. . . . . . . . . . . . . 14
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
207 | 202, 205,
206 | sylanbrc 583 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β (0[,]+β)) |
208 | | ifcl 4529 |
. . . . . . . . . . . . 13
β’ ((π β (0[,]+β) β§ 0
β (0[,]+β)) β if(π₯ β π’, π, 0) β (0[,]+β)) |
209 | 207, 48, 208 | sylancl 586 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β if(π₯ β π’, π, 0) β (0[,]+β)) |
210 | 209 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β β) β if(π₯ β π’, π, 0) β (0[,]+β)) |
211 | 210 | fmpttd 7057 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β π’, π,
0)):ββΆ(0[,]+β)) |
212 | | eldifn 4085 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π’ β (β‘πΉ β (π(,)+β))) β Β¬ π₯ β (β‘πΉ β (π(,)+β))) |
213 | 212 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β Β¬ π₯ β (β‘πΉ β (π(,)+β))) |
214 | | difssd 4090 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π’ β (β‘πΉ β (π(,)+β))) β π’) |
215 | 214 | sselda 3942 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β π₯ β π’) |
216 | 34, 169 | syldan 591 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β π’) β (Β¬ (πΉβπ₯) β€ π β π₯ β (β‘πΉ β (π(,)+β)))) |
217 | 215, 216 | syldan 591 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β (Β¬ (πΉβπ₯) β€ π β π₯ β (β‘πΉ β (π(,)+β)))) |
218 | 217 | con1bid 355 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β (Β¬ π₯ β (β‘πΉ β (π(,)+β)) β (πΉβπ₯) β€ π)) |
219 | 213, 218 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β (πΉβπ₯) β€ π) |
220 | | iftrue 4490 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π’ β (β‘πΉ β (π(,)+β))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = (πΉβπ₯)) |
221 | 220 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = (πΉβπ₯)) |
222 | 215 | iftrued 4492 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β π’, π, 0) = π) |
223 | 219, 221,
222 | 3brtr4d 5135 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
224 | | iffalse 4493 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π₯ β (π’ β (β‘πΉ β (π(,)+β))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = 0) |
225 | 224 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ Β¬ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) = 0) |
226 | | 0le0 12187 |
. . . . . . . . . . . . . . . 16
β’ 0 β€
0 |
227 | | breq2 5107 |
. . . . . . . . . . . . . . . . 17
β’ (π = if(π₯ β π’, π, 0) β (0 β€ π β 0 β€ if(π₯ β π’, π, 0))) |
228 | | breq2 5107 |
. . . . . . . . . . . . . . . . 17
β’ (0 =
if(π₯ β π’, π, 0) β (0 β€ 0 β 0 β€ if(π₯ β π’, π, 0))) |
229 | 227, 228 | ifboth 4523 |
. . . . . . . . . . . . . . . 16
β’ ((0 β€
π β§ 0 β€ 0) β 0
β€ if(π₯ β π’, π, 0)) |
230 | 205, 226,
229 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β 0 β€ if(π₯ β π’, π, 0)) |
231 | 230 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ Β¬ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β 0 β€ if(π₯ β π’, π, 0)) |
232 | 225, 231 | eqbrtrd 5125 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β§ Β¬ π₯ β (π’ β (β‘πΉ β (π(,)+β)))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
233 | 223, 232 | pm2.61dan 811 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
234 | 233 | ralrimivw 3145 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0)) |
235 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π₯ β β β¦ if(π₯ β π’, π, 0)) = (π₯ β β β¦ if(π₯ β π’, π, 0))) |
236 | 64, 74, 210, 81, 235 | ofrfval2 7628 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)) βr β€ (π₯ β β β¦ if(π₯ β π’, π, 0)) β βπ₯ β β if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0) β€ if(π₯ β π’, π, 0))) |
237 | 234, 236 | mpbird 256 |
. . . . . . . . . 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 1371 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0)))) |
240 | | elrege0 13299 |
. . . . . . . . . . 11
β’ (π β (0[,)+β) β
(π β β β§ 0
β€ π)) |
241 | 187, 205,
240 | sylanbrc 583 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β π β (0[,)+β)) |
242 | | itg2const 25027 |
. . . . . . . . . 10
β’ ((π’ β dom vol β§
(volβπ’) β
β β§ π β
(0[,)+β)) β (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0))) = (π Β· (volβπ’))) |
243 | 6, 200, 241, 242 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, π, 0))) = (π Β· (volβπ’))) |
244 | 239, 243 | breqtrd 5129 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) β€ (π Β· (volβπ’))) |
245 | 203 | nngt0d 12135 |
. . . . . . . . . 10
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β 0 < π) |
246 | | ltmuldiv2 11962 |
. . . . . . . . . 10
β’
(((volβπ’)
β β β§ (πΆ /
2) β β β§ (π
β β β§ 0 < π)) β ((π Β· (volβπ’)) < (πΆ / 2) β (volβπ’) < ((πΆ / 2) / π))) |
247 | 200, 91, 187, 245, 246 | syl112anc 1374 |
. . . . . . . . 9
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((π Β· (volβπ’)) < (πΆ / 2) β (volβπ’) < ((πΆ / 2) / π))) |
248 | 195, 247 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (π Β· (volβπ’)) < (πΆ / 2)) |
249 | 87, 201, 91, 244, 248 | lelttrd 11246 |
. . . . . . 7
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) < (πΆ / 2)) |
250 | 72, 87, 91, 91, 186, 249 | lt2addd 11711 |
. . . . . 6
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((β«2β(π₯ β β β¦ if(π₯ β (π’ β© (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0))) + (β«2β(π₯ β β β¦ if(π₯ β (π’ β (β‘πΉ β (π(,)+β))), (πΉβπ₯), 0)))) < ((πΆ / 2) + (πΆ / 2))) |
251 | 88, 250 | eqbrtrd 5125 |
. . . . 5
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < ((πΆ / 2) + (πΆ / 2))) |
252 | 89 | rpcnd 12887 |
. . . . . 6
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β πΆ β β) |
253 | 252 | 2halvesd 12332 |
. . . . 5
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β ((πΆ / 2) + (πΆ / 2)) = πΆ) |
254 | 251, 253 | breqtrd 5129 |
. . . 4
β’ ((π β§ (π’ β dom vol β§ (volβπ’) < ((πΆ / 2) / π))) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ) |
255 | 254 | expr 457 |
. . 3
β’ ((π β§ π’ β dom vol) β ((volβπ’) < ((πΆ / 2) / π) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
256 | 255 | ralrimiva 3141 |
. 2
β’ (π β βπ’ β dom vol((volβπ’) < ((πΆ / 2) / π) β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
257 | | breq2 5107 |
. . 3
β’ (π = ((πΆ / 2) / π) β ((volβπ’) < π β (volβπ’) < ((πΆ / 2) / π))) |
258 | 257 | rspceaimv 3583 |
. 2
β’ ((((πΆ / 2) / π) β β+ β§
βπ’ β dom
vol((volβπ’) <
((πΆ / 2) / π) β
(β«2β(π₯
β β β¦ if(π₯
β π’, (πΉβπ₯), 0))) < πΆ)) β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
259 | 5, 256, 258 | syl2anc 584 |
1
β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |