Step | Hyp | Ref
| Expression |
1 | | drngring 20364 |
. . . . . . 7
β’ (π
β DivRing β π
β Ring) |
2 | | ig1pval.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
3 | 2 | ply1ring 21770 |
. . . . . . 7
β’ (π
β Ring β π β Ring) |
4 | 1, 3 | syl 17 |
. . . . . 6
β’ (π
β DivRing β π β Ring) |
5 | 4 | 3ad2ant1 1134 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β π β§ π β πΌ) β π β Ring) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
7 | | ig1pcl.u |
. . . . . . . 8
β’ π = (LIdealβπ) |
8 | 6, 7 | lidlss 20833 |
. . . . . . 7
β’ (πΌ β π β πΌ β (Baseβπ)) |
9 | 8 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β π β§ π β πΌ) β πΌ β (Baseβπ)) |
10 | | ig1pval.g |
. . . . . . . 8
β’ πΊ =
(idlGen1pβπ
) |
11 | 2, 10, 7 | ig1pcl 25693 |
. . . . . . 7
β’ ((π
β DivRing β§ πΌ β π) β (πΊβπΌ) β πΌ) |
12 | 11 | 3adant3 1133 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β π β§ π β πΌ) β (πΊβπΌ) β πΌ) |
13 | 9, 12 | sseldd 3984 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β π β§ π β πΌ) β (πΊβπΌ) β (Baseβπ)) |
14 | | ig1pdvds.d |
. . . . . 6
β’ β₯ =
(β₯rβπ) |
15 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
16 | 6, 14, 15 | dvdsr01 20185 |
. . . . 5
β’ ((π β Ring β§ (πΊβπΌ) β (Baseβπ)) β (πΊβπΌ) β₯
(0gβπ)) |
17 | 5, 13, 16 | syl2anc 585 |
. . . 4
β’ ((π
β DivRing β§ πΌ β π β§ π β πΌ) β (πΊβπΌ) β₯
(0gβπ)) |
18 | 17 | adantr 482 |
. . 3
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ = {(0gβπ)}) β (πΊβπΌ) β₯
(0gβπ)) |
19 | | eleq2 2823 |
. . . . . 6
β’ (πΌ = {(0gβπ)} β (π β πΌ β π β {(0gβπ)})) |
20 | 19 | biimpac 480 |
. . . . 5
β’ ((π β πΌ β§ πΌ = {(0gβπ)}) β π β {(0gβπ)}) |
21 | 20 | 3ad2antl3 1188 |
. . . 4
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ = {(0gβπ)}) β π β {(0gβπ)}) |
22 | | elsni 4646 |
. . . 4
β’ (π β
{(0gβπ)}
β π =
(0gβπ)) |
23 | 21, 22 | syl 17 |
. . 3
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ = {(0gβπ)}) β π = (0gβπ)) |
24 | 18, 23 | breqtrrd 5177 |
. 2
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ = {(0gβπ)}) β (πΊβπΌ) β₯ π) |
25 | | simpl1 1192 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β π
β DivRing) |
26 | 25, 1 | syl 17 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β π
β Ring) |
27 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β πΌ β π) |
28 | 27, 8 | syl 17 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β πΌ β (Baseβπ)) |
29 | | simpl3 1194 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β π β πΌ) |
30 | 28, 29 | sseldd 3984 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β π β (Baseβπ)) |
31 | | simpr 486 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β πΌ β {(0gβπ)}) |
32 | | eqid 2733 |
. . . . . . . . . . 11
β’ (
deg1 βπ
) =
( deg1 βπ
) |
33 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Monic1pβπ
) = (Monic1pβπ
) |
34 | 2, 10, 15, 7, 32, 33 | ig1pval3 25692 |
. . . . . . . . . 10
β’ ((π
β DivRing β§ πΌ β π β§ πΌ β {(0gβπ)}) β ((πΊβπΌ) β πΌ β§ (πΊβπΌ) β (Monic1pβπ
) β§ (( deg1
βπ
)β(πΊβπΌ)) = inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, <
))) |
35 | 25, 27, 31, 34 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((πΊβπΌ) β πΌ β§ (πΊβπΌ) β (Monic1pβπ
) β§ (( deg1
βπ
)β(πΊβπΌ)) = inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, <
))) |
36 | 35 | simp2d 1144 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΊβπΌ) β (Monic1pβπ
)) |
37 | | eqid 2733 |
. . . . . . . . 9
β’
(Unic1pβπ
) = (Unic1pβπ
) |
38 | 37, 33 | mon1puc1p 25668 |
. . . . . . . 8
β’ ((π
β Ring β§ (πΊβπΌ) β (Monic1pβπ
)) β (πΊβπΌ) β (Unic1pβπ
)) |
39 | 26, 36, 38 | syl2anc 585 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΊβπΌ) β (Unic1pβπ
)) |
40 | | eqid 2733 |
. . . . . . . 8
β’
(rem1pβπ
) = (rem1pβπ
) |
41 | 40, 2, 6, 37, 32 | r1pdeglt 25676 |
. . . . . . 7
β’ ((π
β Ring β§ π β (Baseβπ) β§ (πΊβπΌ) β (Unic1pβπ
)) β (( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) < (( deg1 βπ
)β(πΊβπΌ))) |
42 | 26, 30, 39, 41 | syl3anc 1372 |
. . . . . 6
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) < (( deg1 βπ
)β(πΊβπΌ))) |
43 | 35 | simp3d 1145 |
. . . . . 6
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
)β(πΊβπΌ)) = inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, <
)) |
44 | 42, 43 | breqtrd 5175 |
. . . . 5
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) < inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, <
)) |
45 | 32, 2, 6 | deg1xrf 25599 |
. . . . . . 7
β’ (
deg1 βπ
):(Baseβπ)βΆβ* |
46 | 35 | simp1d 1143 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΊβπΌ) β πΌ) |
47 | 28, 46 | sseldd 3984 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΊβπΌ) β (Baseβπ)) |
48 | | eqid 2733 |
. . . . . . . . . . 11
β’
(quot1pβπ
) = (quot1pβπ
) |
49 | | eqid 2733 |
. . . . . . . . . . 11
β’
(.rβπ) = (.rβπ) |
50 | | eqid 2733 |
. . . . . . . . . . 11
β’
(-gβπ) = (-gβπ) |
51 | 40, 2, 6, 48, 49, 50 | r1pval 25674 |
. . . . . . . . . 10
β’ ((π β (Baseβπ) β§ (πΊβπΌ) β (Baseβπ)) β (π(rem1pβπ
)(πΊβπΌ)) = (π(-gβπ)((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ)))) |
52 | 30, 47, 51 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (π(rem1pβπ
)(πΊβπΌ)) = (π(-gβπ)((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ)))) |
53 | 26, 3 | syl 17 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β π β Ring) |
54 | 48, 2, 6, 37 | q1pcl 25673 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π β (Baseβπ) β§ (πΊβπΌ) β (Unic1pβπ
)) β (π(quot1pβπ
)(πΊβπΌ)) β (Baseβπ)) |
55 | 26, 30, 39, 54 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (π(quot1pβπ
)(πΊβπΌ)) β (Baseβπ)) |
56 | 7, 6, 49 | lidlmcl 20840 |
. . . . . . . . . . 11
β’ (((π β Ring β§ πΌ β π) β§ ((π(quot1pβπ
)(πΊβπΌ)) β (Baseβπ) β§ (πΊβπΌ) β πΌ)) β ((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ)) β πΌ) |
57 | 53, 27, 55, 46, 56 | syl22anc 838 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ)) β πΌ) |
58 | 7, 50 | lidlsubcl 20839 |
. . . . . . . . . 10
β’ (((π β Ring β§ πΌ β π) β§ (π β πΌ β§ ((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ)) β πΌ)) β (π(-gβπ)((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ))) β πΌ) |
59 | 53, 27, 29, 57, 58 | syl22anc 838 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (π(-gβπ)((π(quot1pβπ
)(πΊβπΌ))(.rβπ)(πΊβπΌ))) β πΌ) |
60 | 52, 59 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (π(rem1pβπ
)(πΊβπΌ)) β πΌ) |
61 | 28, 60 | sseldd 3984 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (π(rem1pβπ
)(πΊβπΌ)) β (Baseβπ)) |
62 | | ffvelcdm 7084 |
. . . . . . 7
β’ (((
deg1 βπ
):(Baseβπ)βΆβ* β§ (π(rem1pβπ
)(πΊβπΌ)) β (Baseβπ)) β (( deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β
β*) |
63 | 45, 61, 62 | sylancr 588 |
. . . . . 6
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β
β*) |
64 | 28 | ssdifd 4141 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΌ β {(0gβπ)}) β ((Baseβπ) β
{(0gβπ)})) |
65 | | imass2 6102 |
. . . . . . . . . 10
β’ ((πΌ β
{(0gβπ)})
β ((Baseβπ)
β {(0gβπ)}) β (( deg1 βπ
) β (πΌ β {(0gβπ)})) β (( deg1
βπ
) β
((Baseβπ) β
{(0gβπ)}))) |
66 | 64, 65 | syl 17 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
) β (πΌ β
{(0gβπ)}))
β (( deg1 βπ
) β ((Baseβπ) β {(0gβπ)}))) |
67 | 32, 2, 15, 6 | deg1n0ima 25607 |
. . . . . . . . . . 11
β’ (π
β Ring β ((
deg1 βπ
)
β ((Baseβπ)
β {(0gβπ)})) β
β0) |
68 | 26, 67 | syl 17 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
) β
((Baseβπ) β
{(0gβπ)}))
β β0) |
69 | | nn0uz 12864 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
70 | 68, 69 | sseqtrdi 4033 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
) β
((Baseβπ) β
{(0gβπ)}))
β (β€β₯β0)) |
71 | 66, 70 | sstrd 3993 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
) β (πΌ β
{(0gβπ)}))
β (β€β₯β0)) |
72 | | uzssz 12843 |
. . . . . . . . 9
β’
(β€β₯β0) β β€ |
73 | | zssre 12565 |
. . . . . . . . . 10
β’ β€
β β |
74 | | ressxr 11258 |
. . . . . . . . . 10
β’ β
β β* |
75 | 73, 74 | sstri 3992 |
. . . . . . . . 9
β’ β€
β β* |
76 | 72, 75 | sstri 3992 |
. . . . . . . 8
β’
(β€β₯β0) β
β* |
77 | 71, 76 | sstrdi 3995 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
) β (πΌ β
{(0gβπ)}))
β β*) |
78 | 7, 15 | lidl0cl 20835 |
. . . . . . . . . . . 12
β’ ((π β Ring β§ πΌ β π) β (0gβπ) β πΌ) |
79 | 53, 27, 78 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β
(0gβπ)
β πΌ) |
80 | 79 | snssd 4813 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β
{(0gβπ)}
β πΌ) |
81 | 31 | necomd 2997 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β
{(0gβπ)}
β πΌ) |
82 | | pssdifn0 4366 |
. . . . . . . . . 10
β’
(({(0gβπ)} β πΌ β§ {(0gβπ)} β πΌ) β (πΌ β {(0gβπ)}) β
β
) |
83 | 80, 81, 82 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΌ β {(0gβπ)}) β
β
) |
84 | | ffn 6718 |
. . . . . . . . . . . 12
β’ ((
deg1 βπ
):(Baseβπ)βΆβ* β (
deg1 βπ
)
Fn (Baseβπ)) |
85 | 45, 84 | ax-mp 5 |
. . . . . . . . . . 11
β’ (
deg1 βπ
)
Fn (Baseβπ) |
86 | 28 | ssdifssd 4143 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΌ β {(0gβπ)}) β (Baseβπ)) |
87 | | fnimaeq0 6684 |
. . . . . . . . . . 11
β’ (((
deg1 βπ
)
Fn (Baseβπ) β§
(πΌ β
{(0gβπ)})
β (Baseβπ))
β ((( deg1 βπ
) β (πΌ β {(0gβπ)})) = β
β (πΌ β
{(0gβπ)})
= β
)) |
88 | 85, 86, 87 | sylancr 588 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((( deg1
βπ
) β (πΌ β
{(0gβπ)}))
= β
β (πΌ β
{(0gβπ)})
= β
)) |
89 | 88 | necon3bid 2986 |
. . . . . . . . 9
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((( deg1
βπ
) β (πΌ β
{(0gβπ)}))
β β
β (πΌ
β {(0gβπ)}) β β
)) |
90 | 83, 89 | mpbird 257 |
. . . . . . . 8
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (( deg1
βπ
) β (πΌ β
{(0gβπ)}))
β β
) |
91 | | infssuzcl 12916 |
. . . . . . . 8
β’ ((((
deg1 βπ
)
β (πΌ β
{(0gβπ)}))
β (β€β₯β0) β§ (( deg1 βπ
) β (πΌ β {(0gβπ)})) β β
) β inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β ((
deg1 βπ
)
β (πΌ β
{(0gβπ)}))) |
92 | 71, 90, 91 | syl2anc 585 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β ((
deg1 βπ
)
β (πΌ β
{(0gβπ)}))) |
93 | 77, 92 | sseldd 3984 |
. . . . . 6
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β
β*) |
94 | | xrltnle 11281 |
. . . . . 6
β’ ((((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β β* β§ inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β
β*) β ((( deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))) < inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, < ) β
Β¬ inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))))) |
95 | 63, 93, 94 | syl2anc 585 |
. . . . 5
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) < inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, < ) β
Β¬ inf((( deg1 βπ
) β (πΌ β {(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))))) |
96 | 44, 95 | mpbid 231 |
. . . 4
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β Β¬ inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ)))) |
97 | 71 | adantr 482 |
. . . . . . 7
β’ ((((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) β (( deg1
βπ
) β (πΌ β
{(0gβπ)}))
β (β€β₯β0)) |
98 | 60 | adantr 482 |
. . . . . . . . 9
β’ ((((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) β (π(rem1pβπ
)(πΊβπΌ)) β πΌ) |
99 | | simpr 486 |
. . . . . . . . 9
β’ ((((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) β (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) |
100 | | eldifsn 4791 |
. . . . . . . . 9
β’ ((π(rem1pβπ
)(πΊβπΌ)) β (πΌ β {(0gβπ)}) β ((π(rem1pβπ
)(πΊβπΌ)) β πΌ β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ))) |
101 | 98, 99, 100 | sylanbrc 584 |
. . . . . . . 8
β’ ((((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) β (π(rem1pβπ
)(πΊβπΌ)) β (πΌ β {(0gβπ)})) |
102 | | fnfvima 7235 |
. . . . . . . 8
β’ (((
deg1 βπ
)
Fn (Baseβπ) β§
(πΌ β
{(0gβπ)})
β (Baseβπ)
β§ (π(rem1pβπ
)(πΊβπΌ)) β (πΌ β {(0gβπ)})) β (( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β (( deg1 βπ
) β (πΌ β {(0gβπ)}))) |
103 | 85, 86, 101, 102 | mp3an2ani 1469 |
. . . . . . 7
β’ ((((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) β (( deg1
βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β (( deg1 βπ
) β (πΌ β {(0gβπ)}))) |
104 | | infssuzle 12915 |
. . . . . . 7
β’ ((((
deg1 βπ
)
β (πΌ β
{(0gβπ)}))
β (β€β₯β0) β§ (( deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β (( deg1 βπ
) β (πΌ β {(0gβπ)}))) β inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ)))) |
105 | 97, 103, 104 | syl2anc 585 |
. . . . . 6
β’ ((((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β§ (π(rem1pβπ
)(πΊβπΌ)) β (0gβπ)) β inf((( deg1
βπ
) β (πΌ β
{(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ)))) |
106 | 105 | ex 414 |
. . . . 5
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((π(rem1pβπ
)(πΊβπΌ)) β (0gβπ) β inf((( deg1
βπ
) β (πΌ β
{(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))))) |
107 | 106 | necon1bd 2959 |
. . . 4
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (Β¬ inf(((
deg1 βπ
)
β (πΌ β
{(0gβπ)})), β, < ) β€ ((
deg1 βπ
)β(π(rem1pβπ
)(πΊβπΌ))) β (π(rem1pβπ
)(πΊβπΌ)) = (0gβπ))) |
108 | 96, 107 | mpd 15 |
. . 3
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (π(rem1pβπ
)(πΊβπΌ)) = (0gβπ)) |
109 | 2, 14, 6, 37, 15, 40 | dvdsr1p 25679 |
. . . 4
β’ ((π
β Ring β§ π β (Baseβπ) β§ (πΊβπΌ) β (Unic1pβπ
)) β ((πΊβπΌ) β₯ π β (π(rem1pβπ
)(πΊβπΌ)) = (0gβπ))) |
110 | 26, 30, 39, 109 | syl3anc 1372 |
. . 3
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β ((πΊβπΌ) β₯ π β (π(rem1pβπ
)(πΊβπΌ)) = (0gβπ))) |
111 | 108, 110 | mpbird 257 |
. 2
β’ (((π
β DivRing β§ πΌ β π β§ π β πΌ) β§ πΌ β {(0gβπ)}) β (πΊβπΌ) β₯ π) |
112 | 24, 111 | pm2.61dane 3030 |
1
β’ ((π
β DivRing β§ πΌ β π β§ π β πΌ) β (πΊβπΌ) β₯ π) |