Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . 4
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β π΄ β Fin) |
2 | | simpl2 1192 |
. . . . 5
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β βπ β π΄ π΅ β dom vol) |
3 | | simpr 485 |
. . . . 5
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β βπ β π΄ (volβπ΅) β β) |
4 | | r19.26 3111 |
. . . . 5
β’
(βπ β
π΄ (π΅ β dom vol β§ (volβπ΅) β β) β
(βπ β π΄ π΅ β dom vol β§ βπ β π΄ (volβπ΅) β β)) |
5 | 2, 3, 4 | sylanbrc 583 |
. . . 4
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β βπ β π΄ (π΅ β dom vol β§ (volβπ΅) β
β)) |
6 | | simpl3 1193 |
. . . 4
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β Disj π β π΄ π΅) |
7 | | volfiniun 25063 |
. . . 4
β’ ((π΄ β Fin β§ βπ β π΄ (π΅ β dom vol β§ (volβπ΅) β β) β§
Disj π β π΄ π΅) β (volββͺ π β π΄ π΅) = Ξ£π β π΄ (volβπ΅)) |
8 | 1, 5, 6, 7 | syl3anc 1371 |
. . 3
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β (volββͺ π β π΄ π΅) = Ξ£π β π΄ (volβπ΅)) |
9 | | nfcv 2903 |
. . . 4
β’
β²ππ΄ |
10 | 9 | nfel1 2919 |
. . . . . 6
β’
β²π π΄ β Fin |
11 | | nfra1 3281 |
. . . . . 6
β’
β²πβπ β π΄ π΅ β dom vol |
12 | | nfdisj1 5127 |
. . . . . 6
β’
β²πDisj
π β π΄ π΅ |
13 | 10, 11, 12 | nf3an 1904 |
. . . . 5
β’
β²π(π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) |
14 | | nfra1 3281 |
. . . . 5
β’
β²πβπ β π΄ (volβπ΅) β β |
15 | 13, 14 | nfan 1902 |
. . . 4
β’
β²π((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) |
16 | 3 | r19.21bi 3248 |
. . . . 5
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β§ π β π΄) β (volβπ΅) β β) |
17 | | rspa 3245 |
. . . . . . . 8
β’
((βπ β
π΄ π΅ β dom vol β§ π β π΄) β π΅ β dom vol) |
18 | | volf 25045 |
. . . . . . . . 9
β’ vol:dom
volβΆ(0[,]+β) |
19 | 18 | ffvelcdmi 7085 |
. . . . . . . 8
β’ (π΅ β dom vol β
(volβπ΅) β
(0[,]+β)) |
20 | 17, 19 | syl 17 |
. . . . . . 7
β’
((βπ β
π΄ π΅ β dom vol β§ π β π΄) β (volβπ΅) β (0[,]+β)) |
21 | 2, 20 | sylan 580 |
. . . . . 6
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β§ π β π΄) β (volβπ΅) β (0[,]+β)) |
22 | | 0xr 11260 |
. . . . . . . 8
β’ 0 β
β* |
23 | | pnfxr 11267 |
. . . . . . . 8
β’ +β
β β* |
24 | | elicc1 13367 |
. . . . . . . 8
β’ ((0
β β* β§ +β β β*) β
((volβπ΅) β
(0[,]+β) β ((volβπ΅) β β* β§ 0 β€
(volβπ΅) β§
(volβπ΅) β€
+β))) |
25 | 22, 23, 24 | mp2an 690 |
. . . . . . 7
β’
((volβπ΅)
β (0[,]+β) β ((volβπ΅) β β* β§ 0 β€
(volβπ΅) β§
(volβπ΅) β€
+β)) |
26 | 25 | simp2bi 1146 |
. . . . . 6
β’
((volβπ΅)
β (0[,]+β) β 0 β€ (volβπ΅)) |
27 | 21, 26 | syl 17 |
. . . . 5
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β§ π β π΄) β 0 β€ (volβπ΅)) |
28 | | ltpnf 13099 |
. . . . . 6
β’
((volβπ΅)
β β β (volβπ΅) < +β) |
29 | 16, 28 | syl 17 |
. . . . 5
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β§ π β π΄) β (volβπ΅) < +β) |
30 | | 0re 11215 |
. . . . . 6
β’ 0 β
β |
31 | | elico2 13387 |
. . . . . 6
β’ ((0
β β β§ +β β β*) β
((volβπ΅) β
(0[,)+β) β ((volβπ΅) β β β§ 0 β€
(volβπ΅) β§
(volβπ΅) <
+β))) |
32 | 30, 23, 31 | mp2an 690 |
. . . . 5
β’
((volβπ΅)
β (0[,)+β) β ((volβπ΅) β β β§ 0 β€
(volβπ΅) β§
(volβπ΅) <
+β)) |
33 | 16, 27, 29, 32 | syl3anbrc 1343 |
. . . 4
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β§ π β π΄) β (volβπ΅) β (0[,)+β)) |
34 | 9, 15, 1, 33 | esumpfinvalf 33069 |
. . 3
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β
Ξ£*π β
π΄(volβπ΅) = Ξ£π β π΄ (volβπ΅)) |
35 | 8, 34 | eqtr4d 2775 |
. 2
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) β β) β (volββͺ π β π΄ π΅) = Ξ£*π β π΄(volβπ΅)) |
36 | | simpr 485 |
. . . . . . . 8
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β βπ β π΄ (volβπ΅) = +β) |
37 | | nfv 1917 |
. . . . . . . . 9
β’
β²π(volβπ΅) = +β |
38 | | nfcv 2903 |
. . . . . . . . . . 11
β’
β²πvol |
39 | | nfcsb1v 3918 |
. . . . . . . . . . 11
β’
β²πβ¦π / πβ¦π΅ |
40 | 38, 39 | nffv 6901 |
. . . . . . . . . 10
β’
β²π(volββ¦π / πβ¦π΅) |
41 | 40 | nfeq1 2918 |
. . . . . . . . 9
β’
β²π(volββ¦π / πβ¦π΅) = +β |
42 | | csbeq1a 3907 |
. . . . . . . . . 10
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
43 | 42 | fveqeq2d 6899 |
. . . . . . . . 9
β’ (π = π β ((volβπ΅) = +β β
(volββ¦π
/ πβ¦π΅) = +β)) |
44 | 37, 41, 43 | cbvrexw 3304 |
. . . . . . . 8
β’
(βπ β
π΄ (volβπ΅) = +β β βπ β π΄ (volββ¦π / πβ¦π΅) = +β) |
45 | 36, 44 | sylib 217 |
. . . . . . 7
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β βπ β π΄ (volββ¦π / πβ¦π΅) = +β) |
46 | 39 | nfel1 2919 |
. . . . . . . . . . . . . 14
β’
β²πβ¦π / πβ¦π΅ β dom vol |
47 | 42 | eleq1d 2818 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΅ β dom vol β β¦π / πβ¦π΅ β dom vol)) |
48 | 46, 47 | rspc 3600 |
. . . . . . . . . . . . 13
β’ (π β π΄ β (βπ β π΄ π΅ β dom vol β β¦π / πβ¦π΅ β dom vol)) |
49 | 48 | impcom 408 |
. . . . . . . . . . . 12
β’
((βπ β
π΄ π΅ β dom vol β§ π β π΄) β β¦π / πβ¦π΅ β dom vol) |
50 | 49 | adantll 712 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β§ π β π΄) β β¦π / πβ¦π΅ β dom vol) |
51 | | finiunmbl 25060 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β βͺ π β π΄ π΅ β dom vol) |
52 | 51 | adantr 481 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β§ π β π΄) β βͺ
π β π΄ π΅ β dom vol) |
53 | | nfcv 2903 |
. . . . . . . . . . . . 13
β’
β²ππ |
54 | 9, 53, 39, 42 | ssiun2sf 31786 |
. . . . . . . . . . . 12
β’ (π β π΄ β β¦π / πβ¦π΅ β βͺ
π β π΄ π΅) |
55 | 54 | adantl 482 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β§ π β π΄) β β¦π / πβ¦π΅ β βͺ
π β π΄ π΅) |
56 | | volss 25049 |
. . . . . . . . . . 11
β’
((β¦π /
πβ¦π΅ β dom vol β§ βͺ π β π΄ π΅ β dom vol β§ β¦π / πβ¦π΅ β βͺ
π β π΄ π΅) β (volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅)) |
57 | 50, 52, 55, 56 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β§ π β π΄) β (volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅)) |
58 | 57 | 3adantl3 1168 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ π β π΄) β (volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅)) |
59 | 58 | adantlr 713 |
. . . . . . . 8
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β§ π β π΄) β (volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅)) |
60 | 59 | ralrimiva 3146 |
. . . . . . 7
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β βπ β π΄ (volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅)) |
61 | | r19.29r 3116 |
. . . . . . 7
β’
((βπ β
π΄
(volββ¦π
/ πβ¦π΅) = +β β§ βπ β π΄ (volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅)) β βπ β π΄ ((volββ¦π / πβ¦π΅) = +β β§
(volββ¦π
/ πβ¦π΅) β€ (volββͺ π β π΄ π΅))) |
62 | 45, 60, 61 | syl2anc 584 |
. . . . . 6
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β βπ β π΄ ((volββ¦π / πβ¦π΅) = +β β§
(volββ¦π
/ πβ¦π΅) β€ (volββͺ π β π΄ π΅))) |
63 | | breq1 5151 |
. . . . . . . 8
β’
((volββ¦π / πβ¦π΅) = +β β
((volββ¦π / πβ¦π΅) β€ (volββͺ π β π΄ π΅) β +β β€ (volββͺ π β π΄ π΅))) |
64 | 63 | biimpa 477 |
. . . . . . 7
β’
(((volββ¦π / πβ¦π΅) = +β β§
(volββ¦π
/ πβ¦π΅) β€ (volββͺ π β π΄ π΅)) β +β β€ (volββͺ π β π΄ π΅)) |
65 | 64 | reximi 3084 |
. . . . . 6
β’
(βπ β
π΄
((volββ¦π / πβ¦π΅) = +β β§
(volββ¦π
/ πβ¦π΅) β€ (volββͺ π β π΄ π΅)) β βπ β π΄ +β β€ (volββͺ π β π΄ π΅)) |
66 | 62, 65 | syl 17 |
. . . . 5
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β βπ β π΄ +β β€ (volββͺ π β π΄ π΅)) |
67 | | rexex 3076 |
. . . . . 6
β’
(βπ β
π΄ +β β€
(volββͺ π β π΄ π΅) β βπ+β β€ (volββͺ π β π΄ π΅)) |
68 | | 19.9v 1987 |
. . . . . 6
β’
(βπ+β
β€ (volββͺ π β π΄ π΅) β +β β€ (volββͺ π β π΄ π΅)) |
69 | 67, 68 | sylib 217 |
. . . . 5
β’
(βπ β
π΄ +β β€
(volββͺ π β π΄ π΅) β +β β€ (volββͺ π β π΄ π΅)) |
70 | 66, 69 | syl 17 |
. . . 4
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β +β β€
(volββͺ π β π΄ π΅)) |
71 | | iccssxr 13406 |
. . . . . . . . 9
β’
(0[,]+β) β β* |
72 | 18 | ffvelcdmi 7085 |
. . . . . . . . 9
β’ (βͺ π β π΄ π΅ β dom vol β (volββͺ π β π΄ π΅) β (0[,]+β)) |
73 | 71, 72 | sselid 3980 |
. . . . . . . 8
β’ (βͺ π β π΄ π΅ β dom vol β (volββͺ π β π΄ π΅) β
β*) |
74 | 51, 73 | syl 17 |
. . . . . . 7
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β (volββͺ π β π΄ π΅) β
β*) |
75 | 74 | 3adant3 1132 |
. . . . . 6
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β (volββͺ π β π΄ π΅) β
β*) |
76 | 75 | adantr 481 |
. . . . 5
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β (volββͺ π β π΄ π΅) β
β*) |
77 | | xgepnf 13143 |
. . . . 5
β’
((volββͺ π β π΄ π΅) β β* β
(+β β€ (volββͺ π β π΄ π΅) β (volββͺ π β π΄ π΅) = +β)) |
78 | 76, 77 | syl 17 |
. . . 4
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β (+β β€
(volββͺ π β π΄ π΅) β (volββͺ π β π΄ π΅) = +β)) |
79 | 70, 78 | mpbid 231 |
. . 3
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β (volββͺ π β π΄ π΅) = +β) |
80 | | nfre1 3282 |
. . . . 5
β’
β²πβπ β π΄ (volβπ΅) = +β |
81 | 13, 80 | nfan 1902 |
. . . 4
β’
β²π((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) |
82 | | simpl1 1191 |
. . . 4
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β π΄ β Fin) |
83 | 20 | 3ad2antl2 1186 |
. . . . 5
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ π β π΄) β (volβπ΅) β (0[,]+β)) |
84 | 83 | adantlr 713 |
. . . 4
β’ ((((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β§ π β π΄) β (volβπ΅) β (0[,]+β)) |
85 | 81, 82, 84, 36 | esumpinfval 33066 |
. . 3
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β
Ξ£*π β
π΄(volβπ΅) = +β) |
86 | 79, 85 | eqtr4d 2775 |
. 2
β’ (((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β§ βπ β π΄ (volβπ΅) = +β) β (volββͺ π β π΄ π΅) = Ξ£*π β π΄(volβπ΅)) |
87 | | exmid 893 |
. . . . 5
β’
(βπ β
π΄ (volβπ΅) β β β¨ Β¬
βπ β π΄ (volβπ΅) β β) |
88 | | rexnal 3100 |
. . . . . 6
β’
(βπ β
π΄ Β¬ (volβπ΅) β β β Β¬
βπ β π΄ (volβπ΅) β β) |
89 | 88 | orbi2i 911 |
. . . . 5
β’
((βπ β
π΄ (volβπ΅) β β β¨
βπ β π΄ Β¬ (volβπ΅) β β) β
(βπ β π΄ (volβπ΅) β β β¨ Β¬ βπ β π΄ (volβπ΅) β β)) |
90 | 87, 89 | mpbir 230 |
. . . 4
β’
(βπ β
π΄ (volβπ΅) β β β¨
βπ β π΄ Β¬ (volβπ΅) β
β) |
91 | | r19.29 3114 |
. . . . . . 7
β’
((βπ β
π΄ π΅ β dom vol β§ βπ β π΄ Β¬ (volβπ΅) β β) β βπ β π΄ (π΅ β dom vol β§ Β¬ (volβπ΅) β
β)) |
92 | | xrge0nre 13429 |
. . . . . . . . 9
β’
(((volβπ΅)
β (0[,]+β) β§ Β¬ (volβπ΅) β β) β (volβπ΅) = +β) |
93 | 19, 92 | sylan 580 |
. . . . . . . 8
β’ ((π΅ β dom vol β§ Β¬
(volβπ΅) β
β) β (volβπ΅) = +β) |
94 | 93 | reximi 3084 |
. . . . . . 7
β’
(βπ β
π΄ (π΅ β dom vol β§ Β¬ (volβπ΅) β β) β
βπ β π΄ (volβπ΅) = +β) |
95 | 91, 94 | syl 17 |
. . . . . 6
β’
((βπ β
π΄ π΅ β dom vol β§ βπ β π΄ Β¬ (volβπ΅) β β) β βπ β π΄ (volβπ΅) = +β) |
96 | 95 | ex 413 |
. . . . 5
β’
(βπ β
π΄ π΅ β dom vol β (βπ β π΄ Β¬ (volβπ΅) β β β βπ β π΄ (volβπ΅) = +β)) |
97 | 96 | orim2d 965 |
. . . 4
β’
(βπ β
π΄ π΅ β dom vol β ((βπ β π΄ (volβπ΅) β β β¨ βπ β π΄ Β¬ (volβπ΅) β β) β (βπ β π΄ (volβπ΅) β β β¨ βπ β π΄ (volβπ΅) = +β))) |
98 | 90, 97 | mpi 20 |
. . 3
β’
(βπ β
π΄ π΅ β dom vol β (βπ β π΄ (volβπ΅) β β β¨ βπ β π΄ (volβπ΅) = +β)) |
99 | 98 | 3ad2ant2 1134 |
. 2
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β (βπ β π΄ (volβπ΅) β β β¨ βπ β π΄ (volβπ΅) = +β)) |
100 | 35, 86, 99 | mpjaodan 957 |
1
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β (volββͺ π β π΄ π΅) = Ξ£*π β π΄(volβπ΅)) |