Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β (πΊβπ) = (πΊβπ)) |
2 | 1 | oveq2d 7378 |
. . . . . . . 8
β’ (π = π β (π β (πΊβπ)) = (π β (πΊβπ))) |
3 | 2 | eleq1d 2823 |
. . . . . . 7
β’ (π = π β ((π β (πΊβπ)) β ran πΉ β (π β (πΊβπ)) β ran πΉ)) |
4 | 3 | rabbidv 3418 |
. . . . . 6
β’ (π = π β {π β β β£ (π β (πΊβπ)) β ran πΉ} = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
5 | | vitali.6 |
. . . . . 6
β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
6 | | reex 11149 |
. . . . . . 7
β’ β
β V |
7 | 6 | rabex 5294 |
. . . . . 6
β’ {π β β β£ (π β (πΊβπ)) β ran πΉ} β V |
8 | 4, 5, 7 | fvmpt 6953 |
. . . . 5
β’ (π β β β (πβπ) = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
9 | 8 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β (πβπ) = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
10 | 9 | fveq2d 6851 |
. . 3
β’ ((π β§ π β β) β (vol*β(πβπ)) = (vol*β{π β β β£ (π β (πΊβπ)) β ran πΉ})) |
11 | | vitali.1 |
. . . . . . . 8
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} |
12 | | vitali.2 |
. . . . . . . 8
β’ π = ((0[,]1) / βΌ
) |
13 | | vitali.3 |
. . . . . . . 8
β’ (π β πΉ Fn π) |
14 | | vitali.4 |
. . . . . . . 8
β’ (π β βπ§ β π (π§ β β
β (πΉβπ§) β π§)) |
15 | | vitali.5 |
. . . . . . . 8
β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) |
16 | | vitali.7 |
. . . . . . . 8
β’ (π β Β¬ ran πΉ β (π« β
β dom vol)) |
17 | 11, 12, 13, 14, 15, 5, 16 | vitalilem2 24989 |
. . . . . . 7
β’ (π β (ran πΉ β (0[,]1) β§ (0[,]1) β
βͺ π β β (πβπ) β§ βͺ
π β β (πβπ) β (-1[,]2))) |
18 | 17 | simp1d 1143 |
. . . . . 6
β’ (π β ran πΉ β (0[,]1)) |
19 | | unitssre 13423 |
. . . . . 6
β’ (0[,]1)
β β |
20 | 18, 19 | sstrdi 3961 |
. . . . 5
β’ (π β ran πΉ β β) |
21 | 20 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β ran πΉ β β) |
22 | | neg1rr 12275 |
. . . . . 6
β’ -1 β
β |
23 | | 1re 11162 |
. . . . . 6
β’ 1 β
β |
24 | | iccssre 13353 |
. . . . . 6
β’ ((-1
β β β§ 1 β β) β (-1[,]1) β
β) |
25 | 22, 23, 24 | mp2an 691 |
. . . . 5
β’ (-1[,]1)
β β |
26 | | f1of 6789 |
. . . . . . . 8
β’ (πΊ:ββ1-1-ontoβ(β β© (-1[,]1)) β πΊ:ββΆ(β β©
(-1[,]1))) |
27 | 15, 26 | syl 17 |
. . . . . . 7
β’ (π β πΊ:ββΆ(β β©
(-1[,]1))) |
28 | 27 | ffvelcdmda 7040 |
. . . . . 6
β’ ((π β§ π β β) β (πΊβπ) β (β β©
(-1[,]1))) |
29 | 28 | elin2d 4164 |
. . . . 5
β’ ((π β§ π β β) β (πΊβπ) β (-1[,]1)) |
30 | 25, 29 | sselid 3947 |
. . . 4
β’ ((π β§ π β β) β (πΊβπ) β β) |
31 | | eqidd 2738 |
. . . 4
β’ ((π β§ π β β) β {π β β β£ (π β (πΊβπ)) β ran πΉ} = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
32 | 21, 30, 31 | ovolshft 24891 |
. . 3
β’ ((π β§ π β β) β (vol*βran πΉ) = (vol*β{π β β β£ (π β (πΊβπ)) β ran πΉ})) |
33 | 10, 32 | eqtr4d 2780 |
. 2
β’ ((π β§ π β β) β (vol*β(πβπ)) = (vol*βran πΉ)) |
34 | | 3re 12240 |
. . . . . . . 8
β’ 3 β
β |
35 | 34 | rexri 11220 |
. . . . . . 7
β’ 3 β
β* |
36 | 35 | a1i 11 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β 3 β
β*) |
37 | | 3rp 12928 |
. . . . . . . . . . . . 13
β’ 3 β
β+ |
38 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 β
β |
39 | | 0le1 11685 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 β€
1 |
40 | | ovolicc 24903 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((0
β β β§ 1 β β β§ 0 β€ 1) β
(vol*β(0[,]1)) = (1 β 0)) |
41 | 38, 23, 39, 40 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . 19
β’
(vol*β(0[,]1)) = (1 β 0) |
42 | | 1m0e1 12281 |
. . . . . . . . . . . . . . . . . . 19
β’ (1
β 0) = 1 |
43 | 41, 42 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’
(vol*β(0[,]1)) = 1 |
44 | 43, 23 | eqeltri 2834 |
. . . . . . . . . . . . . . . . 17
β’
(vol*β(0[,]1)) β β |
45 | | ovolsscl 24866 |
. . . . . . . . . . . . . . . . 17
β’ ((ran
πΉ β (0[,]1) β§
(0[,]1) β β β§ (vol*β(0[,]1)) β β) β
(vol*βran πΉ) β
β) |
46 | 19, 44, 45 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
β’ (ran
πΉ β (0[,]1) β
(vol*βran πΉ) β
β) |
47 | 18, 46 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (vol*βran πΉ) β
β) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ 0 < (vol*βran
πΉ)) β (vol*βran
πΉ) β
β) |
49 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ 0 < (vol*βran
πΉ)) β 0 <
(vol*βran πΉ)) |
50 | 48, 49 | elrpd 12961 |
. . . . . . . . . . . . 13
β’ ((π β§ 0 < (vol*βran
πΉ)) β (vol*βran
πΉ) β
β+) |
51 | | rpdivcl 12947 |
. . . . . . . . . . . . 13
β’ ((3
β β+ β§ (vol*βran πΉ) β β+) β (3 /
(vol*βran πΉ)) β
β+) |
52 | 37, 50, 51 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ 0 < (vol*βran
πΉ)) β (3 /
(vol*βran πΉ)) β
β+) |
53 | 52 | rpred 12964 |
. . . . . . . . . . 11
β’ ((π β§ 0 < (vol*βran
πΉ)) β (3 /
(vol*βran πΉ)) β
β) |
54 | 52 | rpge0d 12968 |
. . . . . . . . . . 11
β’ ((π β§ 0 < (vol*βran
πΉ)) β 0 β€ (3 /
(vol*βran πΉ))) |
55 | | flge0nn0 13732 |
. . . . . . . . . . 11
β’ (((3 /
(vol*βran πΉ)) β
β β§ 0 β€ (3 / (vol*βran πΉ))) β (ββ(3 /
(vol*βran πΉ))) β
β0) |
56 | 53, 54, 55 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(ββ(3 / (vol*βran πΉ))) β
β0) |
57 | | nn0p1nn 12459 |
. . . . . . . . . 10
β’
((ββ(3 / (vol*βran πΉ))) β β0 β
((ββ(3 / (vol*βran πΉ))) + 1) β β) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
β’ ((π β§ 0 < (vol*βran
πΉ)) β
((ββ(3 / (vol*βran πΉ))) + 1) β β) |
59 | 58 | nnred 12175 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β
((ββ(3 / (vol*βran πΉ))) + 1) β β) |
60 | 59, 48 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ)) β
β) |
61 | 60 | rexrd 11212 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ)) β
β*) |
62 | 6 | elpw2 5307 |
. . . . . . . . . . . . . . . . . 18
β’ (ran
πΉ β π« β
β ran πΉ β
β) |
63 | 20, 62 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π β ran πΉ β π« β) |
64 | 63 | anim1i 616 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ ran πΉ β dom vol) β (ran πΉ β π« β β§
Β¬ ran πΉ β dom
vol)) |
65 | | eldif 3925 |
. . . . . . . . . . . . . . . 16
β’ (ran
πΉ β (π« β
β dom vol) β (ran πΉ β π« β β§ Β¬ ran
πΉ β dom
vol)) |
66 | 64, 65 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ ran πΉ β dom vol) β ran πΉ β (π« β
β dom vol)) |
67 | 66 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β (Β¬ ran πΉ β dom vol β ran πΉ β (π« β
β dom vol))) |
68 | 16, 67 | mt3d 148 |
. . . . . . . . . . . . 13
β’ (π β ran πΉ β dom vol) |
69 | | inss1 4193 |
. . . . . . . . . . . . . . . 16
β’ (β
β© (-1[,]1)) β β |
70 | | qssre 12891 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
71 | 69, 70 | sstri 3958 |
. . . . . . . . . . . . . . 15
β’ (β
β© (-1[,]1)) β β |
72 | | fss 6690 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:ββΆ(β β©
(-1[,]1)) β§ (β β© (-1[,]1)) β β) β πΊ:ββΆβ) |
73 | 27, 71, 72 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:ββΆβ) |
74 | 73 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΊβπ) β β) |
75 | | shftmbl 24918 |
. . . . . . . . . . . . 13
β’ ((ran
πΉ β dom vol β§
(πΊβπ) β β) β {π β β β£ (π β (πΊβπ)) β ran πΉ} β dom vol) |
76 | 68, 74, 75 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β {π β β β£ (π β (πΊβπ)) β ran πΉ} β dom vol) |
77 | 76, 5 | fmptd 7067 |
. . . . . . . . . . 11
β’ (π β π:ββΆdom vol) |
78 | 77 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) β dom vol) |
79 | 78 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β β (πβπ) β dom vol) |
80 | | iunmbl 24933 |
. . . . . . . . 9
β’
(βπ β
β (πβπ) β dom vol β βͺ π β β (πβπ) β dom vol) |
81 | 79, 80 | syl 17 |
. . . . . . . 8
β’ (π β βͺ π β β (πβπ) β dom vol) |
82 | | mblss 24911 |
. . . . . . . 8
β’ (βͺ π β β (πβπ) β dom vol β βͺ π β β (πβπ) β β) |
83 | | ovolcl 24858 |
. . . . . . . 8
β’ (βͺ π β β (πβπ) β β β (vol*ββͺ π β β (πβπ)) β
β*) |
84 | 81, 82, 83 | 3syl 18 |
. . . . . . 7
β’ (π β (vol*ββͺ π β β (πβπ)) β
β*) |
85 | 84 | adantr 482 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(vol*ββͺ π β β (πβπ)) β
β*) |
86 | | flltp1 13712 |
. . . . . . . 8
β’ ((3 /
(vol*βran πΉ)) β
β β (3 / (vol*βran πΉ)) < ((ββ(3 / (vol*βran
πΉ))) + 1)) |
87 | 53, 86 | syl 17 |
. . . . . . 7
β’ ((π β§ 0 < (vol*βran
πΉ)) β (3 /
(vol*βran πΉ)) <
((ββ(3 / (vol*βran πΉ))) + 1)) |
88 | 34 | a1i 11 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β 3 β
β) |
89 | 88, 59, 50 | ltdivmul2d 13016 |
. . . . . . 7
β’ ((π β§ 0 < (vol*βran
πΉ)) β ((3 /
(vol*βran πΉ)) <
((ββ(3 / (vol*βran πΉ))) + 1) β 3 < (((ββ(3 /
(vol*βran πΉ))) + 1)
Β· (vol*βran πΉ)))) |
90 | 87, 89 | mpbid 231 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β 3 <
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ))) |
91 | | nnuz 12813 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
92 | | 1zzd 12541 |
. . . . . . . . . . 11
β’ ((π β§ 0 < (vol*βran
πΉ)) β 1 β
β€) |
93 | | mblvol 24910 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) β dom vol β (volβ(πβπ)) = (vol*β(πβπ))) |
94 | 78, 93 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (volβ(πβπ)) = (vol*β(πβπ))) |
95 | 94, 33 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (volβ(πβπ)) = (vol*βran πΉ)) |
96 | 47 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (vol*βran πΉ) β
β) |
97 | 95, 96 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (volβ(πβπ)) β β) |
98 | 97 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ 0 < (vol*βran
πΉ)) β§ π β β) β
(volβ(πβπ)) β
β) |
99 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β β¦
(volβ(πβπ))) = (π β β β¦ (volβ(πβπ))) |
100 | 98, 99 | fmptd 7067 |
. . . . . . . . . . . 12
β’ ((π β§ 0 < (vol*βran
πΉ)) β (π β β β¦
(volβ(πβπ))):ββΆβ) |
101 | 100 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ (((π β§ 0 < (vol*βran
πΉ)) β§ π β β) β ((π β β β¦
(volβ(πβπ)))βπ) β β) |
102 | 91, 92, 101 | serfre 13944 |
. . . . . . . . . 10
β’ ((π β§ 0 < (vol*βran
πΉ)) β seq1( + , (π β β β¦
(volβ(πβπ)))):ββΆβ) |
103 | 102 | frnd 6681 |
. . . . . . . . 9
β’ ((π β§ 0 < (vol*βran
πΉ)) β ran seq1( + ,
(π β β β¦
(volβ(πβπ)))) β
β) |
104 | | ressxr 11206 |
. . . . . . . . 9
β’ β
β β* |
105 | 103, 104 | sstrdi 3961 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β ran seq1( + ,
(π β β β¦
(volβ(πβπ)))) β
β*) |
106 | 95 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ 0 < (vol*βran
πΉ)) β§ π β β) β
(volβ(πβπ)) = (vol*βran πΉ)) |
107 | 106 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
β’ ((π β§ 0 < (vol*βran
πΉ)) β (π β β β¦
(volβ(πβπ))) = (π β β β¦ (vol*βran πΉ))) |
108 | | fconstmpt 5699 |
. . . . . . . . . . . . 13
β’ (β
Γ {(vol*βran πΉ)}) = (π β β β¦ (vol*βran πΉ)) |
109 | 107, 108 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π β§ 0 < (vol*βran
πΉ)) β (π β β β¦
(volβ(πβπ))) = (β Γ
{(vol*βran πΉ)})) |
110 | 109 | seqeq3d 13921 |
. . . . . . . . . . 11
β’ ((π β§ 0 < (vol*βran
πΉ)) β seq1( + , (π β β β¦
(volβ(πβπ)))) = seq1( + , (β
Γ {(vol*βran πΉ)}))) |
111 | 110 | fveq1d 6849 |
. . . . . . . . . 10
β’ ((π β§ 0 < (vol*βran
πΉ)) β (seq1( + ,
(π β β β¦
(volβ(πβπ))))β((ββ(3 /
(vol*βran πΉ))) + 1))
= (seq1( + , (β Γ {(vol*βran πΉ)}))β((ββ(3 /
(vol*βran πΉ))) +
1))) |
112 | 48 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ 0 < (vol*βran
πΉ)) β (vol*βran
πΉ) β
β) |
113 | | ser1const 13971 |
. . . . . . . . . . 11
β’
(((vol*βran πΉ)
β β β§ ((ββ(3 / (vol*βran πΉ))) + 1) β β) β (seq1( + ,
(β Γ {(vol*βran πΉ)}))β((ββ(3 /
(vol*βran πΉ))) + 1))
= (((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ))) |
114 | 112, 58, 113 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ 0 < (vol*βran
πΉ)) β (seq1( + ,
(β Γ {(vol*βran πΉ)}))β((ββ(3 /
(vol*βran πΉ))) + 1))
= (((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ))) |
115 | 111, 114 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ 0 < (vol*βran
πΉ)) β (seq1( + ,
(π β β β¦
(volβ(πβπ))))β((ββ(3 /
(vol*βran πΉ))) + 1))
= (((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ))) |
116 | 102 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ 0 < (vol*βran
πΉ)) β seq1( + , (π β β β¦
(volβ(πβπ)))) Fn
β) |
117 | | fnfvelrn 7036 |
. . . . . . . . . 10
β’ ((seq1( +
, (π β β β¦
(volβ(πβπ)))) Fn β β§
((ββ(3 / (vol*βran πΉ))) + 1) β β) β (seq1( + ,
(π β β β¦
(volβ(πβπ))))β((ββ(3 /
(vol*βran πΉ))) + 1))
β ran seq1( + , (π
β β β¦ (volβ(πβπ))))) |
118 | 116, 58, 117 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ 0 < (vol*βran
πΉ)) β (seq1( + ,
(π β β β¦
(volβ(πβπ))))β((ββ(3 /
(vol*βran πΉ))) + 1))
β ran seq1( + , (π
β β β¦ (volβ(πβπ))))) |
119 | 115, 118 | eqeltrrd 2839 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ)) β ran seq1( + , (π β β β¦
(volβ(πβπ))))) |
120 | | supxrub 13250 |
. . . . . . . 8
β’ ((ran
seq1( + , (π β β
β¦ (volβ(πβπ)))) β β* β§
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ)) β ran seq1( + , (π β β β¦
(volβ(πβπ))))) β (((ββ(3
/ (vol*βran πΉ))) + 1)
Β· (vol*βran πΉ)) β€ sup(ran seq1( + , (π β β β¦
(volβ(πβπ)))), β*, <
)) |
121 | 105, 119,
120 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ)) β€ sup(ran seq1( + , (π β β β¦
(volβ(πβπ)))), β*, <
)) |
122 | 81 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ 0 < (vol*βran
πΉ)) β βͺ π β β (πβπ) β dom vol) |
123 | | mblvol 24910 |
. . . . . . . . 9
β’ (βͺ π β β (πβπ) β dom vol β (volββͺ π β β (πβπ)) = (vol*ββͺ π β β (πβπ))) |
124 | 122, 123 | syl 17 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(volββͺ π β β (πβπ)) = (vol*ββͺ π β β (πβπ))) |
125 | 78, 97 | jca 513 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβπ) β dom vol β§ (volβ(πβπ)) β β)) |
126 | 125 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β β ((πβπ) β dom vol β§ (volβ(πβπ)) β β)) |
127 | 11, 12, 13, 14, 15, 5, 16 | vitalilem3 24990 |
. . . . . . . . . 10
β’ (π β Disj π β β (πβπ)) |
128 | 127 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ 0 < (vol*βran
πΉ)) β Disj
π β β (πβπ)) |
129 | | eqid 2737 |
. . . . . . . . . 10
β’ seq1( + ,
(π β β β¦
(volβ(πβπ)))) = seq1( + , (π β β β¦
(volβ(πβπ)))) |
130 | 129, 99 | voliun 24934 |
. . . . . . . . 9
β’
((βπ β
β ((πβπ) β dom vol β§
(volβ(πβπ)) β β) β§
Disj π β
β (πβπ)) β (volββͺ π β β (πβπ)) = sup(ran seq1( + , (π β β β¦ (volβ(πβπ)))), β*, <
)) |
131 | 126, 128,
130 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(volββͺ π β β (πβπ)) = sup(ran seq1( + , (π β β β¦ (volβ(πβπ)))), β*, <
)) |
132 | 124, 131 | eqtr3d 2779 |
. . . . . . 7
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(vol*ββͺ π β β (πβπ)) = sup(ran seq1( + , (π β β β¦ (volβ(πβπ)))), β*, <
)) |
133 | 121, 132 | breqtrrd 5138 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(((ββ(3 / (vol*βran πΉ))) + 1) Β· (vol*βran πΉ)) β€ (vol*ββͺ π β β (πβπ))) |
134 | 36, 61, 85, 90, 133 | xrltletrd 13087 |
. . . . 5
β’ ((π β§ 0 < (vol*βran
πΉ)) β 3 <
(vol*ββͺ π β β (πβπ))) |
135 | 17 | simp3d 1145 |
. . . . . . . . 9
β’ (π β βͺ π β β (πβπ) β (-1[,]2)) |
136 | 135 | adantr 482 |
. . . . . . . 8
β’ ((π β§ 0 < (vol*βran
πΉ)) β βͺ π β β (πβπ) β (-1[,]2)) |
137 | | 2re 12234 |
. . . . . . . . 9
β’ 2 β
β |
138 | | iccssre 13353 |
. . . . . . . . 9
β’ ((-1
β β β§ 2 β β) β (-1[,]2) β
β) |
139 | 22, 137, 138 | mp2an 691 |
. . . . . . . 8
β’ (-1[,]2)
β β |
140 | | ovolss 24865 |
. . . . . . . 8
β’
((βͺ π β β (πβπ) β (-1[,]2) β§ (-1[,]2) β
β) β (vol*ββͺ π β β (πβπ)) β€
(vol*β(-1[,]2))) |
141 | 136, 139,
140 | sylancl 587 |
. . . . . . 7
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(vol*ββͺ π β β (πβπ)) β€
(vol*β(-1[,]2))) |
142 | | 2cn 12235 |
. . . . . . . . 9
β’ 2 β
β |
143 | | ax-1cn 11116 |
. . . . . . . . 9
β’ 1 β
β |
144 | 142, 143 | subnegi 11487 |
. . . . . . . 8
β’ (2
β -1) = (2 + 1) |
145 | | neg1lt0 12277 |
. . . . . . . . . . 11
β’ -1 <
0 |
146 | | 2pos 12263 |
. . . . . . . . . . 11
β’ 0 <
2 |
147 | 22, 38, 137 | lttri 11288 |
. . . . . . . . . . 11
β’ ((-1 <
0 β§ 0 < 2) β -1 < 2) |
148 | 145, 146,
147 | mp2an 691 |
. . . . . . . . . 10
β’ -1 <
2 |
149 | 22, 137, 148 | ltleii 11285 |
. . . . . . . . 9
β’ -1 β€
2 |
150 | | ovolicc 24903 |
. . . . . . . . 9
β’ ((-1
β β β§ 2 β β β§ -1 β€ 2) β
(vol*β(-1[,]2)) = (2 β -1)) |
151 | 22, 137, 149, 150 | mp3an 1462 |
. . . . . . . 8
β’
(vol*β(-1[,]2)) = (2 β -1) |
152 | | df-3 12224 |
. . . . . . . 8
β’ 3 = (2 +
1) |
153 | 144, 151,
152 | 3eqtr4i 2775 |
. . . . . . 7
β’
(vol*β(-1[,]2)) = 3 |
154 | 141, 153 | breqtrdi 5151 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β
(vol*ββͺ π β β (πβπ)) β€ 3) |
155 | | xrlenlt 11227 |
. . . . . . 7
β’
(((vol*ββͺ π β β (πβπ)) β β* β§ 3 β
β*) β ((vol*ββͺ
π β β (πβπ)) β€ 3 β Β¬ 3 <
(vol*ββͺ π β β (πβπ)))) |
156 | 85, 35, 155 | sylancl 587 |
. . . . . 6
β’ ((π β§ 0 < (vol*βran
πΉ)) β
((vol*ββͺ π β β (πβπ)) β€ 3 β Β¬ 3 <
(vol*ββͺ π β β (πβπ)))) |
157 | 154, 156 | mpbid 231 |
. . . . 5
β’ ((π β§ 0 < (vol*βran
πΉ)) β Β¬ 3 <
(vol*ββͺ π β β (πβπ))) |
158 | 134, 157 | pm2.65da 816 |
. . . 4
β’ (π β Β¬ 0 <
(vol*βran πΉ)) |
159 | | ovolge0 24861 |
. . . . . . 7
β’ (ran
πΉ β β β 0
β€ (vol*βran πΉ)) |
160 | 20, 159 | syl 17 |
. . . . . 6
β’ (π β 0 β€ (vol*βran
πΉ)) |
161 | | 0xr 11209 |
. . . . . . 7
β’ 0 β
β* |
162 | | ovolcl 24858 |
. . . . . . . 8
β’ (ran
πΉ β β β
(vol*βran πΉ) β
β*) |
163 | 20, 162 | syl 17 |
. . . . . . 7
β’ (π β (vol*βran πΉ) β
β*) |
164 | | xrleloe 13070 |
. . . . . . 7
β’ ((0
β β* β§ (vol*βran πΉ) β β*) β (0 β€
(vol*βran πΉ) β
(0 < (vol*βran πΉ)
β¨ 0 = (vol*βran πΉ)))) |
165 | 161, 163,
164 | sylancr 588 |
. . . . . 6
β’ (π β (0 β€ (vol*βran
πΉ) β (0 <
(vol*βran πΉ) β¨ 0 =
(vol*βran πΉ)))) |
166 | 160, 165 | mpbid 231 |
. . . . 5
β’ (π β (0 < (vol*βran
πΉ) β¨ 0 = (vol*βran
πΉ))) |
167 | 166 | ord 863 |
. . . 4
β’ (π β (Β¬ 0 <
(vol*βran πΉ) β 0
= (vol*βran πΉ))) |
168 | 158, 167 | mpd 15 |
. . 3
β’ (π β 0 = (vol*βran πΉ)) |
169 | 168 | adantr 482 |
. 2
β’ ((π β§ π β β) β 0 = (vol*βran
πΉ)) |
170 | 33, 169 | eqtr4d 2780 |
1
β’ ((π β§ π β β) β (vol*β(πβπ)) = 0) |