Metamath Proof Explorer

Theorem r1pid2

Description: Identity law for polynomial remainder operation: it leaves a polynomial A unchanged iff the degree of A is less than the degree of the divisor B . (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses r1padd1.p ⊢ P = Poly 1 ⁡ R
r1padd1.u ⊢ U = Base P
r1padd1.n ⊢ N = Unic 1p ⁡ R
r1padd1.e ⊢ E = rem 1p ⁡ R
r1pid2.r ⊢ φ → R ∈ IDomn
r1pid2.d ⊢ D = deg 1 ⁡ R
r1pid2.p ⊢ φ → A ∈ U
r1pid2.q ⊢ φ → B ∈ N
Assertion r1pid2 ⊢ φ → A E B = A ↔ D ⁡ A < D ⁡ B

Proof

Step Hyp Ref Expression
1 r1padd1.p ⊢ P = Poly 1 ⁡ R
2 r1padd1.u ⊢ U = Base P
3 r1padd1.n ⊢ N = Unic 1p ⁡ R
4 r1padd1.e ⊢ E = rem 1p ⁡ R
5 r1pid2.r ⊢ φ → R ∈ IDomn
6 r1pid2.d ⊢ D = deg 1 ⁡ R
7 r1pid2.p ⊢ φ → A ∈ U
8 r1pid2.q ⊢ φ → B ∈ N
9 5 idomringd ⊢ φ → R ∈ Ring
10 eqid ⊢ quot 1p ⁡ R = quot 1p ⁡ R
11 eqid ⊢ ⋅ P = ⋅ P
12 eqid ⊢ + P = + P
13 1 2 3 10 4 11 12 r1pid ⊢ R ∈ Ring ∧ A ∈ U ∧ B ∈ N → A = A quot 1p ⁡ R B ⋅ P B + P A E B
14 9 7 8 13 syl3anc ⊢ φ → A = A quot 1p ⁡ R B ⋅ P B + P A E B
15 14 eqeq2d ⊢ φ → A E B = A ↔ A E B = A quot 1p ⁡ R B ⋅ P B + P A E B
16 eqcom ⊢ A quot 1p ⁡ R B ⋅ P B + P A E B = A E B ↔ A E B = A quot 1p ⁡ R B ⋅ P B + P A E B
17 15 16 bitr4di ⊢ φ → A E B = A ↔ A quot 1p ⁡ R B ⋅ P B + P A E B = A E B
18 eqid ⊢ 0 P = 0 P
19 1 ply1ring ⊢ R ∈ Ring → P ∈ Ring
20 9 19 syl ⊢ φ → P ∈ Ring
21 20 ringgrpd ⊢ φ → P ∈ Grp
22 4 1 2 3 r1pcl ⊢ R ∈ Ring ∧ A ∈ U ∧ B ∈ N → A E B ∈ U
23 9 7 8 22 syl3anc ⊢ φ → A E B ∈ U
24 2 12 18 21 23 grplidd ⊢ φ → 0 P + P A E B = A E B
25 24 eqeq2d ⊢ φ → A quot 1p ⁡ R B ⋅ P B + P A E B = 0 P + P A E B ↔ A quot 1p ⁡ R B ⋅ P B + P A E B = A E B
26 10 1 2 3 q1pcl ⊢ R ∈ Ring ∧ A ∈ U ∧ B ∈ N → A quot 1p ⁡ R B ∈ U
27 9 7 8 26 syl3anc ⊢ φ → A quot 1p ⁡ R B ∈ U
28 1 2 3 uc1pcl ⊢ B ∈ N → B ∈ U
29 8 28 syl ⊢ φ → B ∈ U
30 2 11 20 27 29 ringcld ⊢ φ → A quot 1p ⁡ R B ⋅ P B ∈ U
31 2 18 ring0cl ⊢ P ∈ Ring → 0 P ∈ U
32 9 19 31 3syl ⊢ φ → 0 P ∈ U
33 2 12 grprcan ⊢ P ∈ Grp ∧ A quot 1p ⁡ R B ⋅ P B ∈ U ∧ 0 P ∈ U ∧ A E B ∈ U → A quot 1p ⁡ R B ⋅ P B + P A E B = 0 P + P A E B ↔ A quot 1p ⁡ R B ⋅ P B = 0 P
34 21 30 32 23 33 syl13anc ⊢ φ → A quot 1p ⁡ R B ⋅ P B + P A E B = 0 P + P A E B ↔ A quot 1p ⁡ R B ⋅ P B = 0 P
35 17 25 34 3bitr2d ⊢ φ → A E B = A ↔ A quot 1p ⁡ R B ⋅ P B = 0 P
36 isidom ⊢ R ∈ IDomn ↔ R ∈ CRing ∧ R ∈ Domn
37 5 36 sylib ⊢ φ → R ∈ CRing ∧ R ∈ Domn
38 37 simpld ⊢ φ → R ∈ CRing
39 1 ply1crng ⊢ R ∈ CRing → P ∈ CRing
40 38 39 syl ⊢ φ → P ∈ CRing
41 2 11 crngcom ⊢ P ∈ CRing ∧ B ∈ U ∧ A quot 1p ⁡ R B ∈ U → B ⋅ P A quot 1p ⁡ R B = A quot 1p ⁡ R B ⋅ P B
42 40 29 27 41 syl3anc ⊢ φ → B ⋅ P A quot 1p ⁡ R B = A quot 1p ⁡ R B ⋅ P B
43 42 eqeq1d ⊢ φ → B ⋅ P A quot 1p ⁡ R B = 0 P ↔ A quot 1p ⁡ R B ⋅ P B = 0 P
44 5 idomdomd ⊢ φ → R ∈ Domn
45 1 ply1domn ⊢ R ∈ Domn → P ∈ Domn
46 44 45 syl ⊢ φ → P ∈ Domn
47 1 18 3 uc1pn0 ⊢ B ∈ N → B ≠ 0 P
48 8 47 syl ⊢ φ → B ≠ 0 P
49 eqid ⊢ RLReg ⁡ P = RLReg ⁡ P
50 2 49 18 domnrrg ⊢ P ∈ Domn ∧ B ∈ U ∧ B ≠ 0 P → B ∈ RLReg ⁡ P
51 46 29 48 50 syl3anc ⊢ φ → B ∈ RLReg ⁡ P
52 49 2 11 18 rrgeq0 ⊢ P ∈ Ring ∧ B ∈ RLReg ⁡ P ∧ A quot 1p ⁡ R B ∈ U → B ⋅ P A quot 1p ⁡ R B = 0 P ↔ A quot 1p ⁡ R B = 0 P
53 20 51 27 52 syl3anc ⊢ φ → B ⋅ P A quot 1p ⁡ R B = 0 P ↔ A quot 1p ⁡ R B = 0 P
54 35 43 53 3bitr2d ⊢ φ → A E B = A ↔ A quot 1p ⁡ R B = 0 P
55 2 11 18 20 29 ringlzd ⊢ φ → 0 P ⋅ P B = 0 P
56 55 oveq2d ⊢ φ → A - P 0 P ⋅ P B = A - P 0 P
57 eqid ⊢ - P = - P
58 2 18 57 grpsubid1 ⊢ P ∈ Grp ∧ A ∈ U → A - P 0 P = A
59 21 7 58 syl2anc ⊢ φ → A - P 0 P = A
60 56 59 eqtr2d ⊢ φ → A = A - P 0 P ⋅ P B
61 60 fveq2d ⊢ φ → D ⁡ A = D ⁡ A - P 0 P ⋅ P B
62 61 breq1d ⊢ φ → D ⁡ A < D ⁡ B ↔ D ⁡ A - P 0 P ⋅ P B < D ⁡ B
63 32 biantrurd ⊢ φ → D ⁡ A - P 0 P ⋅ P B < D ⁡ B ↔ 0 P ∈ U ∧ D ⁡ A - P 0 P ⋅ P B < D ⁡ B
64 10 1 2 6 57 11 3 q1peqb ⊢ R ∈ Ring ∧ A ∈ U ∧ B ∈ N → 0 P ∈ U ∧ D ⁡ A - P 0 P ⋅ P B < D ⁡ B ↔ A quot 1p ⁡ R B = 0 P
65 9 7 8 64 syl3anc ⊢ φ → 0 P ∈ U ∧ D ⁡ A - P 0 P ⋅ P B < D ⁡ B ↔ A quot 1p ⁡ R B = 0 P
66 62 63 65 3bitrd ⊢ φ → D ⁡ A < D ⁡ B ↔ A quot 1p ⁡ R B = 0 P
67 54 66 bitr4d ⊢ φ → A E B = A ↔ D ⁡ A < D ⁡ B