Step | Hyp | Ref
| Expression |
1 | | vonicclem1.s |
. . . 4
β’ π = (π β β β¦ ((volnβπ)β(π·βπ))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β π = (π β β β¦ ((volnβπ)β(π·βπ)))) |
3 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
4 | | vonicclem1.d |
. . . . . . . . . 10
β’ π· = (π β β β¦ Xπ β
π ((π΄βπ)[,)((πΆβπ)βπ))) |
5 | 4 | a1i 11 |
. . . . . . . . 9
β’ (π β π· = (π β β β¦ Xπ β
π ((π΄βπ)[,)((πΆβπ)βπ)))) |
6 | | vonicclem1.x |
. . . . . . . . . . . 12
β’ (π β π β Fin) |
7 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β Fin) |
8 | | eqid 2733 |
. . . . . . . . . . 11
β’ dom
(volnβπ) = dom
(volnβπ) |
9 | | vonicclem1.a |
. . . . . . . . . . . 12
β’ (π β π΄:πβΆβ) |
10 | 9 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π΄:πβΆβ) |
11 | | vonicclem1.b |
. . . . . . . . . . . . . . . 16
β’ (π β π΅:πβΆβ) |
12 | 11 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (π΅βπ) β β) |
13 | 12 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) β β) |
14 | | nnrecre 12200 |
. . . . . . . . . . . . . . 15
β’ (π β β β (1 /
π) β
β) |
15 | 14 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β (1 / π) β β) |
16 | 13, 15 | readdcld 11189 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β ((π΅βπ) + (1 / π)) β β) |
17 | 16 | fmpttd 7064 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π β π β¦ ((π΅βπ) + (1 / π))):πβΆβ) |
18 | | vonicclem1.c |
. . . . . . . . . . . . . . 15
β’ πΆ = (π β β β¦ (π β π β¦ ((π΅βπ) + (1 / π)))) |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β πΆ = (π β β β¦ (π β π β¦ ((π΅βπ) + (1 / π))))) |
20 | 6 | mptexd 7175 |
. . . . . . . . . . . . . . 15
β’ (π β (π β π β¦ ((π΅βπ) + (1 / π))) β V) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π β π β¦ ((π΅βπ) + (1 / π))) β V) |
22 | 19, 21 | fvmpt2d 6962 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΆβπ) = (π β π β¦ ((π΅βπ) + (1 / π)))) |
23 | 22 | feq1d 6654 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΆβπ):πβΆβ β (π β π β¦ ((π΅βπ) + (1 / π))):πβΆβ)) |
24 | 17, 23 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
25 | 7, 8, 10, 24 | hoimbl 44958 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Xπ β
π ((π΄βπ)[,)((πΆβπ)βπ)) β dom (volnβπ)) |
26 | 25 | elexd 3464 |
. . . . . . . . 9
β’ ((π β§ π β β) β Xπ β
π ((π΄βπ)[,)((πΆβπ)βπ)) β V) |
27 | 5, 26 | fvmpt2d 6962 |
. . . . . . . 8
β’ ((π β§ π β β) β (π·βπ) = Xπ β π ((π΄βπ)[,)((πΆβπ)βπ))) |
28 | 3, 27 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β β) β (π·βπ) = Xπ β π ((π΄βπ)[,)((πΆβπ)βπ))) |
29 | 28 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π β β) β ((volnβπ)β(π·βπ)) = ((volnβπ)βXπ β π ((π΄βπ)[,)((πΆβπ)βπ)))) |
30 | | vonicclem1.u |
. . . . . . . 8
β’ (π β π β β
) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β β
) |
32 | 3, 24 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
33 | | eqid 2733 |
. . . . . . 7
β’ Xπ β
π ((π΄βπ)[,)((πΆβπ)βπ)) = Xπ β π ((π΄βπ)[,)((πΆβπ)βπ)) |
34 | 7, 31, 10, 32, 33 | vonn0hoi 44997 |
. . . . . 6
β’ ((π β§ π β β) β ((volnβπ)βXπ β
π ((π΄βπ)[,)((πΆβπ)βπ))) = βπ β π (volβ((π΄βπ)[,)((πΆβπ)βπ)))) |
35 | 10 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) β β) |
36 | 3, 35 | syldanl 603 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) β β) |
37 | 32 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β ((πΆβπ)βπ) β β) |
38 | | volico 44310 |
. . . . . . . . 9
β’ (((π΄βπ) β β β§ ((πΆβπ)βπ) β β) β (volβ((π΄βπ)[,)((πΆβπ)βπ))) = if((π΄βπ) < ((πΆβπ)βπ), (((πΆβπ)βπ) β (π΄βπ)), 0)) |
39 | 36, 37, 38 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (volβ((π΄βπ)[,)((πΆβπ)βπ))) = if((π΄βπ) < ((πΆβπ)βπ), (((πΆβπ)βπ) β (π΄βπ)), 0)) |
40 | 3, 13 | syldanl 603 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) β β) |
41 | | vonicclem1.t |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄βπ) β€ (π΅βπ)) |
42 | 41 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) β€ (π΅βπ)) |
43 | | nnrp 12931 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β+) |
44 | 43 | rpreccld 12972 |
. . . . . . . . . . . . 13
β’ (π β β β (1 /
π) β
β+) |
45 | 44 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π) β (1 / π) β
β+) |
46 | 40, 45 | ltaddrpd 12995 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) < ((π΅βπ) + (1 / π))) |
47 | 16 | elexd 3464 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β ((π΅βπ) + (1 / π)) β V) |
48 | 22, 47 | fvmpt2d 6962 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π) β ((πΆβπ)βπ) = ((π΅βπ) + (1 / π))) |
49 | 3, 48 | syldanl 603 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β ((πΆβπ)βπ) = ((π΅βπ) + (1 / π))) |
50 | 46, 49 | breqtrrd 5134 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) < ((πΆβπ)βπ)) |
51 | 36, 40, 37, 42, 50 | lelttrd 11318 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) < ((πΆβπ)βπ)) |
52 | 51 | iftrued 4495 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β if((π΄βπ) < ((πΆβπ)βπ), (((πΆβπ)βπ) β (π΄βπ)), 0) = (((πΆβπ)βπ) β (π΄βπ))) |
53 | 39, 52 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (volβ((π΄βπ)[,)((πΆβπ)βπ))) = (((πΆβπ)βπ) β (π΄βπ))) |
54 | 53 | prodeq2dv 15811 |
. . . . . 6
β’ ((π β§ π β β) β βπ β π (volβ((π΄βπ)[,)((πΆβπ)βπ))) = βπ β π (((πΆβπ)βπ) β (π΄βπ))) |
55 | 29, 34, 54 | 3eqtrd 2777 |
. . . . 5
β’ ((π β§ π β β) β ((volnβπ)β(π·βπ)) = βπ β π (((πΆβπ)βπ) β (π΄βπ))) |
56 | 48 | oveq1d 7373 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ) β (π΄βπ)) = (((π΅βπ) + (1 / π)) β (π΄βπ))) |
57 | 13 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (π΅βπ) β β) |
58 | 15 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (1 / π) β β) |
59 | 35 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β (π΄βπ) β β) |
60 | 57, 58, 59 | addsubd 11538 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (((π΅βπ) + (1 / π)) β (π΄βπ)) = (((π΅βπ) β (π΄βπ)) + (1 / π))) |
61 | 56, 60 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ) β (π΄βπ)) = (((π΅βπ) β (π΄βπ)) + (1 / π))) |
62 | 61 | prodeq2dv 15811 |
. . . . 5
β’ ((π β§ π β β) β βπ β π (((πΆβπ)βπ) β (π΄βπ)) = βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π))) |
63 | 55, 62 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β) β ((volnβπ)β(π·βπ)) = βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π))) |
64 | 63 | mpteq2dva 5206 |
. . 3
β’ (π β (π β β β¦ ((volnβπ)β(π·βπ))) = (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π)))) |
65 | 2, 64 | eqtrd 2773 |
. 2
β’ (π β π = (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π)))) |
66 | | nfv 1918 |
. . 3
β’
β²ππ |
67 | 9 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β π) β (π΄βπ) β β) |
68 | 12, 67 | resubcld 11588 |
. . . 4
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β β) |
69 | 68 | recnd 11188 |
. . 3
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β β) |
70 | | eqid 2733 |
. . 3
β’ (π β β β¦
βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π))) = (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π))) |
71 | 66, 6, 69, 70 | fprodaddrecnncnv 44237 |
. 2
β’ (π β (π β β β¦ βπ β π (((π΅βπ) β (π΄βπ)) + (1 / π))) β βπ β π ((π΅βπ) β (π΄βπ))) |
72 | 65, 71 | eqbrtrd 5128 |
1
β’ (π β π β βπ β π ((π΅βπ) β (π΄βπ))) |