# Metamath Proof Explorer

## Theorem ply1divmo

Description: Uniqueness of a quotient in a polynomial division. For polynomials F , G such that G =/= 0 and the leading coefficient of G is not a zero divisor, there is at most one polynomial q which satisfies F = ( G x. q ) + r where the degree of r is less than the degree of G . (Contributed by Stefan O'Rear, 26-Mar-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Hypotheses ply1divalg.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
ply1divalg.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
ply1divalg.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
ply1divalg.m
ply1divalg.z
ply1divalg.t
ply1divalg.r1 ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
ply1divalg.f ${⊢}{\phi }\to {F}\in {B}$
ply1divalg.g1 ${⊢}{\phi }\to {G}\in {B}$
ply1divalg.g2
ply1divmo.g3 ${⊢}{\phi }\to {\mathrm{coe}}_{1}\left({G}\right)\left({D}\left({G}\right)\right)\in {E}$
ply1divmo.e ${⊢}{E}=\mathrm{RLReg}\left({R}\right)$
Assertion ply1divmo

### Proof

Step Hyp Ref Expression
1 ply1divalg.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ply1divalg.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
3 ply1divalg.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
4 ply1divalg.m
5 ply1divalg.z
6 ply1divalg.t
7 ply1divalg.r1 ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
8 ply1divalg.f ${⊢}{\phi }\to {F}\in {B}$
9 ply1divalg.g1 ${⊢}{\phi }\to {G}\in {B}$
10 ply1divalg.g2
11 ply1divmo.g3 ${⊢}{\phi }\to {\mathrm{coe}}_{1}\left({G}\right)\left({D}\left({G}\right)\right)\in {E}$
12 ply1divmo.e ${⊢}{E}=\mathrm{RLReg}\left({R}\right)$
13 7 adantr ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {R}\in \mathrm{Ring}$
14 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
15 13 14 syl ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {P}\in \mathrm{Ring}$
16 ringgrp ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{Grp}$
17 15 16 syl ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {P}\in \mathrm{Grp}$
18 8 adantr ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {F}\in {B}$
19 9 adantr ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {G}\in {B}$
20 simprl ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {q}\in {B}$
21 3 6 ringcl
22 15 19 20 21 syl3anc
23 3 4 grpsubcl
24 17 18 22 23 syl3anc
25 simprr ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {r}\in {B}$
26 3 6 ringcl
27 15 19 25 26 syl3anc
28 3 4 grpsubcl
29 17 18 27 28 syl3anc
30 3 4 grpsubcl
31 17 24 29 30 syl3anc
32 2 1 3 deg1xrcl
33 31 32 syl
34 2 1 3 deg1xrcl
35 29 34 syl
36 2 1 3 deg1xrcl
37 24 36 syl
38 35 37 ifcld
39 2 1 3 deg1xrcl ${⊢}{G}\in {B}\to {D}\left({G}\right)\in {ℝ}^{*}$
40 19 39 syl ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {D}\left({G}\right)\in {ℝ}^{*}$
41 33 38 40 3jca
42 41 adantr
43 1 2 13 3 4 24 29 deg1suble
44 43 adantr
45 xrmaxlt
46 37 35 40 45 syl3anc
47 46 biimpar
48 44 47 jca
49 xrlelttr
50 42 48 49 sylc
51 50 ex
52 2 1 5 3 deg1nn0cl
53 7 9 10 52 syl3anc ${⊢}{\phi }\to {D}\left({G}\right)\in {ℕ}_{0}$
54 53 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\wedge {q}\ne {r}\right)\to {D}\left({G}\right)\in {ℕ}_{0}$
55 54 nn0red ${⊢}\left(\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\wedge {q}\ne {r}\right)\to {D}\left({G}\right)\in ℝ$
56 7 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\wedge {q}\ne {r}\right)\to {R}\in \mathrm{Ring}$
57 3 4 grpsubcl
58 17 25 20 57 syl3anc
59 58 adantr
60 3 5 4 grpsubeq0
61 17 25 20 60 syl3anc
62 equcom ${⊢}{r}={q}↔{q}={r}$
63 61 62 syl6bb
64 63 necon3bid
65 64 biimpar
66 2 1 5 3 deg1nn0cl
67 56 59 65 66 syl3anc
68 nn0addge1
69 55 67 68 syl2anc
70 9 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\wedge {q}\ne {r}\right)\to {G}\in {B}$
71 10 ad2antrr
72 11 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\wedge {q}\ne {r}\right)\to {\mathrm{coe}}_{1}\left({G}\right)\left({D}\left({G}\right)\right)\in {E}$
73 2 1 12 3 6 5 56 70 71 72 59 65 deg1mul2
74 69 73 breqtrrd
75 ringabl ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{Abel}$
76 15 75 syl ${⊢}\left({\phi }\wedge \left({q}\in {B}\wedge {r}\in {B}\right)\right)\to {P}\in \mathrm{Abel}$
77 3 4 76 18 22 27 ablnnncan1
78 3 6 4 15 19 25 20 ringsubdi
79 77 78 eqtr4d
80 79 fveq2d
81 80 adantr
82 74 81 breqtrrd
83 40 33 xrlenltd
84 83 adantr
85 82 84 mpbid
86 85 ex
87 86 necon4ad
88 51 87 syld
89 88 ralrimivva
90 oveq2
91 90 oveq2d
92 91 fveq2d
93 92 breq1d
94 93 rmo4
95 89 94 sylibr