Step | Hyp | Ref
| Expression |
1 | | itg2cn.3 |
. . . . . 6
β’ (π β
(β«2βπΉ)
β β) |
2 | | itg2cn.4 |
. . . . . . 7
β’ (π β πΆ β
β+) |
3 | 2 | rphalfcld 12898 |
. . . . . 6
β’ (π β (πΆ / 2) β
β+) |
4 | 1, 3 | ltsubrpd 12918 |
. . . . 5
β’ (π β
((β«2βπΉ) β (πΆ / 2)) < (β«2βπΉ)) |
5 | 3 | rpred 12886 |
. . . . . . 7
β’ (π β (πΆ / 2) β β) |
6 | 1, 5 | resubcld 11517 |
. . . . . 6
β’ (π β
((β«2βπΉ) β (πΆ / 2)) β β) |
7 | 6, 1 | ltnled 11236 |
. . . . 5
β’ (π β
(((β«2βπΉ) β (πΆ / 2)) < (β«2βπΉ) β Β¬
(β«2βπΉ)
β€ ((β«2βπΉ) β (πΆ / 2)))) |
8 | 4, 7 | mpbid 231 |
. . . 4
β’ (π β Β¬
(β«2βπΉ)
β€ ((β«2βπΉ) β (πΆ / 2))) |
9 | | itg2cn.1 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:ββΆ(0[,)+β)) |
10 | 9 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β (πΉβπ₯) β (0[,)+β)) |
11 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
12 | 10, 11 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
13 | 12 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
14 | 13 | rexrd 11139 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (πΉβπ₯) β
β*) |
15 | 12 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
16 | | elxrge0 13303 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) β (0[,]+β) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯))) |
17 | 14, 15, 16 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (πΉβπ₯) β (0[,]+β)) |
18 | | 0e0iccpnf 13305 |
. . . . . . . . . . . 12
β’ 0 β
(0[,]+β) |
19 | | ifcl 4530 |
. . . . . . . . . . . 12
β’ (((πΉβπ₯) β (0[,]+β) β§ 0 β
(0[,]+β)) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0[,]+β)) |
20 | 17, 18, 19 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0[,]+β)) |
21 | 20 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0[,]+β)) |
22 | 21 | fmpttd 7058 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯),
0)):ββΆ(0[,]+β)) |
23 | | itg2cl 25019 |
. . . . . . . . 9
β’ ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)):ββΆ(0[,]+β) β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β
β*) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β
β*) |
25 | 24 | fmpttd 7058 |
. . . . . . 7
β’ (π β (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯),
0)))):ββΆβ*) |
26 | 25 | frnd 6672 |
. . . . . 6
β’ (π β ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) β
β*) |
27 | 6 | rexrd 11139 |
. . . . . 6
β’ (π β
((β«2βπΉ) β (πΆ / 2)) β
β*) |
28 | | supxrleub 13174 |
. . . . . 6
β’ ((ran
(π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) β β* β§
((β«2βπΉ) β (πΆ / 2)) β β*) β
(sup(ran (π β β
β¦ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) β€
((β«2βπΉ) β (πΆ / 2)) β βπ§ β ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))π§ β€ ((β«2βπΉ) β (πΆ / 2)))) |
29 | 26, 27, 28 | syl2anc 585 |
. . . . 5
β’ (π β (sup(ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) β€
((β«2βπΉ) β (πΆ / 2)) β βπ§ β ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))π§ β€ ((β«2βπΉ) β (πΆ / 2)))) |
30 | | itg2cn.2 |
. . . . . . 7
β’ (π β πΉ β MblFn) |
31 | 9, 30, 1 | itg2cnlem1 25048 |
. . . . . 6
β’ (π β sup(ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) =
(β«2βπΉ)) |
32 | 31 | breq1d 5114 |
. . . . 5
β’ (π β (sup(ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) β€
((β«2βπΉ) β (πΆ / 2)) β (β«2βπΉ) β€
((β«2βπΉ) β (πΆ / 2)))) |
33 | 25 | ffnd 6665 |
. . . . . 6
β’ (π β (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) Fn β) |
34 | | breq1 5107 |
. . . . . . . 8
β’ (π§ = ((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))βπ) β (π§ β€ ((β«2βπΉ) β (πΆ / 2)) β ((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))βπ) β€ ((β«2βπΉ) β (πΆ / 2)))) |
35 | 34 | ralrn 7033 |
. . . . . . 7
β’ ((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) Fn β β (βπ§ β ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))π§ β€ ((β«2βπΉ) β (πΆ / 2)) β βπ β β ((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))βπ) β€ ((β«2βπΉ) β (πΆ / 2)))) |
36 | | breq2 5108 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ₯) β€ π β (πΉβπ₯) β€ π)) |
37 | 36 | ifbid 4508 |
. . . . . . . . . . . 12
β’ (π = π β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
38 | 37 | mpteq2dv 5206 |
. . . . . . . . . . 11
β’ (π = π β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
39 | 38 | fveq2d 6842 |
. . . . . . . . . 10
β’ (π = π β (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) = (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
40 | | eqid 2738 |
. . . . . . . . . 10
β’ (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) = (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
41 | | fvex 6851 |
. . . . . . . . . 10
β’
(β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β V |
42 | 39, 40, 41 | fvmpt 6944 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))βπ) = (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
43 | 42 | breq1d 5114 |
. . . . . . . 8
β’ (π β β β (((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))βπ) β€ ((β«2βπΉ) β (πΆ / 2)) β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) |
44 | 43 | ralbiia 3093 |
. . . . . . 7
β’
(βπ β
β ((π β β
β¦ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))βπ) β€ ((β«2βπΉ) β (πΆ / 2)) β βπ β β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
45 | 35, 44 | bitrdi 287 |
. . . . . 6
β’ ((π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) Fn β β (βπ§ β ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))π§ β€ ((β«2βπΉ) β (πΆ / 2)) β βπ β β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) |
46 | 33, 45 | syl 17 |
. . . . 5
β’ (π β (βπ§ β ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))))π§ β€ ((β«2βπΉ) β (πΆ / 2)) β βπ β β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) |
47 | 29, 32, 46 | 3bitr3d 309 |
. . . 4
β’ (π β
((β«2βπΉ) β€ ((β«2βπΉ) β (πΆ / 2)) β βπ β β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) |
48 | 8, 47 | mtbid 324 |
. . 3
β’ (π β Β¬ βπ β β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
49 | | rexnal 3102 |
. . 3
β’
(βπ β
β Β¬ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)) β Β¬ βπ β β
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
50 | 48, 49 | sylibr 233 |
. 2
β’ (π β βπ β β Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
51 | 9 | adantr 482 |
. . . 4
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β πΉ:ββΆ(0[,)+β)) |
52 | 30 | adantr 482 |
. . . 4
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β πΉ β MblFn) |
53 | 1 | adantr 482 |
. . . 4
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β
(β«2βπΉ)
β β) |
54 | 2 | adantr 482 |
. . . 4
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β πΆ β
β+) |
55 | | simprl 770 |
. . . 4
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β π β β) |
56 | | simprr 772 |
. . . . 5
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
57 | | fveq2 6838 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
58 | 57 | breq1d 5114 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((πΉβπ₯) β€ π β (πΉβπ¦) β€ π)) |
59 | 58, 57 | ifbieq1d 4509 |
. . . . . . . 8
β’ (π₯ = π¦ β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = if((πΉβπ¦) β€ π, (πΉβπ¦), 0)) |
60 | 59 | cbvmptv 5217 |
. . . . . . 7
β’ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π¦ β β β¦ if((πΉβπ¦) β€ π, (πΉβπ¦), 0)) |
61 | 60 | fveq2i 6841 |
. . . . . 6
β’
(β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) = (β«2β(π¦ β β β¦
if((πΉβπ¦) β€ π, (πΉβπ¦), 0))) |
62 | 61 | breq1i 5111 |
. . . . 5
β’
((β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)) β
(β«2β(π¦
β β β¦ if((πΉβπ¦) β€ π, (πΉβπ¦), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
63 | 56, 62 | sylnib 328 |
. . . 4
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β Β¬
(β«2β(π¦
β β β¦ if((πΉβπ¦) β€ π, (πΉβπ¦), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) |
64 | 51, 52, 53, 54, 55, 63 | itg2cnlem2 25049 |
. . 3
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0))) < πΆ)) |
65 | | elequ1 2114 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π₯ β π’ β π¦ β π’)) |
66 | 65, 57 | ifbieq1d 4509 |
. . . . . . . . 9
β’ (π₯ = π¦ β if(π₯ β π’, (πΉβπ₯), 0) = if(π¦ β π’, (πΉβπ¦), 0)) |
67 | 66 | cbvmptv 5217 |
. . . . . . . 8
β’ (π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0)) = (π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0)) |
68 | 67 | fveq2i 6841 |
. . . . . . 7
β’
(β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) = (β«2β(π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0))) |
69 | 68 | breq1i 5111 |
. . . . . 6
β’
((β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ β (β«2β(π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0))) < πΆ) |
70 | 69 | imbi2i 336 |
. . . . 5
β’
(((volβπ’) <
π β
(β«2β(π₯
β β β¦ if(π₯
β π’, (πΉβπ₯), 0))) < πΆ) β ((volβπ’) < π β (β«2β(π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0))) < πΆ)) |
71 | 70 | ralbii 3095 |
. . . 4
β’
(βπ’ β
dom vol((volβπ’) <
π β
(β«2β(π₯
β β β¦ if(π₯
β π’, (πΉβπ₯), 0))) < πΆ) β βπ’ β dom vol((volβπ’) < π β (β«2β(π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0))) < πΆ)) |
72 | 71 | rexbii 3096 |
. . 3
β’
(βπ β
β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ) β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π¦ β β β¦ if(π¦ β π’, (πΉβπ¦), 0))) < πΆ)) |
73 | 64, 72 | sylibr 233 |
. 2
β’ ((π β§ (π β β β§ Β¬
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2)))) β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |
74 | 50, 73 | rexlimddv 3157 |
1
β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) |