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 = Poly 1 R
ply1divalg.d D = deg 1 R
ply1divalg.b B = Base P
ply1divalg.m - ˙ = - P
ply1divalg.z 0 ˙ = 0 P
ply1divalg.t ˙ = P
ply1divalg.r1 φ R Ring
ply1divalg.f φ F B
ply1divalg.g1 φ G B
ply1divalg.g2 φ G 0 ˙
ply1divmo.g3 φ coe 1 G D G E
ply1divmo.e E = RLReg R
Assertion ply1divmo φ * q B D F - ˙ G ˙ q < D G

Proof

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