Step | Hyp | Ref
| Expression |
1 | | itg2lea.2 |
. . . . . 6
β’ (π β πΊ:ββΆ(0[,]+β)) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β πΊ:ββΆ(0[,]+β)) |
3 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β π β dom
β«1) |
4 | | itg2lea.3 |
. . . . . 6
β’ (π β π΄ β β) |
5 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β π΄ β β) |
6 | | itg2lea.4 |
. . . . . 6
β’ (π β (vol*βπ΄) = 0) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β (vol*βπ΄) = 0) |
8 | | i1ff 25056 |
. . . . . . . . 9
β’ (π β dom β«1
β π:ββΆβ) |
9 | 8 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β π:ββΆβ) |
10 | | eldifi 4087 |
. . . . . . . 8
β’ (π₯ β (β β π΄) β π₯ β β) |
11 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((π:ββΆβ β§
π₯ β β) β
(πβπ₯) β β) |
12 | 9, 10, 11 | syl2an 597 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πβπ₯) β β) |
13 | 12 | rexrd 11210 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πβπ₯) β
β*) |
14 | | iccssxr 13353 |
. . . . . . 7
β’
(0[,]+β) β β* |
15 | | itg2lea.1 |
. . . . . . . . 9
β’ (π β πΉ:ββΆ(0[,]+β)) |
16 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β πΉ:ββΆ(0[,]+β)) |
17 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΉ:ββΆ(0[,]+β)
β§ π₯ β β)
β (πΉβπ₯) β
(0[,]+β)) |
18 | 16, 10, 17 | syl2an 597 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πΉβπ₯) β (0[,]+β)) |
19 | 14, 18 | sselid 3943 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πΉβπ₯) β
β*) |
20 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΊ:ββΆ(0[,]+β)
β§ π₯ β β)
β (πΊβπ₯) β
(0[,]+β)) |
21 | 2, 10, 20 | syl2an 597 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πΊβπ₯) β (0[,]+β)) |
22 | 14, 21 | sselid 3943 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πΊβπ₯) β
β*) |
23 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β π βr β€ πΉ) |
24 | 9 | ffnd 6670 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β π Fn β) |
25 | 16 | ffnd 6670 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β πΉ Fn β) |
26 | | reex 11147 |
. . . . . . . . . . 11
β’ β
β V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β β β
V) |
28 | | inidm 4179 |
. . . . . . . . . 10
β’ (β
β© β) = β |
29 | | eqidd 2734 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β β) β (πβπ₯) = (πβπ₯)) |
30 | | eqidd 2734 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β β) β (πΉβπ₯) = (πΉβπ₯)) |
31 | 24, 25, 27, 27, 28, 29, 30 | ofrfval 7628 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β (π βr β€ πΉ β βπ₯ β β (πβπ₯) β€ (πΉβπ₯))) |
32 | 23, 31 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β βπ₯ β β (πβπ₯) β€ (πΉβπ₯)) |
33 | 32 | r19.21bi 3233 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β β) β (πβπ₯) β€ (πΉβπ₯)) |
34 | 10, 33 | sylan2 594 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πβπ₯) β€ (πΉβπ₯)) |
35 | | itg2lea.5 |
. . . . . . 7
β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) β€ (πΊβπ₯)) |
36 | 35 | adantlr 714 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πΉβπ₯) β€ (πΊβπ₯)) |
37 | 13, 19, 22, 34, 36 | xrletrd 13087 |
. . . . 5
β’ (((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β§ π₯ β (β β π΄)) β (πβπ₯) β€ (πΊβπ₯)) |
38 | 2, 3, 5, 7, 37 | itg2uba 25124 |
. . . 4
β’ ((π β§ (π β dom β«1 β§ π βr β€ πΉ)) β
(β«1βπ)
β€ (β«2βπΊ)) |
39 | 38 | expr 458 |
. . 3
β’ ((π β§ π β dom β«1) β (π βr β€ πΉ β
(β«1βπ)
β€ (β«2βπΊ))) |
40 | 39 | ralrimiva 3140 |
. 2
β’ (π β βπ β dom β«1(π βr β€ πΉ β
(β«1βπ)
β€ (β«2βπΊ))) |
41 | | itg2cl 25113 |
. . . 4
β’ (πΊ:ββΆ(0[,]+β)
β (β«2βπΊ) β
β*) |
42 | 1, 41 | syl 17 |
. . 3
β’ (π β
(β«2βπΊ)
β β*) |
43 | | itg2leub 25115 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ (β«2βπΊ) β β*) β
((β«2βπΉ) β€ (β«2βπΊ) β βπ β dom
β«1(π
βr β€ πΉ
β (β«1βπ) β€ (β«2βπΊ)))) |
44 | 15, 42, 43 | syl2anc 585 |
. 2
β’ (π β
((β«2βπΉ) β€ (β«2βπΊ) β βπ β dom
β«1(π
βr β€ πΉ
β (β«1βπ) β€ (β«2βπΊ)))) |
45 | 40, 44 | mpbird 257 |
1
β’ (π β
(β«2βπΉ)
β€ (β«2βπΊ)) |