# Metamath Proof Explorer

## Theorem quotcan

Description: Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis quotcan.1 ${⊢}{H}={F}{×}_{f}{G}$
Assertion quotcan ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}\mathrm{quot}{G}={F}$

### Proof

Step Hyp Ref Expression
1 quotcan.1 ${⊢}{H}={F}{×}_{f}{G}$
2 plyssc ${⊢}\mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left(ℂ\right)$
3 simp2 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {G}\in \mathrm{Poly}\left({S}\right)$
4 2 3 sseldi ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {G}\in \mathrm{Poly}\left(ℂ\right)$
5 simp1 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}\in \mathrm{Poly}\left({S}\right)$
6 2 5 sseldi ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}\in \mathrm{Poly}\left(ℂ\right)$
7 plymulcl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {F}{×}_{f}{G}\in \mathrm{Poly}\left(ℂ\right)$
8 1 7 eqeltrid ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {H}\in \mathrm{Poly}\left(ℂ\right)$
9 8 3adant3 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}\in \mathrm{Poly}\left(ℂ\right)$
10 simp3 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {G}\ne {0}_{𝑝}$
11 quotcl2 ${⊢}\left({H}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}\mathrm{quot}{G}\in \mathrm{Poly}\left(ℂ\right)$
12 9 4 10 11 syl3anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}\mathrm{quot}{G}\in \mathrm{Poly}\left(ℂ\right)$
13 plysubcl ${⊢}\left({F}\in \mathrm{Poly}\left(ℂ\right)\wedge {H}\mathrm{quot}{G}\in \mathrm{Poly}\left(ℂ\right)\right)\to {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)$
14 6 12 13 syl2anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)$
15 plymul0or ${⊢}\left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)\right)\to \left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}↔\left({G}={0}_{𝑝}\vee {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)\right)$
16 4 14 15 syl2anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}↔\left({G}={0}_{𝑝}\vee {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)\right)$
17 cnex ${⊢}ℂ\in \mathrm{V}$
18 17 a1i ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to ℂ\in \mathrm{V}$
19 plyf ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {F}:ℂ⟶ℂ$
20 5 19 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}:ℂ⟶ℂ$
21 plyf ${⊢}{G}\in \mathrm{Poly}\left({S}\right)\to {G}:ℂ⟶ℂ$
22 3 21 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {G}:ℂ⟶ℂ$
23 mulcom ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}{y}={y}{x}$
24 23 adantl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\wedge \left({x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {x}{y}={y}{x}$
25 18 20 22 24 caofcom ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}{×}_{f}{G}={G}{×}_{f}{F}$
26 1 25 syl5eq ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}={G}{×}_{f}{F}$
27 26 oveq1d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)=\left({G}{×}_{f}{F}\right){-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
28 plyf ${⊢}{H}\mathrm{quot}{G}\in \mathrm{Poly}\left(ℂ\right)\to \left({H}\mathrm{quot}{G}\right):ℂ⟶ℂ$
29 12 28 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({H}\mathrm{quot}{G}\right):ℂ⟶ℂ$
30 subdi ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to {x}\left({y}-{z}\right)={x}{y}-{x}{z}$
31 30 adantl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\wedge \left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\right)\to {x}\left({y}-{z}\right)={x}{y}-{x}{z}$
32 18 22 20 29 31 caofdi ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)=\left({G}{×}_{f}{F}\right){-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
33 27 32 eqtr4d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
34 33 eqeq1d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}↔{G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}\right)$
35 10 neneqd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to ¬{G}={0}_{𝑝}$
36 biorf ${⊢}¬{G}={0}_{𝑝}\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}↔\left({G}={0}_{𝑝}\vee {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)\right)$
37 35 36 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}↔\left({G}={0}_{𝑝}\vee {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)\right)$
38 16 34 37 3bitr4d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}↔{F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)$
39 38 biimpd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}\to {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)$
40 eqid ${⊢}\mathrm{deg}\left({G}\right)=\mathrm{deg}\left({G}\right)$
41 eqid ${⊢}\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)=\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
42 40 41 dgrmul ${⊢}\left(\left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\ne {0}_{𝑝}\right)\wedge \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)\wedge {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\ne {0}_{𝑝}\right)\right)\to \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)=\mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
43 42 expr ${⊢}\left(\left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\ne {0}_{𝑝}\right)\wedge {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\ne {0}_{𝑝}\to \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)=\mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)$
44 4 10 14 43 syl21anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\ne {0}_{𝑝}\to \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)=\mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)$
45 dgrcl ${⊢}{G}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({G}\right)\in {ℕ}_{0}$
46 3 45 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({G}\right)\in {ℕ}_{0}$
47 46 nn0red ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({G}\right)\in ℝ$
48 dgrcl ${⊢}{F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)\to \mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\in {ℕ}_{0}$
49 14 48 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\in {ℕ}_{0}$
50 nn0addge1 ${⊢}\left(\mathrm{deg}\left({G}\right)\in ℝ\wedge \mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\in {ℕ}_{0}\right)\to \mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
51 47 49 50 syl2anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
52 breq2 ${⊢}\mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)=\mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\to \left(\mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)↔\mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)$
53 51 52 syl5ibrcom ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left(\mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)=\mathrm{deg}\left({G}\right)+\mathrm{deg}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\to \mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)\right)$
54 44 53 syld ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\ne {0}_{𝑝}\to \mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)\right)$
55 33 fveq2d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)=\mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)$
56 55 breq2d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left(\mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)↔\mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)\right)$
57 plymulcl ${⊢}\left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge {H}\mathrm{quot}{G}\in \mathrm{Poly}\left(ℂ\right)\right)\to {G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)$
58 4 12 57 syl2anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)$
59 plysubcl ${⊢}\left({H}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\in \mathrm{Poly}\left(ℂ\right)\right)\to {H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\in \mathrm{Poly}\left(ℂ\right)$
60 9 58 59 syl2anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\in \mathrm{Poly}\left(ℂ\right)$
61 dgrcl ${⊢}{H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\in \mathrm{Poly}\left(ℂ\right)\to \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)\in {ℕ}_{0}$
62 60 61 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)\in {ℕ}_{0}$
63 62 nn0red ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)\in ℝ$
64 47 63 lenltd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left(\mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)↔¬\mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)<\mathrm{deg}\left({G}\right)\right)$
65 56 64 bitr3d ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left(\mathrm{deg}\left({G}\right)\le \mathrm{deg}\left({G}{×}_{f}\left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)↔¬\mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)<\mathrm{deg}\left({G}\right)\right)$
66 54 65 sylibd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)\ne {0}_{𝑝}\to ¬\mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)<\mathrm{deg}\left({G}\right)\right)$
67 66 necon4ad ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left(\mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)<\mathrm{deg}\left({G}\right)\to {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}\right)$
68 eqid ${⊢}{H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)$
69 68 quotdgr ${⊢}\left({H}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}\vee \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)<\mathrm{deg}\left({G}\right)\right)$
70 9 4 10 69 syl3anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)={0}_{𝑝}\vee \mathrm{deg}\left({H}{-}_{f}\left({G}{×}_{f}\left({H}\mathrm{quot}{G}\right)\right)\right)<\mathrm{deg}\left({G}\right)\right)$
71 39 67 70 mpjaod ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)={0}_{𝑝}$
72 df-0p ${⊢}{0}_{𝑝}=ℂ×\left\{0\right\}$
73 71 72 syl6eq ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}{-}_{f}\left({H}\mathrm{quot}{G}\right)=ℂ×\left\{0\right\}$
74 ofsubeq0 ${⊢}\left(ℂ\in \mathrm{V}\wedge {F}:ℂ⟶ℂ\wedge \left({H}\mathrm{quot}{G}\right):ℂ⟶ℂ\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)=ℂ×\left\{0\right\}↔{F}={H}\mathrm{quot}{G}\right)$
75 18 20 29 74 syl3anc ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to \left({F}{-}_{f}\left({H}\mathrm{quot}{G}\right)=ℂ×\left\{0\right\}↔{F}={H}\mathrm{quot}{G}\right)$
76 73 75 mpbid ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {F}={H}\mathrm{quot}{G}$
77 76 eqcomd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\wedge {G}\ne {0}_{𝑝}\right)\to {H}\mathrm{quot}{G}={F}$