Step | Hyp | Ref
| Expression |
1 | | eldiophelnn0 41130 |
. . 3
β’ (π΄ β (Diophβπ) β π β
β0) |
2 | | id 22 |
. . . . . 6
β’ (π β β0
β π β
β0) |
3 | | zex 12513 |
. . . . . . 7
β’ β€
β V |
4 | | difexg 5285 |
. . . . . . 7
β’ (β€
β V β (β€ β (β€β₯β(π + 1))) β
V) |
5 | 3, 4 | mp1i 13 |
. . . . . 6
β’ (π β β0
β (β€ β (β€β₯β(π + 1))) β V) |
6 | | ominf 9205 |
. . . . . . 7
β’ Β¬
Ο β Fin |
7 | | nn0z 12529 |
. . . . . . . 8
β’ (π β β0
β π β
β€) |
8 | | lzenom 41136 |
. . . . . . . 8
β’ (π β β€ β (β€
β (β€β₯β(π + 1))) β Ο) |
9 | | enfi 9137 |
. . . . . . . 8
β’ ((β€
β (β€β₯β(π + 1))) β Ο β ((β€
β (β€β₯β(π + 1))) β Fin β Ο β
Fin)) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . 7
β’ (π β β0
β ((β€ β (β€β₯β(π + 1))) β Fin β Ο β
Fin)) |
11 | 6, 10 | mtbiri 327 |
. . . . . 6
β’ (π β β0
β Β¬ (β€ β (β€β₯β(π + 1))) β Fin) |
12 | | fz1eqin 41135 |
. . . . . . 7
β’ (π β β0
β (1...π) = ((β€
β (β€β₯β(π + 1))) β© β)) |
13 | | inss1 4189 |
. . . . . . 7
β’ ((β€
β (β€β₯β(π + 1))) β© β) β (β€
β (β€β₯β(π + 1))) |
14 | 12, 13 | eqsstrdi 3999 |
. . . . . 6
β’ (π β β0
β (1...π) β
(β€ β (β€β₯β(π + 1)))) |
15 | | eldioph2b 41129 |
. . . . . 6
β’ (((π β β0
β§ (β€ β (β€β₯β(π + 1))) β V) β§ (Β¬ (β€
β (β€β₯β(π + 1))) β Fin β§ (1...π) β (β€ β
(β€β₯β(π + 1))))) β (π΄ β (Diophβπ) β βπ β (mzPolyβ(β€ β
(β€β₯β(π + 1))))π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
16 | 2, 5, 11, 14, 15 | syl22anc 838 |
. . . . 5
β’ (π β β0
β (π΄ β
(Diophβπ) β
βπ β
(mzPolyβ(β€ β (β€β₯β(π + 1))))π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
17 | | nnex 12164 |
. . . . . . 7
β’ β
β V |
18 | 17 | a1i 11 |
. . . . . 6
β’ (π β β0
β β β V) |
19 | | 1z 12538 |
. . . . . . 7
β’ 1 β
β€ |
20 | | nnuz 12811 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
21 | 20 | uzinf 13876 |
. . . . . . 7
β’ (1 β
β€ β Β¬ β β Fin) |
22 | 19, 21 | mp1i 13 |
. . . . . 6
β’ (π β β0
β Β¬ β β Fin) |
23 | | elfznn 13476 |
. . . . . . . 8
β’ (π β (1...π) β π β β) |
24 | 23 | ssriv 3949 |
. . . . . . 7
β’
(1...π) β
β |
25 | 24 | a1i 11 |
. . . . . 6
β’ (π β β0
β (1...π) β
β) |
26 | | eldioph2b 41129 |
. . . . . 6
β’ (((π β β0
β§ β β V) β§ (Β¬ β β Fin β§ (1...π) β β)) β
(π΅ β
(Diophβπ) β
βπ β
(mzPolyββ)π΅ =
{π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
27 | 2, 18, 22, 25, 26 | syl22anc 838 |
. . . . 5
β’ (π β β0
β (π΅ β
(Diophβπ) β
βπ β
(mzPolyββ)π΅ =
{π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
28 | 16, 27 | anbi12d 632 |
. . . 4
β’ (π β β0
β ((π΄ β
(Diophβπ) β§ π΅ β (Diophβπ)) β (βπ β (mzPolyβ(β€
β (β€β₯β(π + 1))))π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ βπ β (mzPolyββ)π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}))) |
29 | | reeanv 3216 |
. . . . 5
β’
(βπ β
(mzPolyβ(β€ β (β€β₯β(π + 1))))βπ β (mzPolyββ)(π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (βπ β (mzPolyβ(β€ β
(β€β₯β(π + 1))))π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ βπ β (mzPolyββ)π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
30 | | inab 4260 |
. . . . . . . . 9
β’ ({π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β© {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) = {π β£ (βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0))} |
31 | | reeanv 3216 |
. . . . . . . . . . 11
β’
(βπ β
(β0 βm (β€ β
(β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β (βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0))) |
32 | | simplrl 776 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β π β (β0
βm (β€ β (β€β₯β(π + 1))))) |
33 | | simplrr 777 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β π β (β0
βm β)) |
34 | 12 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β ((β€ β (β€β₯β(π + 1))) β© β) = (1...π)) |
35 | 34 | reseq2d 5938 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π βΎ ((β€
β (β€β₯β(π + 1))) β© β)) = (π βΎ (1...π))) |
36 | 35 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β)) = (π βΎ (1...π))) |
37 | 34 | reseq2d 5938 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β (π βΎ ((β€
β (β€β₯β(π + 1))) β© β)) = (π βΎ (1...π))) |
38 | 37 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β)) = (π βΎ (1...π))) |
39 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β π = (π βΎ (1...π))) |
40 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β π = (π βΎ (1...π))) |
41 | 38, 39, 40 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β)) = (π βΎ (1...π))) |
42 | 36, 41 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β)) = (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β))) |
43 | | elmapresaun 8821 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β) β§ (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β)) = (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β))) β (π βͺ π) β (β0
βm ((β€ β (β€β₯β(π + 1))) βͺ
β))) |
44 | 32, 33, 42, 43 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βͺ π) β (β0
βm ((β€ β (β€β₯β(π + 1))) βͺ
β))) |
45 | 20 | uneq2i 4121 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β€
β (β€β₯β(π + 1))) βͺ β) = ((β€ β
(β€β₯β(π + 1))) βͺ
(β€β₯β1)) |
46 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β 1 β β€) |
47 | | nn0p1nn 12457 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (π + 1) β
β) |
48 | 47 | nnge1d 12206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β 1 β€ (π +
1)) |
49 | | lzunuz 41134 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β€ β§ 1 β
β€ β§ 1 β€ (π +
1)) β ((β€ β (β€β₯β(π + 1))) βͺ
(β€β₯β1)) = β€) |
50 | 7, 46, 48, 49 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β ((β€ β (β€β₯β(π + 1))) βͺ
(β€β₯β1)) = β€) |
51 | 45, 50 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β ((β€ β (β€β₯β(π + 1))) βͺ β) =
β€) |
52 | 51 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (β0 βm ((β€ β
(β€β₯β(π + 1))) βͺ β)) =
(β0 βm β€)) |
53 | 52 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (β0
βm ((β€ β (β€β₯β(π + 1))) βͺ β)) =
(β0 βm β€)) |
54 | 44, 53 | eleqtrd 2836 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βͺ π) β (β0
βm β€)) |
55 | | unidm 4113 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βͺ π) = π |
56 | 40, 39 | uneq12d 4125 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βͺ π) = ((π βΎ (1...π)) βͺ (π βΎ (1...π)))) |
57 | 55, 56 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β π = ((π βΎ (1...π)) βͺ (π βΎ (1...π)))) |
58 | | resundir 5953 |
. . . . . . . . . . . . . . . . . 18
β’ ((π βͺ π) βΎ (1...π)) = ((π βΎ (1...π)) βͺ (π βΎ (1...π))) |
59 | 57, 58 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β π = ((π βͺ π) βΎ (1...π))) |
60 | | uncom 4114 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π βͺ π) = (π βͺ π) |
61 | 60 | reseq1i 5934 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1)))) = ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1)))) |
62 | | incom 4162 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (β
β© (β€ β (β€β₯β(π + 1)))) = ((β€ β
(β€β₯β(π + 1))) β© β) |
63 | 62, 34 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β (β β© (β€ β (β€β₯β(π + 1)))) = (1...π)) |
64 | 63 | reseq2d 5938 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β (π βΎ (β
β© (β€ β (β€β₯β(π + 1))))) = (π βΎ (1...π))) |
65 | 64 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ (β β© (β€ β
(β€β₯β(π + 1))))) = (π βΎ (1...π))) |
66 | 63 | reseq2d 5938 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β (π βΎ (β
β© (β€ β (β€β₯β(π + 1))))) = (π βΎ (1...π))) |
67 | 66 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ (β β© (β€ β
(β€β₯β(π + 1))))) = (π βΎ (1...π))) |
68 | 67, 40, 39 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ (β β© (β€ β
(β€β₯β(π + 1))))) = (π βΎ (1...π))) |
69 | 65, 68 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π βΎ (β β© (β€ β
(β€β₯β(π + 1))))) = (π βΎ (β β© (β€ β
(β€β₯β(π + 1)))))) |
70 | | elmapresaunres2 41137 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (β0
βm β) β§ π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ (π βΎ (β β© (β€
β (β€β₯β(π + 1))))) = (π βΎ (β β© (β€ β
(β€β₯β(π + 1)))))) β ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1)))) = π) |
71 | 33, 32, 69, 70 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1)))) = π) |
72 | 61, 71 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1)))) = π) |
73 | 72 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = (πβπ)) |
74 | | simprlr 779 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (πβπ) = 0) |
75 | 73, 74 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = 0) |
76 | | elmapresaunres2 41137 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β) β§ (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β)) = (π βΎ ((β€ β
(β€β₯β(π + 1))) β© β))) β ((π βͺ π) βΎ β) = π) |
77 | 32, 33, 42, 76 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β ((π βͺ π) βΎ β) = π) |
78 | 77 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (πβ((π βͺ π) βΎ β)) = (πβπ)) |
79 | | simprrr 781 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (πβπ) = 0) |
80 | 78, 79 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (πβ((π βͺ π) βΎ β)) = 0) |
81 | 59, 75, 80 | jca32 517 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β (π = ((π βͺ π) βΎ (1...π)) β§ ((πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ((π βͺ π) βΎ β)) = 0))) |
82 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ π) β (π βΎ (1...π)) = ((π βͺ π) βΎ (1...π))) |
83 | 82 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βͺ π) β (π = (π βΎ (1...π)) β π = ((π βͺ π) βΎ (1...π)))) |
84 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π βͺ π) β (π βΎ (β€ β
(β€β₯β(π + 1)))) = ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) |
85 | 84 | fveqeq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ π) β ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β (πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = 0)) |
86 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π βͺ π) β (π βΎ β) = ((π βͺ π) βΎ β)) |
87 | 86 | fveqeq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ π) β ((πβ(π βΎ β)) = 0 β (πβ((π βͺ π) βΎ β)) = 0)) |
88 | 85, 87 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βͺ π) β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0) β ((πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ((π βͺ π) βΎ β)) = 0))) |
89 | 83, 88 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βͺ π) β ((π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)) β (π = ((π βͺ π) βΎ (1...π)) β§ ((πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ((π βͺ π) βΎ β)) = 0)))) |
90 | 89 | rspcev 3580 |
. . . . . . . . . . . . . . . 16
β’ (((π βͺ π) β (β0
βm β€) β§ (π = ((π βͺ π) βΎ (1...π)) β§ ((πβ((π βͺ π) βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ((π βͺ π) βΎ β)) = 0))) β
βπ β
(β0 βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) |
91 | 54, 81, 90 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β§ ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) |
92 | 91 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ (π β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ π β (β0
βm β))) β (((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)))) |
93 | 92 | rexlimdvva 3202 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(βπ β
(β0 βm (β€ β
(β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)))) |
94 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β π β (β0
βm β€)) |
95 | | difss 4092 |
. . . . . . . . . . . . . . . . 17
β’ (β€
β (β€β₯β(π + 1))) β β€ |
96 | | elmapssres 8808 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (β0
βm β€) β§ (β€ β
(β€β₯β(π + 1))) β β€) β (π βΎ (β€ β
(β€β₯β(π + 1)))) β (β0
βm (β€ β (β€β₯β(π + 1))))) |
97 | 94, 95, 96 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (π βΎ (β€ β
(β€β₯β(π + 1)))) β (β0
βm (β€ β (β€β₯β(π + 1))))) |
98 | 97 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β (π βΎ (β€ β
(β€β₯β(π + 1)))) β (β0
βm (β€ β (β€β₯β(π + 1))))) |
99 | | nnssz 12526 |
. . . . . . . . . . . . . . . . 17
β’ β
β β€ |
100 | | elmapssres 8808 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (β0
βm β€) β§ β β β€) β (π βΎ β) β
(β0 βm β)) |
101 | 94, 99, 100 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (π βΎ β) β (β0
βm β)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β (π βΎ β) β
(β0 βm β)) |
103 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β π = (π βΎ (1...π))) |
104 | 14 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β (1...π) β (β€ β
(β€β₯β(π + 1)))) |
105 | 104 | resabs1d 5969 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) = (π βΎ (1...π))) |
106 | 103, 105 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π))) |
107 | | simprrl 780 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0) |
108 | 106, 107 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β (π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0)) |
109 | | resabs1 5968 |
. . . . . . . . . . . . . . . . . 18
β’
((1...π) β
β β ((π βΎ
β) βΎ (1...π)) =
(π βΎ (1...π))) |
110 | 24, 109 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β ((π βΎ β) βΎ
(1...π)) = (π βΎ (1...π))) |
111 | 103, 110 | eqtr4d 2776 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β π = ((π βΎ β) βΎ (1...π))) |
112 | | simprrr 781 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β (πβ(π βΎ β)) = 0) |
113 | 108, 111,
112 | jca32 517 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β ((π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0) β§ (π = ((π βΎ β) βΎ (1...π)) β§ (πβ(π βΎ β)) = 0))) |
114 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βΎ (β€ β
(β€β₯β(π + 1)))) β (π βΎ (1...π)) = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π))) |
115 | 114 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βΎ (β€ β
(β€β₯β(π + 1)))) β (π = (π βΎ (1...π)) β π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)))) |
116 | | fveqeq2 6852 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βΎ (β€ β
(β€β₯β(π + 1)))) β ((πβπ) = 0 β (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0)) |
117 | 115, 116 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ (β€ β
(β€β₯β(π + 1)))) β ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β (π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0))) |
118 | 117 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (β€ β
(β€β₯β(π + 1)))) β (((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β ((π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)))) |
119 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βΎ β) β (π βΎ (1...π)) = ((π βΎ β) βΎ (1...π))) |
120 | 119 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βΎ β) β (π = (π βΎ (1...π)) β π = ((π βΎ β) βΎ (1...π)))) |
121 | | fveqeq2 6852 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βΎ β) β ((πβπ) = 0 β (πβ(π βΎ β)) = 0)) |
122 | 120, 121 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ β) β ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β (π = ((π βΎ β) βΎ (1...π)) β§ (πβ(π βΎ β)) = 0))) |
123 | 122 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ β) β (((π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β ((π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0) β§ (π = ((π βΎ β) βΎ (1...π)) β§ (πβ(π βΎ β)) = 0)))) |
124 | 118, 123 | rspc2ev 3591 |
. . . . . . . . . . . . . . 15
β’ (((π βΎ (β€ β
(β€β₯β(π + 1)))) β (β0
βm (β€ β (β€β₯β(π + 1)))) β§ (π βΎ β) β
(β0 βm β) β§ ((π = ((π βΎ (β€ β
(β€β₯β(π + 1)))) βΎ (1...π)) β§ (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0) β§ (π = ((π βΎ β) βΎ (1...π)) β§ (πβ(π βΎ β)) = 0))) β βπ β (β0
βm (β€ β (β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) |
125 | 98, 102, 113, 124 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β§ (π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0))) β βπ β (β0
βm (β€ β (β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0))) |
126 | 125 | rexlimdva2 3151 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(βπ β
(β0 βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)) β βπ β (β0
βm (β€ β (β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)))) |
127 | 93, 126 | impbid 211 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(βπ β
(β0 βm (β€ β
(β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)))) |
128 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β π β (mzPolyβ(β€ β
(β€β₯β(π + 1))))) |
129 | | mzpf 41102 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (mzPolyβ(β€
β (β€β₯β(π + 1)))) β π:(β€ βm (β€ β
(β€β₯β(π + 1))))βΆβ€) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β π:(β€ βm (β€ β
(β€β₯β(π + 1))))βΆβ€) |
131 | | nn0ssz 12527 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β0 β β€ |
132 | | mapss 8830 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β€
β V β§ β0 β β€) β (β0
βm β€) β (β€ βm
β€)) |
133 | 3, 131, 132 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β0 βm β€) β (β€
βm β€) |
134 | 133 | sseli 3941 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β0
βm β€) β π β (β€ βm
β€)) |
135 | | elmapssres 8808 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (β€
βm β€) β§ (β€ β
(β€β₯β(π + 1))) β β€) β (π βΎ (β€ β
(β€β₯β(π + 1)))) β (β€ βm
(β€ β (β€β₯β(π + 1))))) |
136 | 134, 95, 135 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β0
βm β€) β (π βΎ (β€ β
(β€β₯β(π + 1)))) β (β€ βm
(β€ β (β€β₯β(π + 1))))) |
137 | 136 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (π βΎ (β€ β
(β€β₯β(π + 1)))) β (β€ βm
(β€ β (β€β₯β(π + 1))))) |
138 | 130, 137 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) β β€) |
139 | 138 | zred 12612 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) β β) |
140 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β π β
(mzPolyββ)) |
141 | | mzpf 41102 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (mzPolyββ)
β π:(β€
βm β)βΆβ€) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β π:(β€ βm
β)βΆβ€) |
143 | | elmapssres 8808 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (β€
βm β€) β§ β β β€) β (π βΎ β) β
(β€ βm β)) |
144 | 134, 99, 143 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β0
βm β€) β (π βΎ β) β (β€
βm β)) |
145 | 144 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (π βΎ β) β (β€
βm β)) |
146 | 142, 145 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (πβ(π βΎ β)) β
β€) |
147 | 146 | zred 12612 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (πβ(π βΎ β)) β
β) |
148 | | sumsqeq0 14089 |
. . . . . . . . . . . . . . . 16
β’ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) β β β§ (πβ(π βΎ β)) β β) β
(((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0) β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)) =
0)) |
149 | 139, 147,
148 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0) β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)) =
0)) |
150 | 134 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β π β (β€ βm
β€)) |
151 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π βΎ (β€ β
(β€β₯β(π + 1)))) = (π βΎ (β€ β
(β€β₯β(π + 1))))) |
152 | 151 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = (πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))) |
153 | 152 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) = ((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2)) |
154 | | reseq1 5932 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π βΎ β) = (π βΎ β)) |
155 | 154 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (πβ(π βΎ β)) = (πβ(π βΎ β))) |
156 | 155 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πβ(π βΎ β))β2) = ((πβ(π βΎ β))β2)) |
157 | 153, 156 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)) = (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) |
158 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β€
βm β€) β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) = (π β (β€
βm β€) β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) |
159 | | ovex 7391 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)) β
V |
160 | 157, 158,
159 | fvmpt 6949 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β€
βm β€) β ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) |
161 | 150, 160 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) |
162 | 161 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0 β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)) =
0)) |
163 | 149, 162 | bitr4d 282 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β (((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0) β ((π β (β€
βm β€) β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0)) |
164 | 163 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β§ π β (β0
βm β€)) β ((π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)) β (π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0))) |
165 | 164 | rexbidva 3170 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(βπ β
(β0 βm β€)(π = (π βΎ (1...π)) β§ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1))))) = 0 β§ (πβ(π βΎ β)) = 0)) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0))) |
166 | 127, 165 | bitrd 279 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(βπ β
(β0 βm (β€ β
(β€β₯β(π + 1))))βπ β (β0
βm β)((π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ (π = (π βΎ (1...π)) β§ (πβπ) = 0)) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0))) |
167 | 31, 166 | bitr3id 285 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
((βπ β
(β0 βm (β€ β
(β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)) β βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0))) |
168 | 167 | abbidv 2802 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
{π β£ (βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0) β§ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0))} = {π β£ βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0)}) |
169 | 30, 168 | eqtrid 2785 |
. . . . . . . 8
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
({π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β© {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) = {π β£ βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0)}) |
170 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β π β
β0) |
171 | | fzssuz 13488 |
. . . . . . . . . . . 12
β’
(1...π) β
(β€β₯β1) |
172 | | uzssz 12789 |
. . . . . . . . . . . 12
β’
(β€β₯β1) β β€ |
173 | 171, 172 | sstri 3954 |
. . . . . . . . . . 11
β’
(1...π) β
β€ |
174 | 3, 173 | pm3.2i 472 |
. . . . . . . . . 10
β’ (β€
β V β§ (1...π)
β β€) |
175 | 174 | a1i 11 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(β€ β V β§ (1...π) β β€)) |
176 | 3 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
β€ β V) |
177 | 95 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(β€ β (β€β₯β(π + 1))) β β€) |
178 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β π β (mzPolyβ(β€
β (β€β₯β(π + 1))))) |
179 | | mzpresrename 41116 |
. . . . . . . . . . . 12
β’ ((β€
β V β§ (β€ β (β€β₯β(π + 1))) β β€ β§
π β
(mzPolyβ(β€ β (β€β₯β(π + 1))))) β (π β (β€ βm β€)
β¦ (πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))) β
(mzPolyββ€)) |
180 | 176, 177,
178, 179 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(π β (β€
βm β€) β¦ (πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))) β
(mzPolyββ€)) |
181 | | 2nn0 12435 |
. . . . . . . . . . 11
β’ 2 β
β0 |
182 | | mzpexpmpt 41111 |
. . . . . . . . . . 11
β’ (((π β (β€
βm β€) β¦ (πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))) β (mzPolyββ€)
β§ 2 β β0) β (π β (β€ βm β€)
β¦ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2)) β
(mzPolyββ€)) |
183 | 180, 181,
182 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(π β (β€
βm β€) β¦ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2)) β
(mzPolyββ€)) |
184 | 99 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
β β β€) |
185 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β π β
(mzPolyββ)) |
186 | | mzpresrename 41116 |
. . . . . . . . . . . 12
β’ ((β€
β V β§ β β β€ β§ π β (mzPolyββ)) β (π β (β€
βm β€) β¦ (πβ(π βΎ β))) β
(mzPolyββ€)) |
187 | 176, 184,
185, 186 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(π β (β€
βm β€) β¦ (πβ(π βΎ β))) β
(mzPolyββ€)) |
188 | | mzpexpmpt 41111 |
. . . . . . . . . . 11
β’ (((π β (β€
βm β€) β¦ (πβ(π βΎ β))) β
(mzPolyββ€) β§ 2 β β0) β (π β (β€
βm β€) β¦ ((πβ(π βΎ β))β2)) β
(mzPolyββ€)) |
189 | 187, 181,
188 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(π β (β€
βm β€) β¦ ((πβ(π βΎ β))β2)) β
(mzPolyββ€)) |
190 | | mzpaddmpt 41107 |
. . . . . . . . . 10
β’ (((π β (β€
βm β€) β¦ ((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2)) β
(mzPolyββ€) β§ (π β (β€ βm β€)
β¦ ((πβ(π βΎ β))β2))
β (mzPolyββ€)) β (π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) β
(mzPolyββ€)) |
191 | 183, 189,
190 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
(π β (β€
βm β€) β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) β
(mzPolyββ€)) |
192 | | eldioph2 41128 |
. . . . . . . . 9
β’ ((π β β0
β§ (β€ β V β§ (1...π) β β€) β§ (π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2))) β
(mzPolyββ€)) β {π β£ βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0)} β
(Diophβπ)) |
193 | 170, 175,
191, 192 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
{π β£ βπ β (β0
βm β€)(π = (π βΎ (1...π)) β§ ((π β (β€ βm β€)
β¦ (((πβ(π βΎ (β€ β
(β€β₯β(π + 1)))))β2) + ((πβ(π βΎ β))β2)))βπ) = 0)} β
(Diophβπ)) |
194 | 169, 193 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
({π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β© {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (Diophβπ)) |
195 | | ineq12 4168 |
. . . . . . . 8
β’ ((π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (π΄ β© π΅) = ({π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β© {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
196 | 195 | eleq1d 2819 |
. . . . . . 7
β’ ((π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β ((π΄ β© π΅) β (Diophβπ) β ({π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β© {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (Diophβπ))) |
197 | 194, 196 | syl5ibrcom 247 |
. . . . . 6
β’ ((π β β0
β§ (π β
(mzPolyβ(β€ β (β€β₯β(π + 1)))) β§ π β (mzPolyββ))) β
((π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (π΄ β© π΅) β (Diophβπ))) |
198 | 197 | rexlimdvva 3202 |
. . . . 5
β’ (π β β0
β (βπ β
(mzPolyβ(β€ β (β€β₯β(π + 1))))βπ β (mzPolyββ)(π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (π΄ β© π΅) β (Diophβπ))) |
199 | 29, 198 | biimtrrid 242 |
. . . 4
β’ (π β β0
β ((βπ β
(mzPolyβ(β€ β (β€β₯β(π + 1))))π΄ = {π β£ βπ β (β0
βm (β€ β (β€β₯β(π + 1))))(π = (π βΎ (1...π)) β§ (πβπ) = 0)} β§ βπ β (mzPolyββ)π΅ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) β (π΄ β© π΅) β (Diophβπ))) |
200 | 28, 199 | sylbid 239 |
. . 3
β’ (π β β0
β ((π΄ β
(Diophβπ) β§ π΅ β (Diophβπ)) β (π΄ β© π΅) β (Diophβπ))) |
201 | 1, 200 | syl 17 |
. 2
β’ (π΄ β (Diophβπ) β ((π΄ β (Diophβπ) β§ π΅ β (Diophβπ)) β (π΄ β© π΅) β (Diophβπ))) |
202 | 201 | anabsi5 668 |
1
β’ ((π΄ β (Diophβπ) β§ π΅ β (Diophβπ)) β (π΄ β© π΅) β (Diophβπ)) |