Step | Hyp | Ref
| Expression |
1 | | ovnsubaddlem1.x |
. . . 4
β’ (π β π β Fin) |
2 | | ovnsubaddlem1.a |
. . . . . . . . 9
β’ (π β π΄:ββΆπ« (β
βm π)) |
3 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π΄:ββΆπ« (β
βm π)) |
4 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
5 | 3, 4 | ffvelcdmd 7083 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄βπ) β π« (β
βm π)) |
6 | | elpwi 4608 |
. . . . . . 7
β’ ((π΄βπ) β π« (β
βm π)
β (π΄βπ) β (β
βm π)) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β (π΄βπ) β (β βm π)) |
8 | 7 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ β β (π΄βπ) β (β βm π)) |
9 | | iunss 5047 |
. . . . 5
β’ (βͺ π β β (π΄βπ) β (β βm π) β βπ β β (π΄βπ) β (β βm π)) |
10 | 8, 9 | sylibr 233 |
. . . 4
β’ (π β βͺ π β β (π΄βπ) β (β βm π)) |
11 | 1, 10 | ovnxrcl 45220 |
. . 3
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β
β*) |
12 | | nfv 1918 |
. . . 4
β’
β²ππ |
13 | | nnex 12214 |
. . . . 5
β’ β
β V |
14 | 13 | a1i 11 |
. . . 4
β’ (π β β β
V) |
15 | | icossicc 13409 |
. . . . 5
β’
(0[,)+β) β (0[,]+β) |
16 | | nfv 1918 |
. . . . . 6
β’
β²π(π β§ π β β) |
17 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π β β) β π) |
18 | 17, 1 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β π β Fin) |
19 | | ovnsubaddlem1.l |
. . . . . 6
β’ πΏ = (π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ))) |
20 | | ovnsubaddlem1.f |
. . . . . . . . . . . 12
β’ (π β πΉ:ββ1-1-ontoβ(β Γ β)) |
21 | | f1of 6830 |
. . . . . . . . . . . 12
β’ (πΉ:ββ1-1-ontoβ(β Γ β) β πΉ:ββΆ(β Γ
β)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆ(β Γ
β)) |
23 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β πΉ:ββΆ(β Γ
β)) |
24 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
25 | 23, 24 | ffvelcdmd 7083 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) β (β Γ
β)) |
26 | | xp1st 8002 |
. . . . . . . . 9
β’ ((πΉβπ) β (β Γ β) β
(1st β(πΉβπ)) β β) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (1st
β(πΉβπ)) β
β) |
28 | | xp2nd 8003 |
. . . . . . . . 9
β’ ((πΉβπ) β (β Γ β) β
(2nd β(πΉβπ)) β β) |
29 | 25, 28 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (2nd
β(πΉβπ)) β
β) |
30 | | fvex 6901 |
. . . . . . . . 9
β’
(2nd β(πΉβπ)) β V |
31 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = (2nd β(πΉβπ)) β (π β β β (2nd
β(πΉβπ)) β
β)) |
32 | 31 | 3anbi3d 1443 |
. . . . . . . . . 10
β’ (π = (2nd β(πΉβπ)) β ((π β§ (1st β(πΉβπ)) β β β§ π β β) β (π β§ (1st β(πΉβπ)) β β β§ (2nd
β(πΉβπ)) β
β))) |
33 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π = (2nd β(πΉβπ)) β ((πΌβ(1st β(πΉβπ)))βπ) = ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) |
34 | 33 | feq1d 6699 |
. . . . . . . . . 10
β’ (π = (2nd β(πΉβπ)) β (((πΌβ(1st β(πΉβπ)))βπ):πβΆ(β Γ β) β
((πΌβ(1st
β(πΉβπ)))β(2nd
β(πΉβπ))):πβΆ(β Γ
β))) |
35 | 32, 34 | imbi12d 345 |
. . . . . . . . 9
β’ (π = (2nd β(πΉβπ)) β (((π β§ (1st β(πΉβπ)) β β β§ π β β) β ((πΌβ(1st β(πΉβπ)))βπ):πβΆ(β Γ β)) β
((π β§ (1st
β(πΉβπ)) β β β§
(2nd β(πΉβπ)) β β) β ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))):πβΆ(β Γ
β)))) |
36 | | fvex 6901 |
. . . . . . . . . 10
β’
(1st β(πΉβπ)) β V |
37 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = (1st β(πΉβπ)) β (π β β β (1st
β(πΉβπ)) β
β)) |
38 | 37 | 3anbi2d 1442 |
. . . . . . . . . . 11
β’ (π = (1st β(πΉβπ)) β ((π β§ π β β β§ π β β) β (π β§ (1st β(πΉβπ)) β β β§ π β β))) |
39 | | fveq2 6888 |
. . . . . . . . . . . . 13
β’ (π = (1st β(πΉβπ)) β (πΌβπ) = (πΌβ(1st β(πΉβπ)))) |
40 | 39 | fveq1d 6890 |
. . . . . . . . . . . 12
β’ (π = (1st β(πΉβπ)) β ((πΌβπ)βπ) = ((πΌβ(1st β(πΉβπ)))βπ)) |
41 | 40 | feq1d 6699 |
. . . . . . . . . . 11
β’ (π = (1st β(πΉβπ)) β (((πΌβπ)βπ):πβΆ(β Γ β) β
((πΌβ(1st
β(πΉβπ)))βπ):πβΆ(β Γ
β))) |
42 | 38, 41 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = (1st β(πΉβπ)) β (((π β§ π β β β§ π β β) β ((πΌβπ)βπ):πβΆ(β Γ β)) β
((π β§ (1st
β(πΉβπ)) β β β§ π β β) β ((πΌβ(1st
β(πΉβπ)))βπ):πβΆ(β Γ
β)))) |
43 | | ovnsubaddlem1.c |
. . . . . . . . . . . . . . . . . . 19
β’ πΆ = (π β π« (β βm
π) β¦ {β β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (ββπ))βπ)}) |
44 | | sseq1 4006 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π΄βπ) β (π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ))) |
45 | 44 | rabbidv 3441 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π΄βπ) β {β β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} = {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)}) |
46 | | ovex 7437 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β Γ β) βm π) βm β) β
V |
47 | 46 | rabex 5331 |
. . . . . . . . . . . . . . . . . . . 20
β’ {β β (((β Γ
β) βm π) βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} β V |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} β V) |
49 | 43, 45, 5, 48 | fvmptd3 7017 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (πΆβ(π΄βπ)) = {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)}) |
50 | | ssrab2 4076 |
. . . . . . . . . . . . . . . . . . 19
β’ {β β (((β Γ
β) βm π) βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} β (((β Γ β)
βm π)
βm β) |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} β (((β Γ β)
βm π)
βm β)) |
52 | 49, 51 | eqsstrd 4019 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΆβ(π΄βπ)) β (((β Γ β)
βm π)
βm β)) |
53 | | ovnsubaddlem1.d |
. . . . . . . . . . . . . . . . . . . . 21
β’ π· = (π β π« (β βm
π) β¦ (π β β+
β¦ {π β (πΆβπ) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) |
54 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π΄βπ) β (πΆβπ) = (πΆβ(π΄βπ))) |
55 | 54 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π΄βπ) β (π β (πΆβπ) β π β (πΆβ(π΄βπ)))) |
56 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π΄βπ) β ((voln*βπ)βπ) = ((voln*βπ)β(π΄βπ))) |
57 | 56 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π΄βπ) β (((voln*βπ)βπ) +π π) = (((voln*βπ)β(π΄βπ)) +π π)) |
58 | 57 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π΄βπ) β
((Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π) β
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π))) |
59 | 55, 58 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π΄βπ) β ((π β (πΆβπ) β§
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)) β (π β (πΆβ(π΄βπ)) β§
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)))) |
60 | 59 | rabbidva2 3435 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π΄βπ) β {π β (πΆβπ) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)} = {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)}) |
61 | 60 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π΄βπ) β (π β β+ β¦ {π β (πΆβπ) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) = (π β β+ β¦ {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)})) |
62 | | rpex 43991 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β+ β V |
63 | 62 | mptex 7220 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β+
β¦ {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)}) β V |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β (π β β+ β¦ {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)}) β V) |
65 | 53, 61, 5, 64 | fvmptd3 7017 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (π·β(π΄βπ)) = (π β β+ β¦ {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)})) |
66 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πΈ / (2βπ)) β (((voln*βπ)β(π΄βπ)) +π π) = (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))) |
67 | 66 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πΈ / (2βπ)) β
((Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π) β
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) |
68 | 67 | rabbidv 3441 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πΈ / (2βπ)) β {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)} = {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))}) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π = (πΈ / (2βπ))) β {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π π)} = {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))}) |
70 | | ovnsubaddlem1.e |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΈ β
β+) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β πΈ β
β+) |
72 | | 2nn 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 2 β
β |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 2 β
β) |
74 | | nnnn0 12475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β π β
β0) |
75 | 73, 74 | nnexpcld 14204 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β
(2βπ) β
β) |
76 | 75 | nnrpd 13010 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β
(2βπ) β
β+) |
77 | 76 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β (2βπ) β
β+) |
78 | 71, 77 | rpdivcld 13029 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (πΈ / (2βπ)) β
β+) |
79 | | fvex 6901 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΆβ(π΄βπ)) β V |
80 | 79 | rabex 5331 |
. . . . . . . . . . . . . . . . . . . . 21
β’ {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))} β V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))} β V) |
82 | 65, 69, 78, 81 | fvmptd 7001 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((π·β(π΄βπ))β(πΈ / (2βπ))) = {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))}) |
83 | | ssrab2 4076 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))} β (πΆβ(π΄βπ)) |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))} β (πΆβ(π΄βπ))) |
85 | 82, 84 | eqsstrd 4019 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β (πΆβ(π΄βπ))) |
86 | | ovnsubaddlem1.i |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (πΌβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
87 | 85, 86 | sseldd 3982 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΌβπ) β (πΆβ(π΄βπ))) |
88 | 52, 87 | sseldd 3982 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΌβπ) β (((β Γ β)
βm π)
βm β)) |
89 | | elmapfn 8855 |
. . . . . . . . . . . . . . . 16
β’ ((πΌβπ) β (((β Γ β)
βm π)
βm β) β (πΌβπ) Fn β) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΌβπ) Fn β) |
91 | | elmapi 8839 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌβπ) β (((β Γ β)
βm π)
βm β) β (πΌβπ):ββΆ((β Γ β)
βm π)) |
92 | 88, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΌβπ):ββΆ((β Γ β)
βm π)) |
93 | 92 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β) β ((πΌβπ)βπ) β ((β Γ β)
βm π)) |
94 | 93 | ralrimiva 3147 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β βπ β β ((πΌβπ)βπ) β ((β Γ β)
βm π)) |
95 | 90, 94 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πΌβπ) Fn β β§ βπ β β ((πΌβπ)βπ) β ((β Γ β)
βm π))) |
96 | 95 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β β§ π β β) β ((πΌβπ) Fn β β§ βπ β β ((πΌβπ)βπ) β ((β Γ β)
βm π))) |
97 | | ffnfv 7113 |
. . . . . . . . . . . . 13
β’ ((πΌβπ):ββΆ((β Γ β)
βm π)
β ((πΌβπ) Fn β β§ βπ β β ((πΌβπ)βπ) β ((β Γ β)
βm π))) |
98 | 96, 97 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π β§ π β β β§ π β β) β (πΌβπ):ββΆ((β Γ β)
βm π)) |
99 | | simp3 1139 |
. . . . . . . . . . . 12
β’ ((π β§ π β β β§ π β β) β π β β) |
100 | 98, 99 | ffvelcdmd 7083 |
. . . . . . . . . . 11
β’ ((π β§ π β β β§ π β β) β ((πΌβπ)βπ) β ((β Γ β)
βm π)) |
101 | | elmapi 8839 |
. . . . . . . . . . 11
β’ (((πΌβπ)βπ) β ((β Γ β)
βm π)
β ((πΌβπ)βπ):πβΆ(β Γ
β)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π β β) β ((πΌβπ)βπ):πβΆ(β Γ
β)) |
103 | 36, 42, 102 | vtocl 3549 |
. . . . . . . . 9
β’ ((π β§ (1st
β(πΉβπ)) β β β§ π β β) β ((πΌβ(1st
β(πΉβπ)))βπ):πβΆ(β Γ
β)) |
104 | 30, 35, 103 | vtocl 3549 |
. . . . . . . 8
β’ ((π β§ (1st
β(πΉβπ)) β β β§
(2nd β(πΉβπ)) β β) β ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))):πβΆ(β Γ
β)) |
105 | 17, 27, 29, 104 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))):πβΆ(β Γ
β)) |
106 | | id 22 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
107 | | fvex 6901 |
. . . . . . . . . . 11
β’ ((πΌβ(1st
β(πΉβπ)))β(2nd
β(πΉβπ))) β V |
108 | 107 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β ((πΌβ(1st
β(πΉβπ)))β(2nd
β(πΉβπ))) β V) |
109 | | ovnsubaddlem1.g |
. . . . . . . . . . 11
β’ πΊ = (π β β β¦ ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) |
110 | 109 | fvmpt2 7005 |
. . . . . . . . . 10
β’ ((π β β β§ ((πΌβ(1st
β(πΉβπ)))β(2nd
β(πΉβπ))) β V) β (πΊβπ) = ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) |
111 | 106, 108,
110 | syl2anc 585 |
. . . . . . . . 9
β’ (π β β β (πΊβπ) = ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) |
112 | 111 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΊβπ) = ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) |
113 | 112 | feq1d 6699 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΊβπ):πβΆ(β Γ β) β
((πΌβ(1st
β(πΉβπ)))β(2nd
β(πΉβπ))):πβΆ(β Γ
β))) |
114 | 105, 113 | mpbird 257 |
. . . . . 6
β’ ((π β§ π β β) β (πΊβπ):πβΆ(β Γ
β)) |
115 | 16, 18, 19, 114 | hoiprodcl2 45206 |
. . . . 5
β’ ((π β§ π β β) β (πΏβ(πΊβπ)) β (0[,)+β)) |
116 | 15, 115 | sselid 3979 |
. . . 4
β’ ((π β§ π β β) β (πΏβ(πΊβπ)) β (0[,]+β)) |
117 | 12, 14, 116 | sge0xrclmpt 45079 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ (πΏβ(πΊβπ)))) β
β*) |
118 | | nfv 1918 |
. . . 4
β’
β²ππ |
119 | | 0xr 11257 |
. . . . . 6
β’ 0 β
β* |
120 | 119 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β 0 β
β*) |
121 | | pnfxr 11264 |
. . . . . 6
β’ +β
β β* |
122 | 121 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β +β β
β*) |
123 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β Fin) |
124 | | ovnsubaddlem1.z |
. . . . . . . . 9
β’ π = (π β π« (β βm
π) β¦ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
125 | 123, 7, 124 | ovnval2b 45203 |
. . . . . . . 8
β’ ((π β§ π β β) β ((voln*βπ)β(π΄βπ)) = if(π = β
, 0, inf((πβ(π΄βπ)), β*, <
))) |
126 | | ovnsubaddlem1.n0 |
. . . . . . . . . . 11
β’ (π β π β β
) |
127 | 126 | neneqd 2946 |
. . . . . . . . . 10
β’ (π β Β¬ π = β
) |
128 | 127 | iffalsed 4538 |
. . . . . . . . 9
β’ (π β if(π = β
, 0, inf((πβ(π΄βπ)), β*, < )) = inf((πβ(π΄βπ)), β*, <
)) |
129 | 128 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β if(π = β
, 0, inf((πβ(π΄βπ)), β*, < )) = inf((πβ(π΄βπ)), β*, <
)) |
130 | 125, 129 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β β) β ((voln*βπ)β(π΄βπ)) = inf((πβ(π΄βπ)), β*, <
)) |
131 | | sseq1 4006 |
. . . . . . . . . . . . 13
β’ (π = (π΄βπ) β (π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ))) |
132 | 131 | anbi1d 631 |
. . . . . . . . . . . 12
β’ (π = (π΄βπ) β ((π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β ((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
133 | 132 | rexbidv 3179 |
. . . . . . . . . . 11
β’ (π = (π΄βπ) β (βπ β (((β Γ β)
βm π)
βm β)(π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β βπ β (((β Γ β)
βm π)
βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
134 | 133 | rabbidv 3441 |
. . . . . . . . . 10
β’ (π = (π΄βπ) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} = {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
135 | | xrex 12967 |
. . . . . . . . . . . 12
β’
β* β V |
136 | 135 | rabex 5331 |
. . . . . . . . . . 11
β’ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β V |
137 | 136 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β V) |
138 | 124, 134,
5, 137 | fvmptd3 7017 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(π΄βπ)) = {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
139 | | ssrab2 4076 |
. . . . . . . . . 10
β’ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β
β* |
140 | 139 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β
β*) |
141 | 138, 140 | eqsstrd 4019 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβ(π΄βπ)) β
β*) |
142 | | infxrcl 13308 |
. . . . . . . 8
β’ ((πβ(π΄βπ)) β β* β
inf((πβ(π΄βπ)), β*, < ) β
β*) |
143 | 141, 142 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β inf((πβ(π΄βπ)), β*, < ) β
β*) |
144 | 130, 143 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π β β) β ((voln*βπ)β(π΄βπ)) β
β*) |
145 | 70 | rpred 13012 |
. . . . . . . . 9
β’ (π β πΈ β β) |
146 | 145 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β πΈ β β) |
147 | | 2re 12282 |
. . . . . . . . . . 11
β’ 2 β
β |
148 | 147 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β 2 β
β) |
149 | 148, 74 | reexpcld 14124 |
. . . . . . . . 9
β’ (π β β β
(2βπ) β
β) |
150 | 149 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β (2βπ) β
β) |
151 | 148 | recnd 11238 |
. . . . . . . . . 10
β’ (π β β β 2 β
β) |
152 | | 2ne0 12312 |
. . . . . . . . . . 11
β’ 2 β
0 |
153 | 152 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β 2 β
0) |
154 | | nnz 12575 |
. . . . . . . . . 10
β’ (π β β β π β
β€) |
155 | 151, 153,
154 | expne0d 14113 |
. . . . . . . . 9
β’ (π β β β
(2βπ) β
0) |
156 | 155 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β (2βπ) β 0) |
157 | 146, 150,
156 | redivcld 12038 |
. . . . . . 7
β’ ((π β§ π β β) β (πΈ / (2βπ)) β β) |
158 | 157 | rexrd 11260 |
. . . . . 6
β’ ((π β§ π β β) β (πΈ / (2βπ)) β
β*) |
159 | 144, 158 | xaddcld 13276 |
. . . . 5
β’ ((π β§ π β β) β (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))) β
β*) |
160 | 123, 7 | ovncl 45218 |
. . . . . . 7
β’ ((π β§ π β β) β ((voln*βπ)β(π΄βπ)) β (0[,]+β)) |
161 | | xrge0ge0 43992 |
. . . . . . 7
β’
(((voln*βπ)β(π΄βπ)) β (0[,]+β) β 0 β€
((voln*βπ)β(π΄βπ))) |
162 | 160, 161 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β 0 β€
((voln*βπ)β(π΄βπ))) |
163 | | 0red 11213 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 β
β) |
164 | 78 | rpgt0d 13015 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 < (πΈ / (2βπ))) |
165 | 163, 157,
164 | ltled 11358 |
. . . . . . . 8
β’ ((π β§ π β β) β 0 β€ (πΈ / (2βπ))) |
166 | 157 | ltpnfd 13097 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΈ / (2βπ)) < +β) |
167 | 158, 122,
166 | xrltled 13125 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΈ / (2βπ)) β€ +β) |
168 | 120, 122,
158, 165, 167 | eliccxrd 44175 |
. . . . . . 7
β’ ((π β§ π β β) β (πΈ / (2βπ)) β (0[,]+β)) |
169 | 144, 168 | xadd0ge 43965 |
. . . . . 6
β’ ((π β§ π β β) β ((voln*βπ)β(π΄βπ)) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))) |
170 | 120, 144,
159, 162, 169 | xrletrd 13137 |
. . . . 5
β’ ((π β§ π β β) β 0 β€
(((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))) |
171 | | pnfge 13106 |
. . . . . 6
β’
((((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))) β β* β
(((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))) β€ +β) |
172 | 159, 171 | syl 17 |
. . . . 5
β’ ((π β§ π β β) β (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))) β€ +β) |
173 | 120, 122,
159, 170, 172 | eliccxrd 44175 |
. . . 4
β’ ((π β§ π β β) β (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))) β (0[,]+β)) |
174 | 118, 14, 173 | sge0xrclmpt 45079 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) β
β*) |
175 | | sseq1 4006 |
. . . . . . . . . . . . 13
β’ (π = (π΄β(1st β(πΉβπ))) β (π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β (π΄β(1st β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ))) |
176 | 175 | rabbidv 3441 |
. . . . . . . . . . . 12
β’ (π = (π΄β(1st β(πΉβπ))) β {β β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} = {β β (((β Γ β)
βm π)
βm β) β£ (π΄β(1st β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ)}) |
177 | 2 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π΄:ββΆπ« (β
βm π)) |
178 | 177, 27 | ffvelcdmd 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π΄β(1st β(πΉβπ))) β π« (β
βm π)) |
179 | 46 | rabex 5331 |
. . . . . . . . . . . . 13
β’ {β β (((β Γ
β) βm π) βm β) β£ (π΄β(1st
β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ)} β V |
180 | 179 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β {β β (((β Γ β)
βm π)
βm β) β£ (π΄β(1st β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ)} β V) |
181 | 43, 176, 178, 180 | fvmptd3 7017 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΆβ(π΄β(1st β(πΉβπ)))) = {β β (((β Γ β)
βm π)
βm β) β£ (π΄β(1st β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ)}) |
182 | | ssrab2 4076 |
. . . . . . . . . . . 12
β’ {β β (((β Γ
β) βm π) βm β) β£ (π΄β(1st
β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ)} β (((β Γ β)
βm π)
βm β) |
183 | 182 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β {β β (((β Γ β)
βm π)
βm β) β£ (π΄β(1st β(πΉβπ))) β βͺ π β β Xπ β π (([,) β (ββπ))βπ)} β (((β Γ β)
βm π)
βm β)) |
184 | 181, 183 | eqsstrd 4019 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΆβ(π΄β(1st β(πΉβπ)))) β (((β Γ β)
βm π)
βm β)) |
185 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π΄β(1st β(πΉβπ))) β (πΆβπ) = (πΆβ(π΄β(1st β(πΉβπ))))) |
186 | 185 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π΄β(1st β(πΉβπ))) β (π β (πΆβπ) β π β (πΆβ(π΄β(1st β(πΉβπ)))))) |
187 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π΄β(1st β(πΉβπ))) β ((voln*βπ)βπ) = ((voln*βπ)β(π΄β(1st β(πΉβπ))))) |
188 | 187 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π΄β(1st β(πΉβπ))) β (((voln*βπ)βπ) +π π) = (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)) |
189 | 188 | breq2d 5159 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π΄β(1st β(πΉβπ))) β
((Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π) β
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π))) |
190 | 186, 189 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = (π΄β(1st β(πΉβπ))) β ((π β (πΆβπ) β§
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)) β (π β (πΆβ(π΄β(1st β(πΉβπ)))) β§
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)))) |
191 | 190 | rabbidva2 3435 |
. . . . . . . . . . . . . . 15
β’ (π = (π΄β(1st β(πΉβπ))) β {π β (πΆβπ) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)} = {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)}) |
192 | 191 | mpteq2dv 5249 |
. . . . . . . . . . . . . 14
β’ (π = (π΄β(1st β(πΉβπ))) β (π β β+ β¦ {π β (πΆβπ) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) = (π β β+ β¦ {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)})) |
193 | 62 | mptex 7220 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β¦ {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)}) β V |
194 | 193 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π β β+ β¦ {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)}) β V) |
195 | 53, 192, 178, 194 | fvmptd3 7017 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π·β(π΄β(1st β(πΉβπ)))) = (π β β+ β¦ {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)})) |
196 | | oveq2 7412 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΈ / (2β(1st β(πΉβπ)))) β (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π) = (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))) |
197 | 196 | breq2d 5159 |
. . . . . . . . . . . . . . 15
β’ (π = (πΈ / (2β(1st β(πΉβπ)))) β
((Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π) β
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ))))))) |
198 | 197 | rabbidv 3441 |
. . . . . . . . . . . . . 14
β’ (π = (πΈ / (2β(1st β(πΉβπ)))) β {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)} = {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))}) |
199 | 198 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π = (πΈ / (2β(1st β(πΉβπ))))) β {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π π)} = {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))}) |
200 | 17, 70 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β πΈ β
β+) |
201 | | 2rp 12975 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β+ |
202 | 201 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β 2 β
β+) |
203 | 27 | nnzd 12581 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (1st
β(πΉβπ)) β
β€) |
204 | 202, 203 | rpexpcld 14206 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β
(2β(1st β(πΉβπ))) β
β+) |
205 | 200, 204 | rpdivcld 13029 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΈ / (2β(1st β(πΉβπ)))) β
β+) |
206 | | fvex 6901 |
. . . . . . . . . . . . . . 15
β’ (πΆβ(π΄β(1st β(πΉβπ)))) β V |
207 | 206 | rabex 5331 |
. . . . . . . . . . . . . 14
β’ {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))} β V |
208 | 207 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))} β V) |
209 | 195, 199,
205, 208 | fvmptd 7001 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ))))) = {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))}) |
210 | | ssrab2 4076 |
. . . . . . . . . . . . 13
β’ {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))} β (πΆβ(π΄β(1st β(πΉβπ)))) |
211 | 210 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β {π β (πΆβ(π΄β(1st β(πΉβπ)))) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄β(1st β(πΉβπ)))) +π (πΈ / (2β(1st β(πΉβπ)))))} β (πΆβ(π΄β(1st β(πΉβπ))))) |
212 | 209, 211 | eqsstrd 4019 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ))))) β (πΆβ(π΄β(1st β(πΉβπ))))) |
213 | 37 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π = (1st β(πΉβπ)) β ((π β§ π β β) β (π β§ (1st β(πΉβπ)) β β))) |
214 | | 2fveq3 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = (1st β(πΉβπ)) β (π·β(π΄βπ)) = (π·β(π΄β(1st β(πΉβπ))))) |
215 | | oveq2 7412 |
. . . . . . . . . . . . . . . . 17
β’ (π = (1st β(πΉβπ)) β (2βπ) = (2β(1st β(πΉβπ)))) |
216 | 215 | oveq2d 7420 |
. . . . . . . . . . . . . . . 16
β’ (π = (1st β(πΉβπ)) β (πΈ / (2βπ)) = (πΈ / (2β(1st β(πΉβπ))))) |
217 | 214, 216 | fveq12d 6895 |
. . . . . . . . . . . . . . 15
β’ (π = (1st β(πΉβπ)) β ((π·β(π΄βπ))β(πΈ / (2βπ))) = ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ)))))) |
218 | 39, 217 | eleq12d 2828 |
. . . . . . . . . . . . . 14
β’ (π = (1st β(πΉβπ)) β ((πΌβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β (πΌβ(1st β(πΉβπ))) β ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ))))))) |
219 | 213, 218 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = (1st β(πΉβπ)) β (((π β§ π β β) β (πΌβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β ((π β§ (1st β(πΉβπ)) β β) β (πΌβ(1st β(πΉβπ))) β ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ)))))))) |
220 | 36, 219, 86 | vtocl 3549 |
. . . . . . . . . . . 12
β’ ((π β§ (1st
β(πΉβπ)) β β) β (πΌβ(1st
β(πΉβπ))) β ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ)))))) |
221 | 17, 27, 220 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΌβ(1st β(πΉβπ))) β ((π·β(π΄β(1st β(πΉβπ))))β(πΈ / (2β(1st β(πΉβπ)))))) |
222 | 212, 221 | sseldd 3982 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΌβ(1st β(πΉβπ))) β (πΆβ(π΄β(1st β(πΉβπ))))) |
223 | 184, 222 | sseldd 3982 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΌβ(1st β(πΉβπ))) β (((β Γ β)
βm π)
βm β)) |
224 | | elmapfn 8855 |
. . . . . . . . 9
β’ ((πΌβ(1st
β(πΉβπ))) β (((β Γ
β) βm π) βm β) β (πΌβ(1st
β(πΉβπ))) Fn β) |
225 | 223, 224 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΌβ(1st β(πΉβπ))) Fn β) |
226 | | elmapi 8839 |
. . . . . . . . . . 11
β’ ((πΌβ(1st
β(πΉβπ))) β (((β Γ
β) βm π) βm β) β (πΌβ(1st
β(πΉβπ))):ββΆ((β
Γ β) βm π)) |
227 | 223, 226 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΌβ(1st β(πΉβπ))):ββΆ((β Γ β)
βm π)) |
228 | 227 | ffvelcdmda 7082 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β ((πΌβ(1st β(πΉβπ)))βπ) β ((β Γ β)
βm π)) |
229 | 228 | ralrimiva 3147 |
. . . . . . . 8
β’ ((π β§ π β β) β βπ β β ((πΌβ(1st
β(πΉβπ)))βπ) β ((β Γ β)
βm π)) |
230 | 225, 229 | jca 513 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΌβ(1st β(πΉβπ))) Fn β β§ βπ β β ((πΌβ(1st
β(πΉβπ)))βπ) β ((β Γ β)
βm π))) |
231 | | ffnfv 7113 |
. . . . . . 7
β’ ((πΌβ(1st
β(πΉβπ))):ββΆ((β
Γ β) βm π) β ((πΌβ(1st β(πΉβπ))) Fn β β§ βπ β β ((πΌβ(1st
β(πΉβπ)))βπ) β ((β Γ β)
βm π))) |
232 | 230, 231 | sylibr 233 |
. . . . . 6
β’ ((π β§ π β β) β (πΌβ(1st β(πΉβπ))):ββΆ((β Γ β)
βm π)) |
233 | 232, 29 | ffvelcdmd 7083 |
. . . . 5
β’ ((π β§ π β β) β ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))) β ((β Γ β)
βm π)) |
234 | 233, 109 | fmptd 7109 |
. . . 4
β’ (π β πΊ:ββΆ((β Γ β)
βm π)) |
235 | | simpl 484 |
. . . . . . . . 9
β’ ((π β§ π β β) β π) |
236 | 86, 82 | eleqtrd 2836 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΌβπ) β {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))}) |
237 | 83, 236 | sselid 3979 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΌβπ) β (πΆβ(π΄βπ))) |
238 | | simp3 1139 |
. . . . . . . . . . . 12
β’ ((π β§ π β β β§ (πΌβπ) β (πΆβ(π΄βπ))) β (πΌβπ) β (πΆβ(π΄βπ))) |
239 | 49 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β β β§ (πΌβπ) β (πΆβ(π΄βπ))) β (πΆβ(π΄βπ)) = {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)}) |
240 | 238, 239 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ π β β β§ (πΌβπ) β (πΆβ(π΄βπ))) β (πΌβπ) β {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)}) |
241 | | fveq1 6887 |
. . . . . . . . . . . . . . . . 17
β’ (β = (πΌβπ) β (ββπ) = ((πΌβπ)βπ)) |
242 | 241 | coeq2d 5860 |
. . . . . . . . . . . . . . . 16
β’ (β = (πΌβπ) β ([,) β (ββπ)) = ([,) β ((πΌβπ)βπ))) |
243 | 242 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (β = (πΌβπ) β (([,) β (ββπ))βπ) = (([,) β ((πΌβπ)βπ))βπ)) |
244 | 243 | ixpeq2dv 8903 |
. . . . . . . . . . . . . 14
β’ (β = (πΌβπ) β Xπ β π (([,) β (ββπ))βπ) = Xπ β π (([,) β ((πΌβπ)βπ))βπ)) |
245 | 244 | iuneq2d 5025 |
. . . . . . . . . . . . 13
β’ (β = (πΌβπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) = βͺ π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ)) |
246 | 245 | sseq2d 4013 |
. . . . . . . . . . . 12
β’ (β = (πΌβπ) β ((π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ))) |
247 | 246 | elrab 3682 |
. . . . . . . . . . 11
β’ ((πΌβπ) β {β β (((β Γ β)
βm π)
βm β) β£ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} β ((πΌβπ) β (((β Γ β)
βm π)
βm β) β§ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ))) |
248 | 240, 247 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ (πΌβπ) β (πΆβ(π΄βπ))) β ((πΌβπ) β (((β Γ β)
βm π)
βm β) β§ (π΄βπ) β βͺ
π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ))) |
249 | 248 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π β β β§ (πΌβπ) β (πΆβ(π΄βπ))) β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ)) |
250 | 235, 4, 237, 249 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β β) β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ)) |
251 | | f1ofo 6837 |
. . . . . . . . . . . . . 14
β’ (πΉ:ββ1-1-ontoβ(β Γ β) β πΉ:ββontoβ(β Γ β)) |
252 | 20, 251 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββontoβ(β Γ β)) |
253 | 252 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β πΉ:ββontoβ(β Γ β)) |
254 | | opelxpi 5712 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β
β¨π, πβ© β (β Γ
β)) |
255 | 4, 254 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β β¨π, πβ© β (β Γ
β)) |
256 | | foelcdmi 6950 |
. . . . . . . . . . . 12
β’ ((πΉ:ββontoβ(β Γ β) β§ β¨π, πβ© β (β Γ β))
β βπ β
β (πΉβπ) = β¨π, πβ©) |
257 | 253, 255,
256 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β β) β βπ β β (πΉβπ) = β¨π, πβ©) |
258 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π((π β§ π β β) β§ π β β) |
259 | | nfre1 3283 |
. . . . . . . . . . . 12
β’
β²πβπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ) |
260 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β π β β) |
261 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) = β¨π, πβ© β (1st β(πΉβπ)) = (1st ββ¨π, πβ©)) |
262 | | op1stg 7982 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β V β§ π β V) β
(1st ββ¨π, πβ©) = π) |
263 | 262 | el2v 3483 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1st ββ¨π, πβ©) = π |
264 | 263 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) = β¨π, πβ© β (1st
ββ¨π, πβ©) = π) |
265 | 261, 264 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = β¨π, πβ© β (1st β(πΉβπ)) = π) |
266 | 265 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β (1st β(πΉβπ)) = π) |
267 | 260, 266 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β (π β β β§ (1st
β(πΉβπ)) = π)) |
268 | | 2fveq3 6893 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (1st β(πΉβπ)) = (1st β(πΉβπ))) |
269 | 268 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((1st β(πΉβπ)) = π β (1st β(πΉβπ)) = π)) |
270 | 269 | elrab 3682 |
. . . . . . . . . . . . . . . 16
β’ (π β {π β β β£ (1st
β(πΉβπ)) = π} β (π β β β§ (1st
β(πΉβπ)) = π)) |
271 | 267, 270 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β π β {π β β β£ (1st
β(πΉβπ)) = π}) |
272 | 271 | 3adant1 1131 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β β) β§ π β β β§ (πΉβπ) = β¨π, πβ©) β π β {π β β β£ (1st
β(πΉβπ)) = π}) |
273 | 260, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β (πΊβπ) = ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) |
274 | 265 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉβπ) = β¨π, πβ© β (πΌβ(1st β(πΉβπ))) = (πΌβπ)) |
275 | | vex 3479 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π β V |
276 | | vex 3479 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π β V |
277 | 275, 276 | op2ndd 7981 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉβπ) = β¨π, πβ© β (2nd β(πΉβπ)) = π) |
278 | 274, 277 | fveq12d 6895 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉβπ) = β¨π, πβ© β ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))) = ((πΌβπ)βπ)) |
279 | 278 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))) = ((πΌβπ)βπ)) |
280 | 273, 279 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β ((πΌβπ)βπ) = (πΊβπ)) |
281 | 280 | coeq2d 5860 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β ([,) β ((πΌβπ)βπ)) = ([,) β (πΊβπ))) |
282 | 281 | fveq1d 6890 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β (([,) β ((πΌβπ)βπ))βπ) = (([,) β (πΊβπ))βπ)) |
283 | 282 | ixpeq2dv 8903 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β Xπ β π (([,) β ((πΌβπ)βπ))βπ) = Xπ β π (([,) β (πΊβπ))βπ)) |
284 | | eqimss 4039 |
. . . . . . . . . . . . . . . 16
β’ (Xπ β
π (([,) β ((πΌβπ)βπ))βπ) = Xπ β π (([,) β (πΊβπ))βπ) β Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
285 | 283, 284 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (πΉβπ) = β¨π, πβ©) β Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
286 | 285 | 3adant1 1131 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β β) β§ π β β β§ (πΉβπ) = β¨π, πβ©) β Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
287 | | rspe 3247 |
. . . . . . . . . . . . . 14
β’ ((π β {π β β β£ (1st
β(πΉβπ)) = π} β§ Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) β βπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
288 | 272, 286,
287 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π β β) β§ π β β β§ (πΉβπ) = β¨π, πβ©) β βπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
289 | 288 | 3exp 1120 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β (π β β β ((πΉβπ) = β¨π, πβ© β βπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)))) |
290 | 258, 259,
289 | rexlimd 3264 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β β) β (βπ β β (πΉβπ) = β¨π, πβ© β βπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ))) |
291 | 257, 290 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β βπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
292 | 291 | ralrimiva 3147 |
. . . . . . . . 9
β’ ((π β§ π β β) β βπ β β βπ β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ)) |
293 | | iunss2 5051 |
. . . . . . . . 9
β’
(βπ β
β βπ β
{π β β β£
(1st β(πΉβπ)) = π}Xπ β π (([,) β ((πΌβπ)βπ))βπ) β Xπ β π (([,) β (πΊβπ))βπ) β βͺ
π β β Xπ β
π (([,) β ((πΌβπ)βπ))βπ) β βͺ
π β {π β β β£
(1st β(πΉβπ)) = π}Xπ β π (([,) β (πΊβπ))βπ)) |
294 | 292, 293 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β βͺ π β β Xπ β π (([,) β ((πΌβπ)βπ))βπ) β βͺ
π β {π β β β£
(1st β(πΉβπ)) = π}Xπ β π (([,) β (πΊβπ))βπ)) |
295 | 250, 294 | sstrd 3991 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄βπ) β βͺ
π β {π β β β£
(1st β(πΉβπ)) = π}Xπ β π (([,) β (πΊβπ))βπ)) |
296 | | ssrab2 4076 |
. . . . . . . . 9
β’ {π β β β£
(1st β(πΉβπ)) = π} β β |
297 | | iunss1 5010 |
. . . . . . . . 9
β’ ({π β β β£
(1st β(πΉβπ)) = π} β β β βͺ π β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β (πΊβπ))βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ)) |
298 | 296, 297 | ax-mp 5 |
. . . . . . . 8
β’ βͺ π β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β (πΊβπ))βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ) |
299 | 298 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β βͺ π β {π β β β£ (1st
β(πΉβπ)) = π}Xπ β π (([,) β (πΊβπ))βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ)) |
300 | 295, 299 | sstrd 3991 |
. . . . . 6
β’ ((π β§ π β β) β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ)) |
301 | 300 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ β β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ)) |
302 | | iunss 5047 |
. . . . 5
β’ (βͺ π β β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ) β βπ β β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ)) |
303 | 301, 302 | sylibr 233 |
. . . 4
β’ (π β βͺ π β β (π΄βπ) β βͺ
π β β Xπ β
π (([,) β (πΊβπ))βπ)) |
304 | 1, 126, 19, 234, 303 | ovnlecvr 45209 |
. . 3
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
(Ξ£^β(π β β β¦ (πΏβ(πΊβπ))))) |
305 | 112 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π β β) β (πΏβ(πΊβπ)) = (πΏβ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))))) |
306 | 305 | mpteq2dva 5247 |
. . . . . 6
β’ (π β (π β β β¦ (πΏβ(πΊβπ))) = (π β β β¦ (πΏβ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))))) |
307 | 306 | fveq2d 6892 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ (πΏβ(πΊβπ)))) =
(Ξ£^β(π β β β¦ (πΏβ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))))))) |
308 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
309 | | 2fveq3 6893 |
. . . . . . . 8
β’ (π = (πΉβπ) β (πΌβ(1st βπ)) = (πΌβ(1st β(πΉβπ)))) |
310 | | fveq2 6888 |
. . . . . . . 8
β’ (π = (πΉβπ) β (2nd βπ) = (2nd
β(πΉβπ))) |
311 | 309, 310 | fveq12d 6895 |
. . . . . . 7
β’ (π = (πΉβπ) β ((πΌβ(1st βπ))β(2nd
βπ)) = ((πΌβ(1st
β(πΉβπ)))β(2nd
β(πΉβπ)))) |
312 | 311 | fveq2d 6892 |
. . . . . 6
β’ (π = (πΉβπ) β (πΏβ((πΌβ(1st βπ))β(2nd
βπ))) = (πΏβ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))))) |
313 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
314 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π β§ π β (β Γ
β)) |
315 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β Γ β)) β
π β
Fin) |
316 | | simpl 484 |
. . . . . . . . 9
β’ ((π β§ π β (β Γ β)) β
π) |
317 | | xp1st 8002 |
. . . . . . . . . 10
β’ (π β (β Γ
β) β (1st βπ) β β) |
318 | 317 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (β Γ β)) β
(1st βπ)
β β) |
319 | | xp2nd 8003 |
. . . . . . . . . 10
β’ (π β (β Γ
β) β (2nd βπ) β β) |
320 | 319 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (β Γ β)) β
(2nd βπ)
β β) |
321 | | fvex 6901 |
. . . . . . . . . 10
β’
(2nd βπ) β V |
322 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = (2nd βπ) β (π β β β (2nd
βπ) β
β)) |
323 | 322 | 3anbi3d 1443 |
. . . . . . . . . . 11
β’ (π = (2nd βπ) β ((π β§ (1st βπ) β β β§ π β β) β (π β§ (1st
βπ) β β
β§ (2nd βπ) β β))) |
324 | | fveq2 6888 |
. . . . . . . . . . . 12
β’ (π = (2nd βπ) β ((πΌβ(1st βπ))βπ) = ((πΌβ(1st βπ))β(2nd
βπ))) |
325 | 324 | feq1d 6699 |
. . . . . . . . . . 11
β’ (π = (2nd βπ) β (((πΌβ(1st βπ))βπ):πβΆ(β Γ β) β
((πΌβ(1st
βπ))β(2nd βπ)):πβΆ(β Γ
β))) |
326 | 323, 325 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = (2nd βπ) β (((π β§ (1st βπ) β β β§ π β β) β ((πΌβ(1st
βπ))βπ):πβΆ(β Γ β)) β
((π β§ (1st
βπ) β β
β§ (2nd βπ) β β) β ((πΌβ(1st βπ))β(2nd
βπ)):πβΆ(β Γ
β)))) |
327 | | fvex 6901 |
. . . . . . . . . . 11
β’
(1st βπ) β V |
328 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π = (1st βπ) β (π β β β (1st
βπ) β
β)) |
329 | 328 | 3anbi2d 1442 |
. . . . . . . . . . . 12
β’ (π = (1st βπ) β ((π β§ π β β β§ π β β) β (π β§ (1st βπ) β β β§ π β
β))) |
330 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = (1st βπ) β (πΌβπ) = (πΌβ(1st βπ))) |
331 | 330 | fveq1d 6890 |
. . . . . . . . . . . . 13
β’ (π = (1st βπ) β ((πΌβπ)βπ) = ((πΌβ(1st βπ))βπ)) |
332 | 331 | feq1d 6699 |
. . . . . . . . . . . 12
β’ (π = (1st βπ) β (((πΌβπ)βπ):πβΆ(β Γ β) β
((πΌβ(1st
βπ))βπ):πβΆ(β Γ
β))) |
333 | 329, 332 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = (1st βπ) β (((π β§ π β β β§ π β β) β ((πΌβπ)βπ):πβΆ(β Γ β)) β
((π β§ (1st
βπ) β β
β§ π β β)
β ((πΌβ(1st βπ))βπ):πβΆ(β Γ
β)))) |
334 | 327, 333,
102 | vtocl 3549 |
. . . . . . . . . 10
β’ ((π β§ (1st
βπ) β β
β§ π β β)
β ((πΌβ(1st βπ))βπ):πβΆ(β Γ
β)) |
335 | 321, 326,
334 | vtocl 3549 |
. . . . . . . . 9
β’ ((π β§ (1st
βπ) β β
β§ (2nd βπ) β β) β ((πΌβ(1st βπ))β(2nd
βπ)):πβΆ(β Γ
β)) |
336 | 316, 318,
320, 335 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β (β Γ β)) β
((πΌβ(1st
βπ))β(2nd βπ)):πβΆ(β Γ
β)) |
337 | 314, 315,
19, 336 | hoiprodcl2 45206 |
. . . . . . 7
β’ ((π β§ π β (β Γ β)) β
(πΏβ((πΌβ(1st
βπ))β(2nd βπ))) β
(0[,)+β)) |
338 | 15, 337 | sselid 3979 |
. . . . . 6
β’ ((π β§ π β (β Γ β)) β
(πΏβ((πΌβ(1st
βπ))β(2nd βπ))) β
(0[,]+β)) |
339 | 308, 12, 312, 14, 20, 313, 338 | sge0f1o 45033 |
. . . . 5
β’ (π β
(Ξ£^β(π β (β Γ β) β¦
(πΏβ((πΌβ(1st
βπ))β(2nd βπ))))) =
(Ξ£^β(π β β β¦ (πΏβ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ))))))) |
340 | 307, 339 | eqtr4d 2776 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ (πΏβ(πΊβπ)))) =
(Ξ£^β(π β (β Γ β) β¦
(πΏβ((πΌβ(1st
βπ))β(2nd βπ)))))) |
341 | | nfv 1918 |
. . . . . . 7
β’
β²ππ |
342 | 275, 276 | op1std 7980 |
. . . . . . . . . 10
β’ (π = β¨π, πβ© β (1st βπ) = π) |
343 | 342 | fveq2d 6892 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (πΌβ(1st βπ)) = (πΌβπ)) |
344 | 275, 276 | op2ndd 7981 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (2nd βπ) = π) |
345 | 343, 344 | fveq12d 6895 |
. . . . . . . 8
β’ (π = β¨π, πβ© β ((πΌβ(1st βπ))β(2nd
βπ)) = ((πΌβπ)βπ)) |
346 | 345 | fveq2d 6892 |
. . . . . . 7
β’ (π = β¨π, πβ© β (πΏβ((πΌβ(1st βπ))β(2nd
βπ))) = (πΏβ((πΌβπ)βπ))) |
347 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π((π β§ π β β) β§ π β β) |
348 | 123 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β π β Fin) |
349 | 93, 101 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β ((πΌβπ)βπ):πβΆ(β Γ
β)) |
350 | 347, 348,
19, 349 | hoiprodcl2 45206 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β (πΏβ((πΌβπ)βπ)) β (0[,)+β)) |
351 | 15, 350 | sselid 3979 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β (πΏβ((πΌβπ)βπ)) β (0[,]+β)) |
352 | 351 | 3impa 1111 |
. . . . . . 7
β’ ((π β§ π β β β§ π β β) β (πΏβ((πΌβπ)βπ)) β (0[,]+β)) |
353 | 341, 346,
14, 14, 352 | sge0xp 45080 |
. . . . . 6
β’ (π β
(Ξ£^β(π β β β¦
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))))) =
(Ξ£^β(π β (β Γ β) β¦
(πΏβ((πΌβ(1st
βπ))β(2nd βπ)))))) |
354 | 353 | eqcomd 2739 |
. . . . 5
β’ (π β
(Ξ£^β(π β (β Γ β) β¦
(πΏβ((πΌβ(1st
βπ))β(2nd βπ))))) =
(Ξ£^β(π β β β¦
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ))))))) |
355 | 13 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β β β
V) |
356 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ (πΏβ((πΌβπ)βπ))) = (π β β β¦ (πΏβ((πΌβπ)βπ))) |
357 | 351, 356 | fmptd 7109 |
. . . . . . 7
β’ ((π β§ π β β) β (π β β β¦ (πΏβ((πΌβπ)βπ))):ββΆ(0[,]+β)) |
358 | 355, 357 | sge0cl 45032 |
. . . . . 6
β’ ((π β§ π β β) β
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))) β (0[,]+β)) |
359 | | fveq1 6887 |
. . . . . . . . . . . . 13
β’ (π = (πΌβπ) β (πβπ) = ((πΌβπ)βπ)) |
360 | 359 | fveq2d 6892 |
. . . . . . . . . . . 12
β’ (π = (πΌβπ) β (πΏβ(πβπ)) = (πΏβ((πΌβπ)βπ))) |
361 | 360 | mpteq2dv 5249 |
. . . . . . . . . . 11
β’ (π = (πΌβπ) β (π β β β¦ (πΏβ(πβπ))) = (π β β β¦ (πΏβ((πΌβπ)βπ)))) |
362 | 361 | fveq2d 6892 |
. . . . . . . . . 10
β’ (π = (πΌβπ) β
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) =
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ))))) |
363 | 362 | breq1d 5157 |
. . . . . . . . 9
β’ (π = (πΌβπ) β
((Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))) β
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) |
364 | 363 | elrab 3682 |
. . . . . . . 8
β’ ((πΌβπ) β {π β (πΆβ(π΄βπ)) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))} β ((πΌβπ) β (πΆβ(π΄βπ)) β§
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) |
365 | 236, 364 | sylib 217 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΌβπ) β (πΆβ(π΄βπ)) β§
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) |
366 | 365 | simprd 497 |
. . . . . 6
β’ ((π β§ π β β) β
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))) β€ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))) |
367 | 118, 14, 358, 173, 366 | sge0lempt 45061 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦
(Ξ£^β(π β β β¦ (πΏβ((πΌβπ)βπ)))))) β€
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))))) |
368 | 354, 367 | eqbrtrd 5169 |
. . . 4
β’ (π β
(Ξ£^β(π β (β Γ β) β¦
(πΏβ((πΌβ(1st
βπ))β(2nd βπ))))) β€
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))))) |
369 | 340, 368 | eqbrtrd 5169 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ (πΏβ(πΊβπ)))) β€
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))))) |
370 | 11, 117, 174, 304, 369 | xrletrd 13137 |
. 2
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ)))))) |
371 | 118, 14, 160, 168 | sge0xadd 45086 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) =
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π
(Ξ£^β(π β β β¦ (πΈ / (2βπ)))))) |
372 | 119 | a1i 11 |
. . . . . 6
β’ (π β 0 β
β*) |
373 | 121 | a1i 11 |
. . . . . 6
β’ (π β +β β
β*) |
374 | 145 | rexrd 11260 |
. . . . . 6
β’ (π β πΈ β
β*) |
375 | 70 | rpge0d 13016 |
. . . . . 6
β’ (π β 0 β€ πΈ) |
376 | 145 | ltpnfd 13097 |
. . . . . 6
β’ (π β πΈ < +β) |
377 | 372, 373,
374, 375, 376 | elicod 13370 |
. . . . 5
β’ (π β πΈ β (0[,)+β)) |
378 | 377 | sge0ad2en 45082 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ (πΈ / (2βπ)))) = πΈ) |
379 | 378 | oveq2d 7420 |
. . 3
β’ (π β
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π
(Ξ£^β(π β β β¦ (πΈ / (2βπ))))) =
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |
380 | 371, 379 | eqtrd 2773 |
. 2
β’ (π β
(Ξ£^β(π β β β¦ (((voln*βπ)β(π΄βπ)) +π (πΈ / (2βπ))))) =
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |
381 | 370, 380 | breqtrd 5173 |
1
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |