Step | Hyp | Ref
| Expression |
1 | | vonioolem1.r |
. . . . 5
β’ π = (π β β β¦ βπ β π ((π΅βπ) β ((πΆβπ)βπ))) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β π = (π β β β¦ βπ β π ((π΅βπ) β ((πΆβπ)βπ)))) |
3 | | vonioolem1.c |
. . . . . . . . . . 11
β’ πΆ = (π β β β¦ (π β π β¦ ((π΄βπ) + (1 / π)))) |
4 | 3 | a1i 11 |
. . . . . . . . . 10
β’ (π β πΆ = (π β β β¦ (π β π β¦ ((π΄βπ) + (1 / π))))) |
5 | | vonioolem1.x |
. . . . . . . . . . . 12
β’ (π β π β Fin) |
6 | 5 | mptexd 7175 |
. . . . . . . . . . 11
β’ (π β (π β π β¦ ((π΄βπ) + (1 / π))) β V) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π β π β¦ ((π΄βπ) + (1 / π))) β V) |
8 | 4, 7 | fvmpt2d 6962 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΆβπ) = (π β π β¦ ((π΄βπ) + (1 / π)))) |
9 | | ovexd 7393 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β ((π΄βπ) + (1 / π)) β V) |
10 | 8, 9 | fvmpt2d 6962 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β ((πΆβπ)βπ) = ((π΄βπ) + (1 / π))) |
11 | 10 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β ((π΅βπ) β ((πΆβπ)βπ)) = ((π΅βπ) β ((π΄βπ) + (1 / π)))) |
12 | | vonioolem1.b |
. . . . . . . . . . 11
β’ (π β π΅:πβΆβ) |
13 | 12 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΅βπ) β β) |
14 | 13 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) β β) |
15 | 14 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) β β) |
16 | | vonioolem1.a |
. . . . . . . . . . 11
β’ (π β π΄:πβΆβ) |
17 | 16 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π΄:πβΆβ) |
18 | 17 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) β β) |
19 | 18 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) β β) |
20 | | nnrecre 12200 |
. . . . . . . . . 10
β’ (π β β β (1 /
π) β
β) |
21 | 20 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β (1 / π) β β) |
22 | 21 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (1 / π) β β) |
23 | 15, 19, 22 | subsub4d 11548 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (((π΅βπ) β (π΄βπ)) β (1 / π)) = ((π΅βπ) β ((π΄βπ) + (1 / π)))) |
24 | 11, 23 | eqtr4d 2776 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β ((π΅βπ) β ((πΆβπ)βπ)) = (((π΅βπ) β (π΄βπ)) β (1 / π))) |
25 | 24 | prodeq2dv 15811 |
. . . . 5
β’ ((π β§ π β β) β βπ β π ((π΅βπ) β ((πΆβπ)βπ)) = βπ β π (((π΅βπ) β (π΄βπ)) β (1 / π))) |
26 | 25 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β β β¦ βπ β π ((π΅βπ) β ((πΆβπ)βπ))) = (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) β (1 / π)))) |
27 | 2, 26 | eqtrd 2773 |
. . 3
β’ (π β π = (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) β (1 / π)))) |
28 | | nfv 1918 |
. . . 4
β’
β²ππ |
29 | | rpssre 12927 |
. . . . . 6
β’
β+ β β |
30 | | vonioolem1.t |
. . . . . . 7
β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) |
31 | 16 | ffvelcdmda 7036 |
. . . . . . . 8
β’ ((π β§ π β π) β (π΄βπ) β β) |
32 | | difrp 12958 |
. . . . . . . 8
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β ((π΄βπ) < (π΅βπ) β ((π΅βπ) β (π΄βπ)) β
β+)) |
33 | 31, 13, 32 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π) β ((π΄βπ) < (π΅βπ) β ((π΅βπ) β (π΄βπ)) β
β+)) |
34 | 30, 33 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β
β+) |
35 | 29, 34 | sselid 3943 |
. . . . 5
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β β) |
36 | 35 | recnd 11188 |
. . . 4
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β β) |
37 | | eqid 2733 |
. . . 4
β’ (π β β β¦
βπ β π (((π΅βπ) β (π΄βπ)) β (1 / π))) = (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) β (1 / π))) |
38 | 28, 5, 36, 37 | fprodsubrecnncnv 44235 |
. . 3
β’ (π β (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) β (1 / π))) β βπ β π ((π΅βπ) β (π΄βπ))) |
39 | 27, 38 | eqbrtrd 5128 |
. 2
β’ (π β π β βπ β π ((π΅βπ) β (π΄βπ))) |
40 | | vonioolem1.z |
. . 3
β’ π =
(β€β₯βπ) |
41 | | nnex 12164 |
. . . . . 6
β’ β
β V |
42 | 41 | mptex 7174 |
. . . . 5
β’ (π β β β¦
βπ β π ((π΅βπ) β ((πΆβπ)βπ))) β V |
43 | 42 | a1i 11 |
. . . 4
β’ (π β (π β β β¦ βπ β π ((π΅βπ) β ((πΆβπ)βπ))) β V) |
44 | 1, 43 | eqeltrid 2838 |
. . 3
β’ (π β π β V) |
45 | | vonioolem1.s |
. . . 4
β’ π = (π β β β¦ ((volnβπ)β(π·βπ))) |
46 | 41 | mptex 7174 |
. . . . 5
β’ (π β β β¦
((volnβπ)β(π·βπ))) β V |
47 | 46 | a1i 11 |
. . . 4
β’ (π β (π β β β¦ ((volnβπ)β(π·βπ))) β V) |
48 | 45, 47 | eqeltrid 2838 |
. . 3
β’ (π β π β V) |
49 | | vonioolem1.n |
. . . 4
β’ π = ((ββ(1 / πΈ)) + 1) |
50 | | 1rp 12924 |
. . . . . . . . . 10
β’ 1 β
β+ |
51 | 50 | a1i 11 |
. . . . . . . . 9
β’ (π β 1 β
β+) |
52 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β π β¦ ((π΅βπ) β (π΄βπ))) = (π β π β¦ ((π΅βπ) β (π΄βπ))) |
53 | 28, 52, 34 | rnmptssd 43504 |
. . . . . . . . . 10
β’ (π β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β
β+) |
54 | | vonioolem1.e |
. . . . . . . . . . 11
β’ πΈ = inf(ran (π β π β¦ ((π΅βπ) β (π΄βπ))), β, < ) |
55 | | ltso 11240 |
. . . . . . . . . . . . 13
β’ < Or
β |
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β < Or
β) |
57 | 52 | rnmptfi 43476 |
. . . . . . . . . . . . 13
β’ (π β Fin β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β Fin) |
58 | 5, 57 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β Fin) |
59 | | vonioolem1.u |
. . . . . . . . . . . . 13
β’ (π β π β β
) |
60 | 28, 34, 52, 59 | rnmptn0 6197 |
. . . . . . . . . . . 12
β’ (π β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β β
) |
61 | 29 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β+
β β) |
62 | 53, 61 | sstrd 3955 |
. . . . . . . . . . . 12
β’ (π β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β β) |
63 | | fiinfcl 9442 |
. . . . . . . . . . . 12
β’ (( <
Or β β§ (ran (π
β π β¦ ((π΅βπ) β (π΄βπ))) β Fin β§ ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β β
β§ ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β β)) β inf(ran (π β π β¦ ((π΅βπ) β (π΄βπ))), β, < ) β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) |
64 | 56, 58, 60, 62, 63 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (π β inf(ran (π β π β¦ ((π΅βπ) β (π΄βπ))), β, < ) β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) |
65 | 54, 64 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β πΈ β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) |
66 | 53, 65 | sseldd 3946 |
. . . . . . . . 9
β’ (π β πΈ β
β+) |
67 | 51, 66 | rpdivcld 12979 |
. . . . . . . 8
β’ (π β (1 / πΈ) β
β+) |
68 | 67 | rpred 12962 |
. . . . . . 7
β’ (π β (1 / πΈ) β β) |
69 | 67 | rpge0d 12966 |
. . . . . . 7
β’ (π β 0 β€ (1 / πΈ)) |
70 | | flge0nn0 13731 |
. . . . . . 7
β’ (((1 /
πΈ) β β β§ 0
β€ (1 / πΈ)) β
(ββ(1 / πΈ))
β β0) |
71 | 68, 69, 70 | syl2anc 585 |
. . . . . 6
β’ (π β (ββ(1 / πΈ)) β
β0) |
72 | | nn0p1nn 12457 |
. . . . . 6
β’
((ββ(1 / πΈ)) β β0 β
((ββ(1 / πΈ)) +
1) β β) |
73 | 71, 72 | syl 17 |
. . . . 5
β’ (π β ((ββ(1 / πΈ)) + 1) β
β) |
74 | 73 | nnzd 12531 |
. . . 4
β’ (π β ((ββ(1 / πΈ)) + 1) β
β€) |
75 | 49, 74 | eqeltrid 2838 |
. . 3
β’ (π β π β β€) |
76 | 49 | recnnltrp 43698 |
. . . . . . . . . . . . 13
β’ (πΈ β β+
β (π β β
β§ (1 / π) < πΈ)) |
77 | 66, 76 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β β β§ (1 / π) < πΈ)) |
78 | 77 | simpld 496 |
. . . . . . . . . . 11
β’ (π β π β β) |
79 | | uznnssnn 12825 |
. . . . . . . . . . 11
β’ (π β β β
(β€β₯βπ) β β) |
80 | 78, 79 | syl 17 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β β) |
81 | 40, 80 | eqsstrid 3993 |
. . . . . . . . 9
β’ (π β π β β) |
82 | 81 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β π β β) |
83 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
84 | 82, 83 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ π β π) β π β β) |
85 | | vonioolem1.d |
. . . . . . . . 9
β’ π· = (π β β β¦ Xπ β
π (((πΆβπ)βπ)[,)(π΅βπ))) |
86 | 85 | a1i 11 |
. . . . . . . 8
β’ (π β π· = (π β β β¦ Xπ β
π (((πΆβπ)βπ)[,)(π΅βπ)))) |
87 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β Fin) |
88 | | eqid 2733 |
. . . . . . . . . 10
β’ dom
(volnβπ) = dom
(volnβπ) |
89 | 18, 21 | readdcld 11189 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π) β ((π΄βπ) + (1 / π)) β β) |
90 | 89 | fmpttd 7064 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π β π β¦ ((π΄βπ) + (1 / π))):πβΆβ) |
91 | 8 | feq1d 6654 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πΆβπ):πβΆβ β (π β π β¦ ((π΄βπ) + (1 / π))):πβΆβ)) |
92 | 90, 91 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
93 | 12 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π΅:πβΆβ) |
94 | 87, 88, 92, 93 | hoimbl 44958 |
. . . . . . . . 9
β’ ((π β§ π β β) β Xπ β
π (((πΆβπ)βπ)[,)(π΅βπ)) β dom (volnβπ)) |
95 | 94 | elexd 3464 |
. . . . . . . 8
β’ ((π β§ π β β) β Xπ β
π (((πΆβπ)βπ)[,)(π΅βπ)) β V) |
96 | 86, 95 | fvmpt2d 6962 |
. . . . . . 7
β’ ((π β§ π β β) β (π·βπ) = Xπ β π (((πΆβπ)βπ)[,)(π΅βπ))) |
97 | 84, 96 | syldan 592 |
. . . . . 6
β’ ((π β§ π β π) β (π·βπ) = Xπ β π (((πΆβπ)βπ)[,)(π΅βπ))) |
98 | 97 | fveq2d 6847 |
. . . . 5
β’ ((π β§ π β π) β ((volnβπ)β(π·βπ)) = ((volnβπ)βXπ β π (((πΆβπ)βπ)[,)(π΅βπ)))) |
99 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π β Fin) |
100 | 59 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π β β
) |
101 | 84, 92 | syldan 592 |
. . . . . 6
β’ ((π β§ π β π) β (πΆβπ):πβΆβ) |
102 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π΅:πβΆβ) |
103 | | eqid 2733 |
. . . . . 6
β’ Xπ β
π (((πΆβπ)βπ)[,)(π΅βπ)) = Xπ β π (((πΆβπ)βπ)[,)(π΅βπ)) |
104 | 99, 100, 101, 102, 103 | vonn0hoi 44997 |
. . . . 5
β’ ((π β§ π β π) β ((volnβπ)βXπ β π (((πΆβπ)βπ)[,)(π΅βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)(π΅βπ)))) |
105 | 101 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β ((πΆβπ)βπ) β β) |
106 | 84, 14 | syldanl 603 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β (π΅βπ) β β) |
107 | | volico 44310 |
. . . . . . . 8
β’ ((((πΆβπ)βπ) β β β§ (π΅βπ) β β) β (volβ(((πΆβπ)βπ)[,)(π΅βπ))) = if(((πΆβπ)βπ) < (π΅βπ), ((π΅βπ) β ((πΆβπ)βπ)), 0)) |
108 | 105, 106,
107 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π) β (volβ(((πΆβπ)βπ)[,)(π΅βπ))) = if(((πΆβπ)βπ) < (π΅βπ), ((π΅βπ) β ((πΆβπ)βπ)), 0)) |
109 | 84, 10 | syldanl 603 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β ((πΆβπ)βπ) = ((π΄βπ) + (1 / π))) |
110 | 84, 21 | syldanl 603 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β (1 / π) β β) |
111 | 78 | nnrecred 12209 |
. . . . . . . . . . . 12
β’ (π β (1 / π) β β) |
112 | 111 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β (1 / π) β β) |
113 | 35 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β ((π΅βπ) β (π΄βπ)) β β) |
114 | 40 | eleq2i 2826 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β (β€β₯βπ)) |
115 | 114 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (π β π β π β (β€β₯βπ)) |
116 | | eluzle 12781 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β π β€ π) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β π β€ π) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β€ π) |
119 | 78 | nnrpd 12960 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β+) |
120 | 119 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β
β+) |
121 | | nnrp 12931 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β+) |
122 | 84, 121 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β β+) |
123 | 120, 122 | lerecd 12981 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π β€ π β (1 / π) β€ (1 / π))) |
124 | 118, 123 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (1 / π) β€ (1 / π)) |
125 | 124 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β (1 / π) β€ (1 / π)) |
126 | 111 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (1 / π) β β) |
127 | 29, 66 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β β) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β πΈ β β) |
129 | 77 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β (1 / π) < πΈ) |
130 | 129 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (1 / π) < πΈ) |
131 | 62 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β β) |
132 | 58 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β Fin) |
133 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π β π) |
134 | | ovexd 7393 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((π΅βπ) β (π΄βπ)) β V) |
135 | 52 | elrnmpt1 5914 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ ((π΅βπ) β (π΄βπ)) β V) β ((π΅βπ) β (π΄βπ)) β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) |
136 | 133, 134,
135 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β π β ((π΅βπ) β (π΄βπ)) β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) |
137 | 136 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) |
138 | | infrefilb 12146 |
. . . . . . . . . . . . . . 15
β’ ((ran
(π β π β¦ ((π΅βπ) β (π΄βπ))) β β β§ ran (π β π β¦ ((π΅βπ) β (π΄βπ))) β Fin β§ ((π΅βπ) β (π΄βπ)) β ran (π β π β¦ ((π΅βπ) β (π΄βπ)))) β inf(ran (π β π β¦ ((π΅βπ) β (π΄βπ))), β, < ) β€ ((π΅βπ) β (π΄βπ))) |
139 | 131, 132,
137, 138 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β inf(ran (π β π β¦ ((π΅βπ) β (π΄βπ))), β, < ) β€ ((π΅βπ) β (π΄βπ))) |
140 | 54, 139 | eqbrtrid 5141 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β πΈ β€ ((π΅βπ) β (π΄βπ))) |
141 | 126, 128,
35, 130, 140 | ltletrd 11320 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (1 / π) < ((π΅βπ) β (π΄βπ))) |
142 | 141 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β (1 / π) < ((π΅βπ) β (π΄βπ))) |
143 | 110, 112,
113, 125, 142 | lelttrd 11318 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β π) β (1 / π) < ((π΅βπ) β (π΄βπ))) |
144 | 84, 18 | syldanl 603 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β (π΄βπ) β β) |
145 | 144, 110,
106 | ltaddsub2d 11761 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β π) β (((π΄βπ) + (1 / π)) < (π΅βπ) β (1 / π) < ((π΅βπ) β (π΄βπ)))) |
146 | 143, 145 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β ((π΄βπ) + (1 / π)) < (π΅βπ)) |
147 | 109, 146 | eqbrtrd 5128 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β ((πΆβπ)βπ) < (π΅βπ)) |
148 | 147 | iftrued 4495 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π) β if(((πΆβπ)βπ) < (π΅βπ), ((π΅βπ) β ((πΆβπ)βπ)), 0) = ((π΅βπ) β ((πΆβπ)βπ))) |
149 | 108, 148 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π β π) β§ π β π) β (volβ(((πΆβπ)βπ)[,)(π΅βπ))) = ((π΅βπ) β ((πΆβπ)βπ))) |
150 | 149 | prodeq2dv 15811 |
. . . . 5
β’ ((π β§ π β π) β βπ β π (volβ(((πΆβπ)βπ)[,)(π΅βπ))) = βπ β π ((π΅βπ) β ((πΆβπ)βπ))) |
151 | 98, 104, 150 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π β π) β ((volnβπ)β(π·βπ)) = βπ β π ((π΅βπ) β ((πΆβπ)βπ))) |
152 | | fvexd 6858 |
. . . . 5
β’ ((π β§ π β π) β ((volnβπ)β(π·βπ)) β V) |
153 | 45 | fvmpt2 6960 |
. . . . 5
β’ ((π β β β§
((volnβπ)β(π·βπ)) β V) β (πβπ) = ((volnβπ)β(π·βπ))) |
154 | 84, 152, 153 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π) β (πβπ) = ((volnβπ)β(π·βπ))) |
155 | | prodex 15795 |
. . . . . 6
β’
βπ β
π ((π΅βπ) β ((πΆβπ)βπ)) β V |
156 | 155 | a1i 11 |
. . . . 5
β’ ((π β§ π β π) β βπ β π ((π΅βπ) β ((πΆβπ)βπ)) β V) |
157 | 1 | fvmpt2 6960 |
. . . . 5
β’ ((π β β β§
βπ β π ((π΅βπ) β ((πΆβπ)βπ)) β V) β (πβπ) = βπ β π ((π΅βπ) β ((πΆβπ)βπ))) |
158 | 84, 156, 157 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π) β (πβπ) = βπ β π ((π΅βπ) β ((πΆβπ)βπ))) |
159 | 151, 154,
158 | 3eqtr4rd 2784 |
. . 3
β’ ((π β§ π β π) β (πβπ) = (πβπ)) |
160 | 40, 44, 48, 75, 159 | climeq 15455 |
. 2
β’ (π β (π β βπ β π ((π΅βπ) β (π΄βπ)) β π β βπ β π ((π΅βπ) β (π΄βπ)))) |
161 | 39, 160 | mpbid 231 |
1
β’ (π β π β βπ β π ((π΅βπ) β (π΄βπ))) |