Step | Hyp | Ref
| Expression |
1 | | itg10a.1 |
. . . . 5
β’ (π β πΉ β dom
β«1) |
2 | | i1frn 25057 |
. . . . 5
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β ran πΉ β Fin) |
4 | | difss 4096 |
. . . 4
β’ (ran
πΉ β {0}) β ran
πΉ |
5 | | ssfi 9124 |
. . . 4
β’ ((ran
πΉ β Fin β§ (ran
πΉ β {0}) β ran
πΉ) β (ran πΉ β {0}) β
Fin) |
6 | 3, 4, 5 | sylancl 587 |
. . 3
β’ (π β (ran πΉ β {0}) β Fin) |
7 | | i1ff 25056 |
. . . . . . . 8
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
8 | 1, 7 | syl 17 |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
9 | 8 | frnd 6681 |
. . . . . 6
β’ (π β ran πΉ β β) |
10 | 9 | ssdifssd 4107 |
. . . . 5
β’ (π β (ran πΉ β {0}) β
β) |
11 | 10 | sselda 3949 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β π β β) |
12 | | i1fima2sn 25060 |
. . . . 5
β’ ((πΉ β dom β«1
β§ π β (ran πΉ β {0})) β
(volβ(β‘πΉ β {π})) β β) |
13 | 1, 12 | sylan 581 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) β β) |
14 | 11, 13 | remulcld 11192 |
. . 3
β’ ((π β§ π β (ran πΉ β {0})) β (π Β· (volβ(β‘πΉ β {π}))) β β) |
15 | | 0le0 12261 |
. . . . 5
β’ 0 β€
0 |
16 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (β‘πΉ β {π}) β dom vol) |
17 | 1, 16 | syl 17 |
. . . . . . . . . 10
β’ (π β (β‘πΉ β {π}) β dom vol) |
18 | | mblvol 24910 |
. . . . . . . . . 10
β’ ((β‘πΉ β {π}) β dom vol β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (π β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
20 | 19 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
21 | 8 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn β) |
22 | | fniniseg 7015 |
. . . . . . . . . . . . 13
β’ (πΉ Fn β β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
25 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β π₯ β β) |
26 | | eldif 3925 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (β β π΄) β (π₯ β β β§ Β¬ π₯ β π΄)) |
27 | | itg1ge0a.4 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (β β π΄)) β 0 β€ (πΉβπ₯)) |
28 | 27 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π₯ β (β β π΄) β 0 β€ (πΉβπ₯))) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (π₯ β (β β π΄) β 0 β€ (πΉβπ₯))) |
30 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (πΉβπ₯) = π) |
31 | 30 | breq2d 5122 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (0 β€ (πΉβπ₯) β 0 β€ π)) |
32 | | 0red 11165 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β 0 β β) |
33 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β π β β) |
34 | 32, 33 | lenltd 11308 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (0 β€ π β Β¬ π < 0)) |
35 | 31, 34 | bitrd 279 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (0 β€ (πΉβπ₯) β Β¬ π < 0)) |
36 | 29, 35 | sylibd 238 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (π₯ β (β β π΄) β Β¬ π < 0)) |
37 | 26, 36 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β ((π₯ β β β§ Β¬ π₯ β π΄) β Β¬ π < 0)) |
38 | 25, 37 | mpand 694 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (Β¬ π₯ β π΄ β Β¬ π < 0)) |
39 | 38 | con4d 115 |
. . . . . . . . . . . 12
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (π < 0 β π₯ β π΄)) |
40 | 39 | impancom 453 |
. . . . . . . . . . 11
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β ((π₯ β β β§ (πΉβπ₯) = π) β π₯ β π΄)) |
41 | 24, 40 | sylbid 239 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (π₯ β (β‘πΉ β {π}) β π₯ β π΄)) |
42 | 41 | ssrdv 3955 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (β‘πΉ β {π}) β π΄) |
43 | | itg10a.2 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
44 | 43 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β π΄ β β) |
45 | | itg10a.3 |
. . . . . . . . . 10
β’ (π β (vol*βπ΄) = 0) |
46 | 45 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (vol*βπ΄) = 0) |
47 | | ovolssnul 24867 |
. . . . . . . . 9
β’ (((β‘πΉ β {π}) β π΄ β§ π΄ β β β§ (vol*βπ΄) = 0) β (vol*β(β‘πΉ β {π})) = 0) |
48 | 42, 44, 46, 47 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (vol*β(β‘πΉ β {π})) = 0) |
49 | 20, 48 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (volβ(β‘πΉ β {π})) = 0) |
50 | 49 | oveq2d 7378 |
. . . . . 6
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (π Β· (volβ(β‘πΉ β {π}))) = (π Β· 0)) |
51 | 11 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β π β β) |
52 | 51 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β π β β) |
53 | 52 | mul01d 11361 |
. . . . . 6
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (π Β· 0) = 0) |
54 | 50, 53 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β (π Β· (volβ(β‘πΉ β {π}))) = 0) |
55 | 15, 54 | breqtrrid 5148 |
. . . 4
β’ (((π β§ π β (ran πΉ β {0})) β§ π < 0) β 0 β€ (π Β· (volβ(β‘πΉ β {π})))) |
56 | 11 | adantr 482 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β π β β) |
57 | 13 | adantr 482 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β (volβ(β‘πΉ β {π})) β β) |
58 | | simpr 486 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β 0 β€ π) |
59 | 17 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β (β‘πΉ β {π}) β dom vol) |
60 | | mblss 24911 |
. . . . . . . 8
β’ ((β‘πΉ β {π}) β dom vol β (β‘πΉ β {π}) β β) |
61 | 59, 60 | syl 17 |
. . . . . . 7
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β (β‘πΉ β {π}) β β) |
62 | | ovolge0 24861 |
. . . . . . 7
β’ ((β‘πΉ β {π}) β β β 0 β€
(vol*β(β‘πΉ β {π}))) |
63 | 61, 62 | syl 17 |
. . . . . 6
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β 0 β€
(vol*β(β‘πΉ β {π}))) |
64 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
65 | 63, 64 | breqtrrd 5138 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β 0 β€
(volβ(β‘πΉ β {π}))) |
66 | 56, 57, 58, 65 | mulge0d 11739 |
. . . 4
β’ (((π β§ π β (ran πΉ β {0})) β§ 0 β€ π) β 0 β€ (π Β· (volβ(β‘πΉ β {π})))) |
67 | | 0red 11165 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β 0 β
β) |
68 | 55, 66, 11, 67 | ltlecasei 11270 |
. . 3
β’ ((π β§ π β (ran πΉ β {0})) β 0 β€ (π Β· (volβ(β‘πΉ β {π})))) |
69 | 6, 14, 68 | fsumge0 15687 |
. 2
β’ (π β 0 β€ Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
70 | | itg1val 25063 |
. . 3
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
71 | 1, 70 | syl 17 |
. 2
β’ (π β
(β«1βπΉ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
72 | 69, 71 | breqtrrd 5138 |
1
β’ (π β 0 β€
(β«1βπΉ)) |