Step | Hyp | Ref
| Expression |
1 | | 0lt1 11685 |
. . . 4
β’ 0 <
1 |
2 | | 0re 11165 |
. . . . . 6
β’ 0 β
β |
3 | | 1re 11163 |
. . . . . 6
β’ 1 β
β |
4 | | 0le1 11686 |
. . . . . 6
β’ 0 β€
1 |
5 | | ovolicc 24910 |
. . . . . 6
β’ ((0
β β β§ 1 β β β§ 0 β€ 1) β
(vol*β(0[,]1)) = (1 β 0)) |
6 | 2, 3, 4, 5 | mp3an 1462 |
. . . . 5
β’
(vol*β(0[,]1)) = (1 β 0) |
7 | | 1m0e1 12282 |
. . . . 5
β’ (1
β 0) = 1 |
8 | 6, 7 | eqtri 2761 |
. . . 4
β’
(vol*β(0[,]1)) = 1 |
9 | 1, 8 | breqtrri 5136 |
. . 3
β’ 0 <
(vol*β(0[,]1)) |
10 | 8, 3 | eqeltri 2830 |
. . . 4
β’
(vol*β(0[,]1)) β β |
11 | 2, 10 | ltnlei 11284 |
. . 3
β’ (0 <
(vol*β(0[,]1)) β Β¬ (vol*β(0[,]1)) β€ 0) |
12 | 9, 11 | mpbi 229 |
. 2
β’ Β¬
(vol*β(0[,]1)) β€ 0 |
13 | | vitali.1 |
. . . . . 6
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} |
14 | | vitali.2 |
. . . . . 6
β’ π = ((0[,]1) / βΌ
) |
15 | | vitali.3 |
. . . . . 6
β’ (π β πΉ Fn π) |
16 | | vitali.4 |
. . . . . 6
β’ (π β βπ§ β π (π§ β β
β (πΉβπ§) β π§)) |
17 | | vitali.5 |
. . . . . 6
β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) |
18 | | vitali.6 |
. . . . . 6
β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
19 | | vitali.7 |
. . . . . 6
β’ (π β Β¬ ran πΉ β (π« β
β dom vol)) |
20 | 13, 14, 15, 16, 17, 18, 19 | vitalilem2 24996 |
. . . . 5
β’ (π β (ran πΉ β (0[,]1) β§ (0[,]1) β
βͺ π β β (πβπ) β§ βͺ
π β β (πβπ) β (-1[,]2))) |
21 | 20 | simp2d 1144 |
. . . 4
β’ (π β (0[,]1) β βͺ π β β (πβπ)) |
22 | 13 | vitalilem1 24995 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ βΌ Er
(0[,]1) |
23 | | erdm 8664 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ( βΌ Er
(0[,]1) β dom βΌ =
(0[,]1)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ dom βΌ =
(0[,]1) |
25 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β π) β π§ β π) |
26 | 25, 14 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β π) β π§ β ((0[,]1) / βΌ )) |
27 | | elqsn0 8731 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((dom
βΌ
= (0[,]1) β§ π§ β
((0[,]1) / βΌ )) β π§ β β
) |
28 | 24, 26, 27 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β π) β π§ β β
) |
29 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βΌ Er
(0[,]1)) |
30 | 29 | qsss 8723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((0[,]1) / βΌ )
β π« (0[,]1)) |
31 | 14, 30 | eqsstrid 3996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β π« (0[,]1)) |
32 | 31 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β π) β π§ β π« (0[,]1)) |
33 | 32 | elpwid 4573 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β π) β π§ β (0[,]1)) |
34 | 33 | sseld 3947 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β π) β ((πΉβπ§) β π§ β (πΉβπ§) β (0[,]1))) |
35 | 28, 34 | embantd 59 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β π) β ((π§ β β
β (πΉβπ§) β π§) β (πΉβπ§) β (0[,]1))) |
36 | 35 | ralimdva 3161 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (βπ§ β π (π§ β β
β (πΉβπ§) β π§) β βπ§ β π (πΉβπ§) β (0[,]1))) |
37 | 16, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ§ β π (πΉβπ§) β (0[,]1)) |
38 | | ffnfv 7070 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ:πβΆ(0[,]1) β (πΉ Fn π β§ βπ§ β π (πΉβπ§) β (0[,]1))) |
39 | 15, 37, 38 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:πβΆ(0[,]1)) |
40 | 39 | frnd 6680 |
. . . . . . . . . . . . . . . 16
β’ (π β ran πΉ β (0[,]1)) |
41 | | unitssre 13425 |
. . . . . . . . . . . . . . . 16
β’ (0[,]1)
β β |
42 | 40, 41 | sstrdi 3960 |
. . . . . . . . . . . . . . 15
β’ (π β ran πΉ β β) |
43 | | reex 11150 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
44 | 43 | elpw2 5306 |
. . . . . . . . . . . . . . 15
β’ (ran
πΉ β π« β
β ran πΉ β
β) |
45 | 42, 44 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π β ran πΉ β π« β) |
46 | 45 | anim1i 616 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ ran πΉ β dom vol) β (ran πΉ β π« β β§
Β¬ ran πΉ β dom
vol)) |
47 | | eldif 3924 |
. . . . . . . . . . . . 13
β’ (ran
πΉ β (π« β
β dom vol) β (ran πΉ β π« β β§ Β¬ ran
πΉ β dom
vol)) |
48 | 46, 47 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ ran πΉ β dom vol) β ran πΉ β (π« β
β dom vol)) |
49 | 48 | ex 414 |
. . . . . . . . . . 11
β’ (π β (Β¬ ran πΉ β dom vol β ran πΉ β (π« β
β dom vol))) |
50 | 19, 49 | mt3d 148 |
. . . . . . . . . 10
β’ (π β ran πΉ β dom vol) |
51 | | f1of 6788 |
. . . . . . . . . . . . 13
β’ (πΊ:ββ1-1-ontoβ(β β© (-1[,]1)) β πΊ:ββΆ(β β©
(-1[,]1))) |
52 | 17, 51 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΊ:ββΆ(β β©
(-1[,]1))) |
53 | | inss1 4192 |
. . . . . . . . . . . . 13
β’ (β
β© (-1[,]1)) β β |
54 | | qssre 12892 |
. . . . . . . . . . . . 13
β’ β
β β |
55 | 53, 54 | sstri 3957 |
. . . . . . . . . . . 12
β’ (β
β© (-1[,]1)) β β |
56 | | fss 6689 |
. . . . . . . . . . . 12
β’ ((πΊ:ββΆ(β β©
(-1[,]1)) β§ (β β© (-1[,]1)) β β) β πΊ:ββΆβ) |
57 | 52, 55, 56 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β πΊ:ββΆβ) |
58 | 57 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΊβπ) β β) |
59 | | shftmbl 24925 |
. . . . . . . . . 10
β’ ((ran
πΉ β dom vol β§
(πΊβπ) β β) β {π β β β£ (π β (πΊβπ)) β ran πΉ} β dom vol) |
60 | 50, 58, 59 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ π β β) β {π β β β£ (π β (πΊβπ)) β ran πΉ} β dom vol) |
61 | 60, 18 | fmptd 7066 |
. . . . . . . 8
β’ (π β π:ββΆdom vol) |
62 | 61 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) β dom vol) |
63 | 62 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ β β (πβπ) β dom vol) |
64 | | iunmbl 24940 |
. . . . . 6
β’
(βπ β
β (πβπ) β dom vol β βͺ π β β (πβπ) β dom vol) |
65 | 63, 64 | syl 17 |
. . . . 5
β’ (π β βͺ π β β (πβπ) β dom vol) |
66 | | mblss 24918 |
. . . . 5
β’ (βͺ π β β (πβπ) β dom vol β βͺ π β β (πβπ) β β) |
67 | 65, 66 | syl 17 |
. . . 4
β’ (π β βͺ π β β (πβπ) β β) |
68 | | ovolss 24872 |
. . . 4
β’ (((0[,]1)
β βͺ π β β (πβπ) β§ βͺ
π β β (πβπ) β β) β
(vol*β(0[,]1)) β€ (vol*ββͺ π β β (πβπ))) |
69 | 21, 67, 68 | syl2anc 585 |
. . 3
β’ (π β (vol*β(0[,]1)) β€
(vol*ββͺ π β β (πβπ))) |
70 | | eqid 2733 |
. . . . . 6
β’ seq1( + ,
(π β β β¦
(vol*β(πβπ)))) = seq1( + , (π β β β¦
(vol*β(πβπ)))) |
71 | | eqid 2733 |
. . . . . 6
β’ (π β β β¦
(vol*β(πβπ))) = (π β β β¦ (vol*β(πβπ))) |
72 | | mblss 24918 |
. . . . . . 7
β’ ((πβπ) β dom vol β (πβπ) β β) |
73 | 62, 72 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β (πβπ) β β) |
74 | 13, 14, 15, 16, 17, 18, 19 | vitalilem4 24998 |
. . . . . . 7
β’ ((π β§ π β β) β (vol*β(πβπ)) = 0) |
75 | 74, 2 | eqeltrdi 2842 |
. . . . . 6
β’ ((π β§ π β β) β (vol*β(πβπ)) β β) |
76 | 74 | mpteq2dva 5209 |
. . . . . . . . . 10
β’ (π β (π β β β¦ (vol*β(πβπ))) = (π β β β¦ 0)) |
77 | | fconstmpt 5698 |
. . . . . . . . . . 11
β’ (β
Γ {0}) = (π β
β β¦ 0) |
78 | | nnuz 12814 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
79 | 78 | xpeq1i 5663 |
. . . . . . . . . . 11
β’ (β
Γ {0}) = ((β€β₯β1) Γ {0}) |
80 | 77, 79 | eqtr3i 2763 |
. . . . . . . . . 10
β’ (π β β β¦ 0) =
((β€β₯β1) Γ {0}) |
81 | 76, 80 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β (π β β β¦ (vol*β(πβπ))) = ((β€β₯β1)
Γ {0})) |
82 | 81 | seqeq3d 13923 |
. . . . . . . 8
β’ (π β seq1( + , (π β β β¦
(vol*β(πβπ)))) = seq1( + ,
((β€β₯β1) Γ {0}))) |
83 | | 1z 12541 |
. . . . . . . . 9
β’ 1 β
β€ |
84 | | serclim0 15468 |
. . . . . . . . 9
β’ (1 β
β€ β seq1( + , ((β€β₯β1) Γ {0}))
β 0) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . 8
β’ seq1( + ,
((β€β₯β1) Γ {0})) β 0 |
86 | 82, 85 | eqbrtrdi 5148 |
. . . . . . 7
β’ (π β seq1( + , (π β β β¦
(vol*β(πβπ)))) β 0) |
87 | | seqex 13917 |
. . . . . . . 8
β’ seq1( + ,
(π β β β¦
(vol*β(πβπ)))) β V |
88 | | c0ex 11157 |
. . . . . . . 8
β’ 0 β
V |
89 | 87, 88 | breldm 5868 |
. . . . . . 7
β’ (seq1( +
, (π β β β¦
(vol*β(πβπ)))) β 0 β seq1( + ,
(π β β β¦
(vol*β(πβπ)))) β dom β
) |
90 | 86, 89 | syl 17 |
. . . . . 6
β’ (π β seq1( + , (π β β β¦
(vol*β(πβπ)))) β dom β
) |
91 | 70, 71, 73, 75, 90 | ovoliun2 24893 |
. . . . 5
β’ (π β (vol*ββͺ π β β (πβπ)) β€ Ξ£π β β (vol*β(πβπ))) |
92 | 74 | sumeq2dv 15596 |
. . . . . 6
β’ (π β Ξ£π β β (vol*β(πβπ)) = Ξ£π β β 0) |
93 | 78 | eqimssi 4006 |
. . . . . . . 8
β’ β
β (β€β₯β1) |
94 | 93 | orci 864 |
. . . . . . 7
β’ (β
β (β€β₯β1) β¨ β β
Fin) |
95 | | sumz 15615 |
. . . . . . 7
β’ ((β
β (β€β₯β1) β¨ β β Fin) β
Ξ£π β β 0 =
0) |
96 | 94, 95 | ax-mp 5 |
. . . . . 6
β’
Ξ£π β
β 0 = 0 |
97 | 92, 96 | eqtrdi 2789 |
. . . . 5
β’ (π β Ξ£π β β (vol*β(πβπ)) = 0) |
98 | 91, 97 | breqtrd 5135 |
. . . 4
β’ (π β (vol*ββͺ π β β (πβπ)) β€ 0) |
99 | | ovolge0 24868 |
. . . . 5
β’ (βͺ π β β (πβπ) β β β 0 β€
(vol*ββͺ π β β (πβπ))) |
100 | 67, 99 | syl 17 |
. . . 4
β’ (π β 0 β€
(vol*ββͺ π β β (πβπ))) |
101 | | ovolcl 24865 |
. . . . . 6
β’ (βͺ π β β (πβπ) β β β (vol*ββͺ π β β (πβπ)) β
β*) |
102 | 67, 101 | syl 17 |
. . . . 5
β’ (π β (vol*ββͺ π β β (πβπ)) β
β*) |
103 | | 0xr 11210 |
. . . . 5
β’ 0 β
β* |
104 | | xrletri3 13082 |
. . . . 5
β’
(((vol*ββͺ π β β (πβπ)) β β* β§ 0 β
β*) β ((vol*ββͺ
π β β (πβπ)) = 0 β ((vol*ββͺ π β β (πβπ)) β€ 0 β§ 0 β€ (vol*ββͺ π β β (πβπ))))) |
105 | 102, 103,
104 | sylancl 587 |
. . . 4
β’ (π β ((vol*ββͺ π β β (πβπ)) = 0 β ((vol*ββͺ π β β (πβπ)) β€ 0 β§ 0 β€ (vol*ββͺ π β β (πβπ))))) |
106 | 98, 100, 105 | mpbir2and 712 |
. . 3
β’ (π β (vol*ββͺ π β β (πβπ)) = 0) |
107 | 69, 106 | breqtrd 5135 |
. 2
β’ (π β (vol*β(0[,]1)) β€
0) |
108 | 12, 107 | mto 196 |
1
β’ Β¬
π |