Step | Hyp | Ref
| Expression |
1 | | itg2uba.2 |
. . . 4
β’ (π β πΊ β dom
β«1) |
2 | | itg1cl 24971 |
. . . 4
β’ (πΊ β dom β«1
β (β«1βπΊ) β β) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β
(β«1βπΊ)
β β) |
4 | 3 | rexrd 11139 |
. 2
β’ (π β
(β«1βπΊ)
β β*) |
5 | | itg2uba.3 |
. . . . . . 7
β’ (π β π΄ β β) |
6 | | itg2uba.4 |
. . . . . . 7
β’ (π β (vol*βπ΄) = 0) |
7 | | nulmbl 24821 |
. . . . . . 7
β’ ((π΄ β β β§
(vol*βπ΄) = 0) β
π΄ β dom
vol) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . . 6
β’ (π β π΄ β dom vol) |
9 | | cmmbl 24820 |
. . . . . 6
β’ (π΄ β dom vol β (β
β π΄) β dom
vol) |
10 | 8, 9 | syl 17 |
. . . . 5
β’ (π β (β β π΄) β dom
vol) |
11 | | ifnot 4537 |
. . . . . . . 8
β’ if(Β¬
π₯ β π΄, (πΊβπ₯), 0) = if(π₯ β π΄, 0, (πΊβπ₯)) |
12 | | eldif 3919 |
. . . . . . . . . 10
β’ (π₯ β (β β π΄) β (π₯ β β β§ Β¬ π₯ β π΄)) |
13 | 12 | baibr 538 |
. . . . . . . . 9
β’ (π₯ β β β (Β¬
π₯ β π΄ β π₯ β (β β π΄))) |
14 | 13 | ifbid 4508 |
. . . . . . . 8
β’ (π₯ β β β if(Β¬
π₯ β π΄, (πΊβπ₯), 0) = if(π₯ β (β β π΄), (πΊβπ₯), 0)) |
15 | 11, 14 | eqtr3id 2792 |
. . . . . . 7
β’ (π₯ β β β if(π₯ β π΄, 0, (πΊβπ₯)) = if(π₯ β (β β π΄), (πΊβπ₯), 0)) |
16 | 15 | mpteq2ia 5207 |
. . . . . 6
β’ (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) = (π₯ β β β¦ if(π₯ β (β β π΄), (πΊβπ₯), 0)) |
17 | 16 | i1fres 24992 |
. . . . 5
β’ ((πΊ β dom β«1
β§ (β β π΄)
β dom vol) β (π₯
β β β¦ if(π₯
β π΄, 0, (πΊβπ₯))) β dom
β«1) |
18 | 1, 10, 17 | syl2anc 585 |
. . . 4
β’ (π β (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) β dom
β«1) |
19 | | itg1cl 24971 |
. . . 4
β’ ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) β dom β«1 β
(β«1β(π₯
β β β¦ if(π₯
β π΄, 0, (πΊβπ₯)))) β β) |
20 | 18, 19 | syl 17 |
. . 3
β’ (π β
(β«1β(π₯
β β β¦ if(π₯
β π΄, 0, (πΊβπ₯)))) β β) |
21 | 20 | rexrd 11139 |
. 2
β’ (π β
(β«1β(π₯
β β β¦ if(π₯
β π΄, 0, (πΊβπ₯)))) β
β*) |
22 | | itg2uba.1 |
. . 3
β’ (π β πΉ:ββΆ(0[,]+β)) |
23 | | itg2cl 25019 |
. . 3
β’ (πΉ:ββΆ(0[,]+β)
β (β«2βπΉ) β
β*) |
24 | 22, 23 | syl 17 |
. 2
β’ (π β
(β«2βπΉ)
β β*) |
25 | | i1ff 24962 |
. . . . . . 7
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
26 | 1, 25 | syl 17 |
. . . . . 6
β’ (π β πΊ:ββΆβ) |
27 | | eldifi 4085 |
. . . . . 6
β’ (π¦ β (β β π΄) β π¦ β β) |
28 | | ffvelcdm 7028 |
. . . . . 6
β’ ((πΊ:ββΆβ β§
π¦ β β) β
(πΊβπ¦) β β) |
29 | 26, 27, 28 | syl2an 597 |
. . . . 5
β’ ((π β§ π¦ β (β β π΄)) β (πΊβπ¦) β β) |
30 | 29 | leidd 11655 |
. . . 4
β’ ((π β§ π¦ β (β β π΄)) β (πΊβπ¦) β€ (πΊβπ¦)) |
31 | | eldif 3919 |
. . . . . 6
β’ (π¦ β (β β π΄) β (π¦ β β β§ Β¬ π¦ β π΄)) |
32 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ β π΄ β π¦ β π΄)) |
33 | | fveq2 6838 |
. . . . . . . . 9
β’ (π₯ = π¦ β (πΊβπ₯) = (πΊβπ¦)) |
34 | 32, 33 | ifbieq2d 4511 |
. . . . . . . 8
β’ (π₯ = π¦ β if(π₯ β π΄, 0, (πΊβπ₯)) = if(π¦ β π΄, 0, (πΊβπ¦))) |
35 | | eqid 2738 |
. . . . . . . 8
β’ (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) = (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) |
36 | | c0ex 11083 |
. . . . . . . . 9
β’ 0 β
V |
37 | | fvex 6851 |
. . . . . . . . 9
β’ (πΊβπ¦) β V |
38 | 36, 37 | ifex 4535 |
. . . . . . . 8
β’ if(π¦ β π΄, 0, (πΊβπ¦)) β V |
39 | 34, 35, 38 | fvmpt 6944 |
. . . . . . 7
β’ (π¦ β β β ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯)))βπ¦) = if(π¦ β π΄, 0, (πΊβπ¦))) |
40 | | iffalse 4494 |
. . . . . . 7
β’ (Β¬
π¦ β π΄ β if(π¦ β π΄, 0, (πΊβπ¦)) = (πΊβπ¦)) |
41 | 39, 40 | sylan9eq 2798 |
. . . . . 6
β’ ((π¦ β β β§ Β¬
π¦ β π΄) β ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯)))βπ¦) = (πΊβπ¦)) |
42 | 31, 41 | sylbi 216 |
. . . . 5
β’ (π¦ β (β β π΄) β ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯)))βπ¦) = (πΊβπ¦)) |
43 | 42 | adantl 483 |
. . . 4
β’ ((π β§ π¦ β (β β π΄)) β ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯)))βπ¦) = (πΊβπ¦)) |
44 | 30, 43 | breqtrrd 5132 |
. . 3
β’ ((π β§ π¦ β (β β π΄)) β (πΊβπ¦) β€ ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯)))βπ¦)) |
45 | 1, 5, 6, 18, 44 | itg1lea 24999 |
. 2
β’ (π β
(β«1βπΊ)
β€ (β«1β(π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))))) |
46 | | iftrue 4491 |
. . . . . . . 8
β’ (π₯ β π΄ β if(π₯ β π΄, 0, (πΊβπ₯)) = 0) |
47 | 46 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β if(π₯ β π΄, 0, (πΊβπ₯)) = 0) |
48 | 22 | ffvelcdmda 7030 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (πΉβπ₯) β (0[,]+β)) |
49 | | elxrge0 13303 |
. . . . . . . . . 10
β’ ((πΉβπ₯) β (0[,]+β) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯))) |
51 | 50 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
52 | 51 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β 0 β€ (πΉβπ₯)) |
53 | 47, 52 | eqbrtrd 5126 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ π₯ β π΄) β if(π₯ β π΄, 0, (πΊβπ₯)) β€ (πΉβπ₯)) |
54 | | iffalse 4494 |
. . . . . . . 8
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, 0, (πΊβπ₯)) = (πΊβπ₯)) |
55 | 54 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΄) β if(π₯ β π΄, 0, (πΊβπ₯)) = (πΊβπ₯)) |
56 | | itg2uba.5 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β β π΄)) β (πΊβπ₯) β€ (πΉβπ₯)) |
57 | 12, 56 | sylan2br 596 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ Β¬ π₯ β π΄)) β (πΊβπ₯) β€ (πΉβπ₯)) |
58 | 57 | anassrs 469 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΄) β (πΊβπ₯) β€ (πΉβπ₯)) |
59 | 55, 58 | eqbrtrd 5126 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β π΄) β if(π₯ β π΄, 0, (πΊβπ₯)) β€ (πΉβπ₯)) |
60 | 53, 59 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π₯ β β) β if(π₯ β π΄, 0, (πΊβπ₯)) β€ (πΉβπ₯)) |
61 | 60 | ralrimiva 3142 |
. . . 4
β’ (π β βπ₯ β β if(π₯ β π΄, 0, (πΊβπ₯)) β€ (πΉβπ₯)) |
62 | | reex 11076 |
. . . . . 6
β’ β
β V |
63 | 62 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
64 | | fvex 6851 |
. . . . . . 7
β’ (πΊβπ₯) β V |
65 | 36, 64 | ifex 4535 |
. . . . . 6
β’ if(π₯ β π΄, 0, (πΊβπ₯)) β V |
66 | 65 | a1i 11 |
. . . . 5
β’ ((π β§ π₯ β β) β if(π₯ β π΄, 0, (πΊβπ₯)) β V) |
67 | | fvexd 6853 |
. . . . 5
β’ ((π β§ π₯ β β) β (πΉβπ₯) β V) |
68 | | eqidd 2739 |
. . . . 5
β’ (π β (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) = (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯)))) |
69 | 22 | feqmptd 6906 |
. . . . 5
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
70 | 63, 66, 67, 68, 69 | ofrfval2 7629 |
. . . 4
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) βr β€ πΉ β βπ₯ β β if(π₯ β π΄, 0, (πΊβπ₯)) β€ (πΉβπ₯))) |
71 | 61, 70 | mpbird 257 |
. . 3
β’ (π β (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) βr β€ πΉ) |
72 | | itg2ub 25020 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ (π₯ β β
β¦ if(π₯ β π΄, 0, (πΊβπ₯))) β dom β«1 β§ (π₯ β β β¦ if(π₯ β π΄, 0, (πΊβπ₯))) βr β€ πΉ) β
(β«1β(π₯
β β β¦ if(π₯
β π΄, 0, (πΊβπ₯)))) β€ (β«2βπΉ)) |
73 | 22, 18, 71, 72 | syl3anc 1372 |
. 2
β’ (π β
(β«1β(π₯
β β β¦ if(π₯
β π΄, 0, (πΊβπ₯)))) β€ (β«2βπΉ)) |
74 | 4, 21, 24, 45, 73 | xrletrd 13010 |
1
β’ (π β
(β«1βπΊ)
β€ (β«2βπΉ)) |