Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²ππ |
2 | | nfcv 2908 |
. . . . 5
β’
β²π(!β(π΅βπ·)) |
3 | | mccllem.a |
. . . . . 6
β’ (π β π΄ β Fin) |
4 | | mccllem.c |
. . . . . 6
β’ (π β πΆ β π΄) |
5 | | ssfi 9118 |
. . . . . 6
β’ ((π΄ β Fin β§ πΆ β π΄) β πΆ β Fin) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . 5
β’ (π β πΆ β Fin) |
7 | | mccllem.d |
. . . . 5
β’ (π β π· β (π΄ β πΆ)) |
8 | | eldifn 4088 |
. . . . . 6
β’ (π· β (π΄ β πΆ) β Β¬ π· β πΆ) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ (π β Β¬ π· β πΆ) |
10 | | mccllem.b |
. . . . . . . . . 10
β’ (π β π΅ β (β0
βm (πΆ βͺ
{π·}))) |
11 | | elmapi 8788 |
. . . . . . . . . 10
β’ (π΅ β (β0
βm (πΆ βͺ
{π·})) β π΅:(πΆ βͺ {π·})βΆβ0) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ (π β π΅:(πΆ βͺ {π·})βΆβ0) |
13 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β π΅:(πΆ βͺ {π·})βΆβ0) |
14 | | elun1 4137 |
. . . . . . . . 9
β’ (π β πΆ β π β (πΆ βͺ {π·})) |
15 | 14 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β π β (πΆ βͺ {π·})) |
16 | 13, 15 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ π β πΆ) β (π΅βπ) β
β0) |
17 | 16 | faccld 14185 |
. . . . . 6
β’ ((π β§ π β πΆ) β (!β(π΅βπ)) β β) |
18 | 17 | nncnd 12170 |
. . . . 5
β’ ((π β§ π β πΆ) β (!β(π΅βπ)) β β) |
19 | | 2fveq3 6848 |
. . . . 5
β’ (π = π· β (!β(π΅βπ)) = (!β(π΅βπ·))) |
20 | | snidg 4621 |
. . . . . . . . . 10
β’ (π· β (π΄ β πΆ) β π· β {π·}) |
21 | 7, 20 | syl 17 |
. . . . . . . . 9
β’ (π β π· β {π·}) |
22 | | elun2 4138 |
. . . . . . . . 9
β’ (π· β {π·} β π· β (πΆ βͺ {π·})) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
β’ (π β π· β (πΆ βͺ {π·})) |
24 | 12, 23 | ffvelcdmd 7037 |
. . . . . . 7
β’ (π β (π΅βπ·) β
β0) |
25 | 24 | faccld 14185 |
. . . . . 6
β’ (π β (!β(π΅βπ·)) β β) |
26 | 25 | nncnd 12170 |
. . . . 5
β’ (π β (!β(π΅βπ·)) β β) |
27 | 1, 2, 6, 7, 9, 18,
19, 26 | fprodsplitsn 15873 |
. . . 4
β’ (π β βπ β (πΆ βͺ {π·})(!β(π΅βπ)) = (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·)))) |
28 | 27 | oveq2d 7374 |
. . 3
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / βπ β (πΆ βͺ {π·})(!β(π΅βπ))) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))))) |
29 | 7 | eldifad 3923 |
. . . . . . . . . . . 12
β’ (π β π· β π΄) |
30 | | snssi 4769 |
. . . . . . . . . . . 12
β’ (π· β π΄ β {π·} β π΄) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
β’ (π β {π·} β π΄) |
32 | 4, 31 | unssd 4147 |
. . . . . . . . . 10
β’ (π β (πΆ βͺ {π·}) β π΄) |
33 | | ssfi 9118 |
. . . . . . . . . 10
β’ ((π΄ β Fin β§ (πΆ βͺ {π·}) β π΄) β (πΆ βͺ {π·}) β Fin) |
34 | 3, 32, 33 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΆ βͺ {π·}) β Fin) |
35 | 12 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ ((π β§ π β (πΆ βͺ {π·})) β (π΅βπ) β
β0) |
36 | 34, 35 | fsumnn0cl 15622 |
. . . . . . . 8
β’ (π β Ξ£π β (πΆ βͺ {π·})(π΅βπ) β
β0) |
37 | 36 | faccld 14185 |
. . . . . . 7
β’ (π β (!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) β β) |
38 | 37 | nncnd 12170 |
. . . . . 6
β’ (π β (!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) β β) |
39 | 1, 6, 18 | fprodclf 15876 |
. . . . . . 7
β’ (π β βπ β πΆ (!β(π΅βπ)) β β) |
40 | 39, 26 | mulcld 11176 |
. . . . . 6
β’ (π β (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))) β β) |
41 | 17 | nnne0d 12204 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (!β(π΅βπ)) β 0) |
42 | 6, 18, 41 | fprodn0 15863 |
. . . . . . 7
β’ (π β βπ β πΆ (!β(π΅βπ)) β 0) |
43 | 25 | nnne0d 12204 |
. . . . . . 7
β’ (π β (!β(π΅βπ·)) β 0) |
44 | 39, 26, 42, 43 | mulne0d 11808 |
. . . . . 6
β’ (π β (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))) β 0) |
45 | 38, 40, 44 | divcld 11932 |
. . . . 5
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·)))) β β) |
46 | 45 | mulid2d 11174 |
. . . 4
β’ (π β (1 Β·
((!βΞ£π β
(πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))))) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))))) |
47 | 46 | eqcomd 2743 |
. . 3
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·)))) = (1 Β· ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·)))))) |
48 | 6, 16 | fsumnn0cl 15622 |
. . . . . . . . 9
β’ (π β Ξ£π β πΆ (π΅βπ) β
β0) |
49 | 48 | faccld 14185 |
. . . . . . . 8
β’ (π β (!βΞ£π β πΆ (π΅βπ)) β β) |
50 | 49 | nncnd 12170 |
. . . . . . 7
β’ (π β (!βΞ£π β πΆ (π΅βπ)) β β) |
51 | | nnne0 12188 |
. . . . . . . 8
β’
((!βΞ£π
β πΆ (π΅βπ)) β β β
(!βΞ£π β
πΆ (π΅βπ)) β 0) |
52 | 49, 51 | syl 17 |
. . . . . . 7
β’ (π β (!βΞ£π β πΆ (π΅βπ)) β 0) |
53 | 50, 52 | dividd 11930 |
. . . . . 6
β’ (π β ((!βΞ£π β πΆ (π΅βπ)) / (!βΞ£π β πΆ (π΅βπ))) = 1) |
54 | 53 | eqcomd 2743 |
. . . . 5
β’ (π β 1 = ((!βΞ£π β πΆ (π΅βπ)) / (!βΞ£π β πΆ (π΅βπ)))) |
55 | 39, 26 | mulcomd 11177 |
. . . . . . 7
β’ (π β (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))) = ((!β(π΅βπ·)) Β· βπ β πΆ (!β(π΅βπ)))) |
56 | 55 | oveq2d 7374 |
. . . . . 6
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·)))) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(π΅βπ·)) Β· βπ β πΆ (!β(π΅βπ))))) |
57 | 38, 26, 39, 43, 42 | divdiv1d 11963 |
. . . . . . 7
β’ (π β (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / βπ β πΆ (!β(π΅βπ))) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(π΅βπ·)) Β· βπ β πΆ (!β(π΅βπ))))) |
58 | 57 | eqcomd 2743 |
. . . . . 6
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(π΅βπ·)) Β· βπ β πΆ (!β(π΅βπ)))) = (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / βπ β πΆ (!β(π΅βπ)))) |
59 | 56, 58 | eqtrd 2777 |
. . . . 5
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·)))) = (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / βπ β πΆ (!β(π΅βπ)))) |
60 | 54, 59 | oveq12d 7376 |
. . . 4
β’ (π β (1 Β·
((!βΞ£π β
(πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))))) = (((!βΞ£π β πΆ (π΅βπ)) / (!βΞ£π β πΆ (π΅βπ))) Β· (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / βπ β πΆ (!β(π΅βπ))))) |
61 | 38, 26, 43 | divcld 11932 |
. . . . 5
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) β β) |
62 | 50, 50, 61, 39, 52, 42 | divmul13d 11974 |
. . . 4
β’ (π β (((!βΞ£π β πΆ (π΅βπ)) / (!βΞ£π β πΆ (π΅βπ))) Β· (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / βπ β πΆ (!β(π΅βπ)))) = ((((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) Β· ((!βΞ£π β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ))))) |
63 | 60, 62 | eqtrd 2777 |
. . 3
β’ (π β (1 Β·
((!βΞ£π β
(πΆ βͺ {π·})(π΅βπ)) / (βπ β πΆ (!β(π΅βπ)) Β· (!β(π΅βπ·))))) = ((((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) Β· ((!βΞ£π β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ))))) |
64 | 28, 47, 63 | 3eqtrd 2781 |
. 2
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / βπ β (πΆ βͺ {π·})(!β(π΅βπ))) = ((((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) Β· ((!βΞ£π β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ))))) |
65 | 38, 26, 50, 43, 52 | divdiv1d 11963 |
. . . . 5
β’ (π β (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(π΅βπ·)) Β· (!βΞ£π β πΆ (π΅βπ))))) |
66 | | nfcsb1v 3881 |
. . . . . . . . . . 11
β’
β²πβ¦π· / πβ¦(π΅βπ) |
67 | 16 | nn0cnd 12476 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (π΅βπ) β β) |
68 | | csbeq1a 3870 |
. . . . . . . . . . 11
β’ (π = π· β (π΅βπ) = β¦π· / πβ¦(π΅βπ)) |
69 | | csbfv 6893 |
. . . . . . . . . . . . 13
β’
β¦π· /
πβ¦(π΅βπ) = (π΅βπ·) |
70 | 69 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β¦π· / πβ¦(π΅βπ) = (π΅βπ·)) |
71 | 24 | nn0cnd 12476 |
. . . . . . . . . . . 12
β’ (π β (π΅βπ·) β β) |
72 | 70, 71 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (π β β¦π· / πβ¦(π΅βπ) β β) |
73 | 1, 66, 6, 29, 9, 67, 68, 72 | fsumsplitsn 15630 |
. . . . . . . . . 10
β’ (π β Ξ£π β (πΆ βͺ {π·})(π΅βπ) = (Ξ£π β πΆ (π΅βπ) + β¦π· / πβ¦(π΅βπ))) |
74 | 73 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β (Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ)) = ((Ξ£π β πΆ (π΅βπ) + β¦π· / πβ¦(π΅βπ)) β Ξ£π β πΆ (π΅βπ))) |
75 | 48 | nn0cnd 12476 |
. . . . . . . . . 10
β’ (π β Ξ£π β πΆ (π΅βπ) β β) |
76 | 75, 72 | pncan2d 11515 |
. . . . . . . . 9
β’ (π β ((Ξ£π β πΆ (π΅βπ) + β¦π· / πβ¦(π΅βπ)) β Ξ£π β πΆ (π΅βπ)) = β¦π· / πβ¦(π΅βπ)) |
77 | 74, 76, 70 | 3eqtrrd 2782 |
. . . . . . . 8
β’ (π β (π΅βπ·) = (Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ))) |
78 | 77 | fveq2d 6847 |
. . . . . . 7
β’ (π β (!β(π΅βπ·)) = (!β(Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ)))) |
79 | 78 | oveq1d 7373 |
. . . . . 6
β’ (π β ((!β(π΅βπ·)) Β· (!βΞ£π β πΆ (π΅βπ))) = ((!β(Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ))) Β· (!βΞ£π β πΆ (π΅βπ)))) |
80 | 79 | oveq2d 7374 |
. . . . 5
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(π΅βπ·)) Β· (!βΞ£π β πΆ (π΅βπ)))) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ))) Β· (!βΞ£π β πΆ (π΅βπ))))) |
81 | | 0zd 12512 |
. . . . . . . 8
β’ (π β 0 β
β€) |
82 | 36 | nn0zd 12526 |
. . . . . . . 8
β’ (π β Ξ£π β (πΆ βͺ {π·})(π΅βπ) β β€) |
83 | 48 | nn0zd 12526 |
. . . . . . . 8
β’ (π β Ξ£π β πΆ (π΅βπ) β β€) |
84 | 48 | nn0ge0d 12477 |
. . . . . . . 8
β’ (π β 0 β€ Ξ£π β πΆ (π΅βπ)) |
85 | 24 | nn0ge0d 12477 |
. . . . . . . . . . 11
β’ (π β 0 β€ (π΅βπ·)) |
86 | 70 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β (π΅βπ·) = β¦π· / πβ¦(π΅βπ)) |
87 | 85, 86 | breqtrd 5132 |
. . . . . . . . . 10
β’ (π β 0 β€
β¦π· / πβ¦(π΅βπ)) |
88 | 48 | nn0red 12475 |
. . . . . . . . . . 11
β’ (π β Ξ£π β πΆ (π΅βπ) β β) |
89 | 24 | nn0red 12475 |
. . . . . . . . . . . 12
β’ (π β (π΅βπ·) β β) |
90 | 70, 89 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (π β β¦π· / πβ¦(π΅βπ) β β) |
91 | 88, 90 | addge01d 11744 |
. . . . . . . . . 10
β’ (π β (0 β€
β¦π· / πβ¦(π΅βπ) β Ξ£π β πΆ (π΅βπ) β€ (Ξ£π β πΆ (π΅βπ) + β¦π· / πβ¦(π΅βπ)))) |
92 | 87, 91 | mpbid 231 |
. . . . . . . . 9
β’ (π β Ξ£π β πΆ (π΅βπ) β€ (Ξ£π β πΆ (π΅βπ) + β¦π· / πβ¦(π΅βπ))) |
93 | 73 | eqcomd 2743 |
. . . . . . . . 9
β’ (π β (Ξ£π β πΆ (π΅βπ) + β¦π· / πβ¦(π΅βπ)) = Ξ£π β (πΆ βͺ {π·})(π΅βπ)) |
94 | 92, 93 | breqtrd 5132 |
. . . . . . . 8
β’ (π β Ξ£π β πΆ (π΅βπ) β€ Ξ£π β (πΆ βͺ {π·})(π΅βπ)) |
95 | 81, 82, 83, 84, 94 | elfzd 13433 |
. . . . . . 7
β’ (π β Ξ£π β πΆ (π΅βπ) β (0...Ξ£π β (πΆ βͺ {π·})(π΅βπ))) |
96 | | bcval2 14206 |
. . . . . . 7
β’
(Ξ£π β
πΆ (π΅βπ) β (0...Ξ£π β (πΆ βͺ {π·})(π΅βπ)) β (Ξ£π β (πΆ βͺ {π·})(π΅βπ)CΞ£π β πΆ (π΅βπ)) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ))) Β· (!βΞ£π β πΆ (π΅βπ))))) |
97 | 95, 96 | syl 17 |
. . . . . 6
β’ (π β (Ξ£π β (πΆ βͺ {π·})(π΅βπ)CΞ£π β πΆ (π΅βπ)) = ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ))) Β· (!βΞ£π β πΆ (π΅βπ))))) |
98 | 97 | eqcomd 2743 |
. . . . 5
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / ((!β(Ξ£π β (πΆ βͺ {π·})(π΅βπ) β Ξ£π β πΆ (π΅βπ))) Β· (!βΞ£π β πΆ (π΅βπ)))) = (Ξ£π β (πΆ βͺ {π·})(π΅βπ)CΞ£π β πΆ (π΅βπ))) |
99 | 65, 80, 98 | 3eqtrd 2781 |
. . . 4
β’ (π β (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) = (Ξ£π β (πΆ βͺ {π·})(π΅βπ)CΞ£π β πΆ (π΅βπ))) |
100 | | bccl2 14224 |
. . . . 5
β’
(Ξ£π β
πΆ (π΅βπ) β (0...Ξ£π β (πΆ βͺ {π·})(π΅βπ)) β (Ξ£π β (πΆ βͺ {π·})(π΅βπ)CΞ£π β πΆ (π΅βπ)) β β) |
101 | 95, 100 | syl 17 |
. . . 4
β’ (π β (Ξ£π β (πΆ βͺ {π·})(π΅βπ)CΞ£π β πΆ (π΅βπ)) β β) |
102 | 99, 101 | eqeltrd 2838 |
. . 3
β’ (π β (((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) β β) |
103 | | mccllem.6 |
. . . 4
β’ (π β βπ β (β0
βm πΆ)((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) β β) |
104 | | ssun1 4133 |
. . . . . 6
β’ πΆ β (πΆ βͺ {π·}) |
105 | 104 | a1i 11 |
. . . . 5
β’ (π β πΆ β (πΆ βͺ {π·})) |
106 | | elmapssres 8806 |
. . . . 5
β’ ((π΅ β (β0
βm (πΆ βͺ
{π·})) β§ πΆ β (πΆ βͺ {π·})) β (π΅ βΎ πΆ) β (β0
βm πΆ)) |
107 | 10, 105, 106 | syl2anc 585 |
. . . 4
β’ (π β (π΅ βΎ πΆ) β (β0
βm πΆ)) |
108 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (π = (π΅ βΎ πΆ) β (πβπ) = ((π΅ βΎ πΆ)βπ)) |
109 | 108 | adantr 482 |
. . . . . . . . . 10
β’ ((π = (π΅ βΎ πΆ) β§ π β πΆ) β (πβπ) = ((π΅ βΎ πΆ)βπ)) |
110 | | fvres 6862 |
. . . . . . . . . . 11
β’ (π β πΆ β ((π΅ βΎ πΆ)βπ) = (π΅βπ)) |
111 | 110 | adantl 483 |
. . . . . . . . . 10
β’ ((π = (π΅ βΎ πΆ) β§ π β πΆ) β ((π΅ βΎ πΆ)βπ) = (π΅βπ)) |
112 | 109, 111 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π = (π΅ βΎ πΆ) β§ π β πΆ) β (πβπ) = (π΅βπ)) |
113 | 112 | sumeq2dv 15589 |
. . . . . . . 8
β’ (π = (π΅ βΎ πΆ) β Ξ£π β πΆ (πβπ) = Ξ£π β πΆ (π΅βπ)) |
114 | 113 | fveq2d 6847 |
. . . . . . 7
β’ (π = (π΅ βΎ πΆ) β (!βΞ£π β πΆ (πβπ)) = (!βΞ£π β πΆ (π΅βπ))) |
115 | 112 | fveq2d 6847 |
. . . . . . . 8
β’ ((π = (π΅ βΎ πΆ) β§ π β πΆ) β (!β(πβπ)) = (!β(π΅βπ))) |
116 | 115 | prodeq2dv 15807 |
. . . . . . 7
β’ (π = (π΅ βΎ πΆ) β βπ β πΆ (!β(πβπ)) = βπ β πΆ (!β(π΅βπ))) |
117 | 114, 116 | oveq12d 7376 |
. . . . . 6
β’ (π = (π΅ βΎ πΆ) β ((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) = ((!βΞ£π β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ)))) |
118 | 117 | eleq1d 2823 |
. . . . 5
β’ (π = (π΅ βΎ πΆ) β (((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) β β β
((!βΞ£π β
πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ))) β β)) |
119 | 118 | rspccva 3581 |
. . . 4
β’
((βπ β
(β0 βm πΆ)((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) β β β§ (π΅ βΎ πΆ) β (β0
βm πΆ))
β ((!βΞ£π
β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ))) β β) |
120 | 103, 107,
119 | syl2anc 585 |
. . 3
β’ (π β ((!βΞ£π β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ))) β β) |
121 | 102, 120 | nnmulcld 12207 |
. 2
β’ (π β ((((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / (!β(π΅βπ·))) / (!βΞ£π β πΆ (π΅βπ))) Β· ((!βΞ£π β πΆ (π΅βπ)) / βπ β πΆ (!β(π΅βπ)))) β β) |
122 | 64, 121 | eqeltrd 2838 |
1
β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / βπ β (πΆ βͺ {π·})(!β(π΅βπ))) β β) |