Step | Hyp | Ref
| Expression |
1 | | inss1 4192 |
. . . 4
β’ (πΈ β© π΄) β πΈ |
2 | | uniioombl.s |
. . . . 5
β’ (π β πΈ β βͺ ran
((,) β πΊ)) |
3 | | uniioombl.g |
. . . . . . . 8
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
4 | 3 | uniiccdif 24965 |
. . . . . . 7
β’ (π β (βͺ ran ((,) β πΊ) β βͺ ran
([,] β πΊ) β§
(vol*β(βͺ ran ([,] β πΊ) β βͺ ran
((,) β πΊ))) =
0)) |
5 | 4 | simpld 496 |
. . . . . 6
β’ (π β βͺ ran ((,) β πΊ) β βͺ ran
([,] β πΊ)) |
6 | | ovolficcss 24856 |
. . . . . . 7
β’ (πΊ:ββΆ( β€ β©
(β Γ β)) β βͺ ran ([,] β
πΊ) β
β) |
7 | 3, 6 | syl 17 |
. . . . . 6
β’ (π β βͺ ran ([,] β πΊ) β β) |
8 | 5, 7 | sstrd 3958 |
. . . . 5
β’ (π β βͺ ran ((,) β πΊ) β β) |
9 | 2, 8 | sstrd 3958 |
. . . 4
β’ (π β πΈ β β) |
10 | | uniioombl.e |
. . . 4
β’ (π β (vol*βπΈ) β
β) |
11 | | ovolsscl 24873 |
. . . 4
β’ (((πΈ β© π΄) β πΈ β§ πΈ β β β§ (vol*βπΈ) β β) β
(vol*β(πΈ β© π΄)) β
β) |
12 | 1, 9, 10, 11 | mp3an2i 1467 |
. . 3
β’ (π β (vol*β(πΈ β© π΄)) β β) |
13 | | difssd 4096 |
. . . 4
β’ (π β (πΈ β π΄) β πΈ) |
14 | | ovolsscl 24873 |
. . . 4
β’ (((πΈ β π΄) β πΈ β§ πΈ β β β§ (vol*βπΈ) β β) β
(vol*β(πΈ β
π΄)) β
β) |
15 | 13, 9, 10, 14 | syl3anc 1372 |
. . 3
β’ (π β (vol*β(πΈ β π΄)) β β) |
16 | 12, 15 | readdcld 11192 |
. 2
β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β β) |
17 | | inss1 4192 |
. . . . 5
β’ (πΎ β© π΄) β πΎ |
18 | | uniioombl.k |
. . . . . . 7
β’ πΎ = βͺ
(((,) β πΊ) β
(1...π)) |
19 | | imassrn 6028 |
. . . . . . . 8
β’ (((,)
β πΊ) β
(1...π)) β ran ((,)
β πΊ) |
20 | 19 | unissi 4878 |
. . . . . . 7
β’ βͺ (((,) β πΊ) β (1...π)) β βͺ ran
((,) β πΊ) |
21 | 18, 20 | eqsstri 3982 |
. . . . . 6
β’ πΎ β βͺ ran ((,) β πΊ) |
22 | 21, 8 | sstrid 3959 |
. . . . 5
β’ (π β πΎ β β) |
23 | | uniioombl.1 |
. . . . . . . 8
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
24 | | uniioombl.2 |
. . . . . . . 8
β’ (π β Disj π₯ β β
((,)β(πΉβπ₯))) |
25 | | uniioombl.3 |
. . . . . . . 8
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
26 | | uniioombl.a |
. . . . . . . 8
β’ π΄ = βͺ
ran ((,) β πΉ) |
27 | | uniioombl.c |
. . . . . . . 8
β’ (π β πΆ β
β+) |
28 | | uniioombl.t |
. . . . . . . 8
β’ π = seq1( + , ((abs β
β ) β πΊ)) |
29 | | uniioombl.v |
. . . . . . . 8
β’ (π β sup(ran π, β*, < ) β€
((vol*βπΈ) + πΆ)) |
30 | 23, 24, 25, 26, 10, 27, 3, 2, 28, 29 | uniioombllem1 24968 |
. . . . . . 7
β’ (π β sup(ran π, β*, < ) β
β) |
31 | | ssid 3970 |
. . . . . . . 8
β’ βͺ ran ((,) β πΊ) β βͺ ran
((,) β πΊ) |
32 | 28 | ovollb 24866 |
. . . . . . . 8
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ βͺ ran ((,) β
πΊ) β βͺ ran ((,) β πΊ)) β (vol*ββͺ ran ((,) β πΊ)) β€ sup(ran π, β*, <
)) |
33 | 3, 31, 32 | sylancl 587 |
. . . . . . 7
β’ (π β (vol*ββͺ ran ((,) β πΊ)) β€ sup(ran π, β*, <
)) |
34 | | ovollecl 24870 |
. . . . . . 7
β’ ((βͺ ran ((,) β πΊ) β β β§ sup(ran π, β*, < )
β β β§ (vol*ββͺ ran ((,) β
πΊ)) β€ sup(ran π, β*, < ))
β (vol*ββͺ ran ((,) β πΊ)) β
β) |
35 | 8, 30, 33, 34 | syl3anc 1372 |
. . . . . 6
β’ (π β (vol*ββͺ ran ((,) β πΊ)) β β) |
36 | | ovolsscl 24873 |
. . . . . 6
β’ ((πΎ β βͺ ran ((,) β πΊ) β§ βͺ ran
((,) β πΊ) β
β β§ (vol*ββͺ ran ((,) β πΊ)) β β) β
(vol*βπΎ) β
β) |
37 | 21, 8, 35, 36 | mp3an2i 1467 |
. . . . 5
β’ (π β (vol*βπΎ) β
β) |
38 | | ovolsscl 24873 |
. . . . 5
β’ (((πΎ β© π΄) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β© π΄)) β
β) |
39 | 17, 22, 37, 38 | mp3an2i 1467 |
. . . 4
β’ (π β (vol*β(πΎ β© π΄)) β β) |
40 | | difssd 4096 |
. . . . 5
β’ (π β (πΎ β π΄) β πΎ) |
41 | | ovolsscl 24873 |
. . . . 5
β’ (((πΎ β π΄) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β
π΄)) β
β) |
42 | 40, 22, 37, 41 | syl3anc 1372 |
. . . 4
β’ (π β (vol*β(πΎ β π΄)) β β) |
43 | 39, 42 | readdcld 11192 |
. . 3
β’ (π β ((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) β β) |
44 | 27 | rpred 12965 |
. . . 4
β’ (π β πΆ β β) |
45 | 44, 44 | readdcld 11192 |
. . 3
β’ (π β (πΆ + πΆ) β β) |
46 | 43, 45 | readdcld 11192 |
. 2
β’ (π β (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ)) β β) |
47 | | 4re 12245 |
. . . 4
β’ 4 β
β |
48 | | remulcl 11144 |
. . . 4
β’ ((4
β β β§ πΆ
β β) β (4 Β· πΆ) β β) |
49 | 47, 44, 48 | sylancr 588 |
. . 3
β’ (π β (4 Β· πΆ) β
β) |
50 | 10, 49 | readdcld 11192 |
. 2
β’ (π β ((vol*βπΈ) + (4 Β· πΆ)) β
β) |
51 | | uniioombl.m |
. . . 4
β’ (π β π β β) |
52 | | uniioombl.m2 |
. . . 4
β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) |
53 | 23, 24, 25, 26, 10, 27, 3, 2, 28, 29, 51, 52, 18 | uniioombllem3 24972 |
. . 3
β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) < (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ))) |
54 | 16, 46, 53 | ltled 11311 |
. 2
β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ))) |
55 | 10, 45 | readdcld 11192 |
. . . 4
β’ (π β ((vol*βπΈ) + (πΆ + πΆ)) β β) |
56 | 37, 44 | readdcld 11192 |
. . . . 5
β’ (π β ((vol*βπΎ) + πΆ) β β) |
57 | | inss1 4192 |
. . . . . . . . 9
β’ (πΎ β© πΏ) β πΎ |
58 | | ovolsscl 24873 |
. . . . . . . . 9
β’ (((πΎ β© πΏ) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β© πΏ)) β
β) |
59 | 57, 22, 37, 58 | mp3an2i 1467 |
. . . . . . . 8
β’ (π β (vol*β(πΎ β© πΏ)) β β) |
60 | 59, 44 | readdcld 11192 |
. . . . . . 7
β’ (π β ((vol*β(πΎ β© πΏ)) + πΆ) β β) |
61 | | difssd 4096 |
. . . . . . . 8
β’ (π β (πΎ β πΏ) β πΎ) |
62 | | ovolsscl 24873 |
. . . . . . . 8
β’ (((πΎ β πΏ) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β
πΏ)) β
β) |
63 | 61, 22, 37, 62 | syl3anc 1372 |
. . . . . . 7
β’ (π β (vol*β(πΎ β πΏ)) β β) |
64 | | uniioombl.n |
. . . . . . . 8
β’ (π β π β β) |
65 | | uniioombl.n2 |
. . . . . . . 8
β’ (π β βπ β (1...π)(absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) |
66 | | uniioombl.l |
. . . . . . . 8
β’ πΏ = βͺ
(((,) β πΉ) β
(1...π)) |
67 | 23, 24, 25, 26, 10, 27, 3, 2, 28, 29, 51, 52, 18, 64, 65, 66 | uniioombllem4 24973 |
. . . . . . 7
β’ (π β (vol*β(πΎ β© π΄)) β€ ((vol*β(πΎ β© πΏ)) + πΆ)) |
68 | | imassrn 6028 |
. . . . . . . . . . 11
β’ (((,)
β πΉ) β
(1...π)) β ran ((,)
β πΉ) |
69 | 68 | unissi 4878 |
. . . . . . . . . 10
β’ βͺ (((,) β πΉ) β (1...π)) β βͺ ran
((,) β πΉ) |
70 | 69, 66, 26 | 3sstr4i 3991 |
. . . . . . . . 9
β’ πΏ β π΄ |
71 | | sscon 4102 |
. . . . . . . . 9
β’ (πΏ β π΄ β (πΎ β π΄) β (πΎ β πΏ)) |
72 | 70, 71 | mp1i 13 |
. . . . . . . 8
β’ (π β (πΎ β π΄) β (πΎ β πΏ)) |
73 | 61, 22 | sstrd 3958 |
. . . . . . . 8
β’ (π β (πΎ β πΏ) β β) |
74 | | ovolss 24872 |
. . . . . . . 8
β’ (((πΎ β π΄) β (πΎ β πΏ) β§ (πΎ β πΏ) β β) β (vol*β(πΎ β π΄)) β€ (vol*β(πΎ β πΏ))) |
75 | 72, 73, 74 | syl2anc 585 |
. . . . . . 7
β’ (π β (vol*β(πΎ β π΄)) β€ (vol*β(πΎ β πΏ))) |
76 | 39, 42, 60, 63, 67, 75 | le2addd 11782 |
. . . . . 6
β’ (π β ((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) β€ (((vol*β(πΎ β© πΏ)) + πΆ) + (vol*β(πΎ β πΏ)))) |
77 | 59 | recnd 11191 |
. . . . . . . 8
β’ (π β (vol*β(πΎ β© πΏ)) β β) |
78 | 44 | recnd 11191 |
. . . . . . . 8
β’ (π β πΆ β β) |
79 | 63 | recnd 11191 |
. . . . . . . 8
β’ (π β (vol*β(πΎ β πΏ)) β β) |
80 | 77, 78, 79 | add32d 11390 |
. . . . . . 7
β’ (π β (((vol*β(πΎ β© πΏ)) + πΆ) + (vol*β(πΎ β πΏ))) = (((vol*β(πΎ β© πΏ)) + (vol*β(πΎ β πΏ))) + πΆ)) |
81 | | ioof 13373 |
. . . . . . . . . . . . 13
β’
(,):(β* Γ β*)βΆπ«
β |
82 | | inss2 4193 |
. . . . . . . . . . . . . . 15
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
83 | | rexpssxrxp 11208 |
. . . . . . . . . . . . . . 15
β’ (β
Γ β) β (β* Γ
β*) |
84 | 82, 83 | sstri 3957 |
. . . . . . . . . . . . . 14
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
85 | | fss 6689 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
86 | 23, 84, 85 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆ(β* Γ
β*)) |
87 | | fco 6696 |
. . . . . . . . . . . . 13
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΉ:ββΆ(β* Γ
β*)) β ((,) β πΉ):ββΆπ«
β) |
88 | 81, 86, 87 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β ((,) β πΉ):ββΆπ«
β) |
89 | | ffun 6675 |
. . . . . . . . . . . 12
β’ (((,)
β πΉ):ββΆπ« β β
Fun ((,) β πΉ)) |
90 | | funiunfv 7199 |
. . . . . . . . . . . 12
β’ (Fun ((,)
β πΉ) β βͺ π β (1...π)(((,) β πΉ)βπ) = βͺ (((,)
β πΉ) β
(1...π))) |
91 | 88, 89, 90 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β βͺ π β (1...π)(((,) β πΉ)βπ) = βͺ (((,)
β πΉ) β
(1...π))) |
92 | 91, 66 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π β βͺ π β (1...π)(((,) β πΉ)βπ) = πΏ) |
93 | | fzfid 13887 |
. . . . . . . . . . 11
β’ (π β (1...π) β Fin) |
94 | | elfznn 13479 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β π β β) |
95 | | fvco3 6944 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((,) β πΉ)βπ) = ((,)β(πΉβπ))) |
96 | 23, 94, 95 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (((,) β πΉ)βπ) = ((,)β(πΉβπ))) |
97 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) β ( β€ β© (β Γ
β))) |
98 | 23, 94, 97 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (πΉβπ) β ( β€ β© (β Γ
β))) |
99 | 98 | elin2d 4163 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β (πΉβπ) β (β Γ
β)) |
100 | | 1st2nd2 7964 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β (β Γ β) β
(πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
102 | 101 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((,)β(πΉβπ)) = ((,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©)) |
103 | | df-ov 7364 |
. . . . . . . . . . . . . . 15
β’
((1st β(πΉβπ))(,)(2nd β(πΉβπ))) = ((,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©) |
104 | 102, 103 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((,)β(πΉβπ)) = ((1st β(πΉβπ))(,)(2nd β(πΉβπ)))) |
105 | 96, 104 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (((,) β πΉ)βπ) = ((1st β(πΉβπ))(,)(2nd β(πΉβπ)))) |
106 | | ioombl 24952 |
. . . . . . . . . . . . 13
β’
((1st β(πΉβπ))(,)(2nd β(πΉβπ))) β dom vol |
107 | 105, 106 | eqeltrdi 2842 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (((,) β πΉ)βπ) β dom vol) |
108 | 107 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β (1...π)(((,) β πΉ)βπ) β dom vol) |
109 | | finiunmbl 24931 |
. . . . . . . . . . 11
β’
(((1...π) β Fin
β§ βπ β
(1...π)(((,) β πΉ)βπ) β dom vol) β βͺ π β (1...π)(((,) β πΉ)βπ) β dom vol) |
110 | 93, 108, 109 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β βͺ π β (1...π)(((,) β πΉ)βπ) β dom vol) |
111 | 92, 110 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΏ β dom vol) |
112 | | mblsplit 24919 |
. . . . . . . . 9
β’ ((πΏ β dom vol β§ πΎ β β β§
(vol*βπΎ) β
β) β (vol*βπΎ) = ((vol*β(πΎ β© πΏ)) + (vol*β(πΎ β πΏ)))) |
113 | 111, 22, 37, 112 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (vol*βπΎ) = ((vol*β(πΎ β© πΏ)) + (vol*β(πΎ β πΏ)))) |
114 | 113 | oveq1d 7376 |
. . . . . . 7
β’ (π β ((vol*βπΎ) + πΆ) = (((vol*β(πΎ β© πΏ)) + (vol*β(πΎ β πΏ))) + πΆ)) |
115 | 80, 114 | eqtr4d 2776 |
. . . . . 6
β’ (π β (((vol*β(πΎ β© πΏ)) + πΆ) + (vol*β(πΎ β πΏ))) = ((vol*βπΎ) + πΆ)) |
116 | 76, 115 | breqtrd 5135 |
. . . . 5
β’ (π β ((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) β€ ((vol*βπΎ) + πΆ)) |
117 | 10, 44 | readdcld 11192 |
. . . . . . 7
β’ (π β ((vol*βπΈ) + πΆ) β β) |
118 | 28 | ovollb 24866 |
. . . . . . . . 9
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ πΎ β βͺ ran
((,) β πΊ)) β
(vol*βπΎ) β€ sup(ran
π, β*,
< )) |
119 | 3, 21, 118 | sylancl 587 |
. . . . . . . 8
β’ (π β (vol*βπΎ) β€ sup(ran π, β*, <
)) |
120 | 37, 30, 117, 119, 29 | letrd 11320 |
. . . . . . 7
β’ (π β (vol*βπΎ) β€ ((vol*βπΈ) + πΆ)) |
121 | 37, 117, 44, 120 | leadd1dd 11777 |
. . . . . 6
β’ (π β ((vol*βπΎ) + πΆ) β€ (((vol*βπΈ) + πΆ) + πΆ)) |
122 | 10 | recnd 11191 |
. . . . . . 7
β’ (π β (vol*βπΈ) β
β) |
123 | 122, 78, 78 | addassd 11185 |
. . . . . 6
β’ (π β (((vol*βπΈ) + πΆ) + πΆ) = ((vol*βπΈ) + (πΆ + πΆ))) |
124 | 121, 123 | breqtrd 5135 |
. . . . 5
β’ (π β ((vol*βπΎ) + πΆ) β€ ((vol*βπΈ) + (πΆ + πΆ))) |
125 | 43, 56, 55, 116, 124 | letrd 11320 |
. . . 4
β’ (π β ((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) β€ ((vol*βπΈ) + (πΆ + πΆ))) |
126 | 43, 55, 45, 125 | leadd1dd 11777 |
. . 3
β’ (π β (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ)) β€ (((vol*βπΈ) + (πΆ + πΆ)) + (πΆ + πΆ))) |
127 | 45 | recnd 11191 |
. . . . 5
β’ (π β (πΆ + πΆ) β β) |
128 | 122, 127,
127 | addassd 11185 |
. . . 4
β’ (π β (((vol*βπΈ) + (πΆ + πΆ)) + (πΆ + πΆ)) = ((vol*βπΈ) + ((πΆ + πΆ) + (πΆ + πΆ)))) |
129 | | 2t2e4 12325 |
. . . . . . 7
β’ (2
Β· 2) = 4 |
130 | 129 | oveq1i 7371 |
. . . . . 6
β’ ((2
Β· 2) Β· πΆ) =
(4 Β· πΆ) |
131 | | 2cnd 12239 |
. . . . . . . 8
β’ (π β 2 β
β) |
132 | 131, 131,
78 | mulassd 11186 |
. . . . . . 7
β’ (π β ((2 Β· 2) Β·
πΆ) = (2 Β· (2
Β· πΆ))) |
133 | 78 | 2timesd 12404 |
. . . . . . . 8
β’ (π β (2 Β· πΆ) = (πΆ + πΆ)) |
134 | 133 | oveq2d 7377 |
. . . . . . 7
β’ (π β (2 Β· (2 Β·
πΆ)) = (2 Β· (πΆ + πΆ))) |
135 | 127 | 2timesd 12404 |
. . . . . . 7
β’ (π β (2 Β· (πΆ + πΆ)) = ((πΆ + πΆ) + (πΆ + πΆ))) |
136 | 132, 134,
135 | 3eqtrd 2777 |
. . . . . 6
β’ (π β ((2 Β· 2) Β·
πΆ) = ((πΆ + πΆ) + (πΆ + πΆ))) |
137 | 130, 136 | eqtr3id 2787 |
. . . . 5
β’ (π β (4 Β· πΆ) = ((πΆ + πΆ) + (πΆ + πΆ))) |
138 | 137 | oveq2d 7377 |
. . . 4
β’ (π β ((vol*βπΈ) + (4 Β· πΆ)) = ((vol*βπΈ) + ((πΆ + πΆ) + (πΆ + πΆ)))) |
139 | 128, 138 | eqtr4d 2776 |
. . 3
β’ (π β (((vol*βπΈ) + (πΆ + πΆ)) + (πΆ + πΆ)) = ((vol*βπΈ) + (4 Β· πΆ))) |
140 | 126, 139 | breqtrd 5135 |
. 2
β’ (π β (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ)) β€ ((vol*βπΈ) + (4 Β· πΆ))) |
141 | 16, 46, 50, 54, 140 | letrd 11320 |
1
β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) |