# Metamath Proof Explorer

## Theorem plydivex

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plydiv.pl ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
plydiv.tm ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
plydiv.rc ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {x}\ne 0\right)\right)\to \frac{1}{{x}}\in {S}$
plydiv.m1 ${⊢}{\phi }\to -1\in {S}$
plydiv.f ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
plydiv.g ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
plydiv.z ${⊢}{\phi }\to {G}\ne {0}_{𝑝}$
plydiv.r ${⊢}{R}={F}{-}_{f}\left({G}{×}_{f}{q}\right)$
Assertion plydivex ${⊢}{\phi }\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)$

### Proof

Step Hyp Ref Expression
1 plydiv.pl ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
2 plydiv.tm ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
3 plydiv.rc ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {x}\ne 0\right)\right)\to \frac{1}{{x}}\in {S}$
4 plydiv.m1 ${⊢}{\phi }\to -1\in {S}$
5 plydiv.f ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
6 plydiv.g ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
7 plydiv.z ${⊢}{\phi }\to {G}\ne {0}_{𝑝}$
8 plydiv.r ${⊢}{R}={F}{-}_{f}\left({G}{×}_{f}{q}\right)$
9 dgrcl ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({F}\right)\in {ℕ}_{0}$
10 5 9 syl ${⊢}{\phi }\to \mathrm{deg}\left({F}\right)\in {ℕ}_{0}$
11 10 nn0red ${⊢}{\phi }\to \mathrm{deg}\left({F}\right)\in ℝ$
12 dgrcl ${⊢}{G}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({G}\right)\in {ℕ}_{0}$
13 6 12 syl ${⊢}{\phi }\to \mathrm{deg}\left({G}\right)\in {ℕ}_{0}$
14 13 nn0red ${⊢}{\phi }\to \mathrm{deg}\left({G}\right)\in ℝ$
15 11 14 resubcld ${⊢}{\phi }\to \mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)\in ℝ$
16 arch ${⊢}\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)\in ℝ\to \exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}$
17 15 16 syl ${⊢}{\phi }\to \exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}$
18 olc ${⊢}\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\to \left({F}={0}_{𝑝}\vee \mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\right)$
19 eqeq1 ${⊢}{f}={F}\to \left({f}={0}_{𝑝}↔{F}={0}_{𝑝}\right)$
20 fveq2 ${⊢}{f}={F}\to \mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)$
21 20 oveq1d ${⊢}{f}={F}\to \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)=\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)$
22 21 breq1d ${⊢}{f}={F}\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}↔\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\right)$
23 19 22 orbi12d ${⊢}{f}={F}\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)↔\left({F}={0}_{𝑝}\vee \mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\right)$
24 oveq1 ${⊢}{f}={F}\to {f}{-}_{f}\left({G}{×}_{f}{q}\right)={F}{-}_{f}\left({G}{×}_{f}{q}\right)$
25 24 8 syl6eqr ${⊢}{f}={F}\to {f}{-}_{f}\left({G}{×}_{f}{q}\right)={R}$
26 25 eqeq1d ${⊢}{f}={F}\to \left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}↔{R}={0}_{𝑝}\right)$
27 25 fveq2d ${⊢}{f}={F}\to \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)=\mathrm{deg}\left({R}\right)$
28 27 breq1d ${⊢}{f}={F}\to \left(\mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)↔\mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)$
29 26 28 orbi12d ${⊢}{f}={F}\to \left(\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)↔\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)\right)$
30 29 rexbidv ${⊢}{f}={F}\to \left(\exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)↔\exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)\right)$
31 23 30 imbi12d ${⊢}{f}={F}\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left({F}={0}_{𝑝}\vee \mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
32 nnnn0 ${⊢}{d}\in ℕ\to {d}\in {ℕ}_{0}$
33 breq2 ${⊢}{x}=0\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}↔\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)$
34 33 orbi2d ${⊢}{x}=0\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)↔\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)$
35 34 imbi1d ${⊢}{x}=0\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
36 35 ralbidv ${⊢}{x}=0\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
37 36 imbi2d ${⊢}{x}=0\to \left(\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)↔\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
38 breq2 ${⊢}{x}={d}\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}↔\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)$
39 38 orbi2d ${⊢}{x}={d}\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)↔\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\right)$
40 39 imbi1d ${⊢}{x}={d}\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
41 40 ralbidv ${⊢}{x}={d}\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
42 41 imbi2d ${⊢}{x}={d}\to \left(\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)↔\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
43 breq2 ${⊢}{x}={d}+1\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}↔\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)$
44 43 orbi2d ${⊢}{x}={d}+1\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)↔\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\right)$
45 44 imbi1d ${⊢}{x}={d}+1\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
46 45 ralbidv ${⊢}{x}={d}+1\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
47 46 imbi2d ${⊢}{x}={d}+1\to \left(\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{x}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)↔\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
48 1 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
49 2 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
50 3 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\wedge \left({x}\in {S}\wedge {x}\ne 0\right)\right)\to \frac{1}{{x}}\in {S}$
51 4 adantr ${⊢}\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\to -1\in {S}$
52 simprl ${⊢}\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\to {f}\in \mathrm{Poly}\left({S}\right)$
53 6 adantr ${⊢}\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\to {G}\in \mathrm{Poly}\left({S}\right)$
54 7 adantr ${⊢}\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\to {G}\ne {0}_{𝑝}$
55 eqid ${⊢}{f}{-}_{f}\left({G}{×}_{f}{q}\right)={f}{-}_{f}\left({G}{×}_{f}{q}\right)$
56 simprr ${⊢}\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\to \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)$
57 48 49 50 51 52 53 54 55 56 plydivlem3 ${⊢}\left({\phi }\wedge \left({f}\in \mathrm{Poly}\left({S}\right)\wedge \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\right)\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)$
58 57 expr ${⊢}\left({\phi }\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
59 58 ralrimiva ${⊢}{\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<0\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
60 eqeq1 ${⊢}{f}={g}\to \left({f}={0}_{𝑝}↔{g}={0}_{𝑝}\right)$
61 fveq2 ${⊢}{f}={g}\to \mathrm{deg}\left({f}\right)=\mathrm{deg}\left({g}\right)$
62 61 oveq1d ${⊢}{f}={g}\to \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)=\mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)$
63 62 breq1d ${⊢}{f}={g}\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}↔\mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)$
64 60 63 orbi12d ${⊢}{f}={g}\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)↔\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\right)$
65 oveq1 ${⊢}{f}={g}\to {f}{-}_{f}\left({G}{×}_{f}{q}\right)={g}{-}_{f}\left({G}{×}_{f}{q}\right)$
66 65 eqeq1d ${⊢}{f}={g}\to \left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}↔{g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\right)$
67 65 fveq2d ${⊢}{f}={g}\to \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)=\mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)$
68 67 breq1d ${⊢}{f}={g}\to \left(\mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)↔\mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)$
69 66 68 orbi12d ${⊢}{f}={g}\to \left(\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)↔\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
70 69 rexbidv ${⊢}{f}={g}\to \left(\exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)↔\exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
71 64 70 imbi12d ${⊢}{f}={g}\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
72 71 cbvralvw ${⊢}\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
73 simplll ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to {\phi }$
74 73 1 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
75 73 2 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
76 73 3 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\wedge \left({x}\in {S}\wedge {x}\ne 0\right)\right)\to \frac{1}{{x}}\in {S}$
77 73 4 syl ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to -1\in {S}$
78 simplr ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to {f}\in \mathrm{Poly}\left({S}\right)$
79 73 6 syl ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to {G}\in \mathrm{Poly}\left({S}\right)$
80 73 7 syl ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to {G}\ne {0}_{𝑝}$
81 simpllr ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to {d}\in {ℕ}_{0}$
82 simprrr ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}$
83 simprrl ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to {f}\ne {0}_{𝑝}$
84 eqid ${⊢}{g}{-}_{f}\left({G}{×}_{f}{p}\right)={g}{-}_{f}\left({G}{×}_{f}{p}\right)$
85 oveq1 ${⊢}{w}={z}\to {{w}}^{{d}}={{z}}^{{d}}$
86 85 oveq2d ${⊢}{w}={z}\to \left(\frac{\mathrm{coeff}\left({f}\right)\left(\mathrm{deg}\left({f}\right)\right)}{\mathrm{coeff}\left({G}\right)\left(\mathrm{deg}\left({G}\right)\right)}\right){{w}}^{{d}}=\left(\frac{\mathrm{coeff}\left({f}\right)\left(\mathrm{deg}\left({f}\right)\right)}{\mathrm{coeff}\left({G}\right)\left(\mathrm{deg}\left({G}\right)\right)}\right){{z}}^{{d}}$
87 86 cbvmptv ${⊢}\left({w}\in ℂ⟼\left(\frac{\mathrm{coeff}\left({f}\right)\left(\mathrm{deg}\left({f}\right)\right)}{\mathrm{coeff}\left({G}\right)\left(\mathrm{deg}\left({G}\right)\right)}\right){{w}}^{{d}}\right)=\left({z}\in ℂ⟼\left(\frac{\mathrm{coeff}\left({f}\right)\left(\mathrm{deg}\left({f}\right)\right)}{\mathrm{coeff}\left({G}\right)\left(\mathrm{deg}\left({G}\right)\right)}\right){{z}}^{{d}}\right)$
88 simprl ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to \forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
89 oveq2 ${⊢}{q}={p}\to {G}{×}_{f}{q}={G}{×}_{f}{p}$
90 89 oveq2d ${⊢}{q}={p}\to {g}{-}_{f}\left({G}{×}_{f}{q}\right)={g}{-}_{f}\left({G}{×}_{f}{p}\right)$
91 90 eqeq1d ${⊢}{q}={p}\to \left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}↔{g}{-}_{f}\left({G}{×}_{f}{p}\right)={0}_{𝑝}\right)$
92 90 fveq2d ${⊢}{q}={p}\to \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)=\mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)$
93 92 breq1d ${⊢}{q}={p}\to \left(\mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)↔\mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)<\mathrm{deg}\left({G}\right)\right)$
94 91 93 orbi12d ${⊢}{q}={p}\to \left(\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)↔\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
95 94 cbvrexvw ${⊢}\exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)↔\exists {p}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)<\mathrm{deg}\left({G}\right)\right)$
96 95 imbi2i ${⊢}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {p}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
97 96 ralbii ${⊢}\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {p}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
98 88 97 sylib ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to \forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {p}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{p}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
99 eqid ${⊢}\mathrm{coeff}\left({f}\right)=\mathrm{coeff}\left({f}\right)$
100 eqid ${⊢}\mathrm{coeff}\left({G}\right)=\mathrm{coeff}\left({G}\right)$
101 eqid ${⊢}\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({f}\right)$
102 eqid ${⊢}\mathrm{deg}\left({G}\right)=\mathrm{deg}\left({G}\right)$
103 74 75 76 77 78 79 80 55 81 82 83 84 87 98 99 100 101 102 plydivlem4 ${⊢}\left(\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)$
104 103 exp32 ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\to \left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
105 104 ralrimdva ${⊢}\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\to \left(\forall {g}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({g}={0}_{𝑝}\vee \mathrm{deg}\left({g}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({g}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
106 72 105 syl5bi ${⊢}\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
107 106 ancld ${⊢}\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
108 dgrcl ${⊢}{f}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({f}\right)\in {ℕ}_{0}$
109 108 adantl ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \mathrm{deg}\left({f}\right)\in {ℕ}_{0}$
110 109 nn0zd ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \mathrm{deg}\left({f}\right)\in ℤ$
111 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to {G}\in \mathrm{Poly}\left({S}\right)$
112 111 12 syl ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \mathrm{deg}\left({G}\right)\in {ℕ}_{0}$
113 112 nn0zd ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \mathrm{deg}\left({G}\right)\in ℤ$
114 110 113 zsubcld ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)\in ℤ$
115 nn0z ${⊢}{d}\in {ℕ}_{0}\to {d}\in ℤ$
116 115 ad2antlr ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to {d}\in ℤ$
117 zleltp1 ${⊢}\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)\in ℤ\wedge {d}\in ℤ\right)\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)\le {d}↔\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)$
118 114 116 117 syl2anc ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)\le {d}↔\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)$
119 114 zred ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)\in ℝ$
120 nn0re ${⊢}{d}\in {ℕ}_{0}\to {d}\in ℝ$
121 120 ad2antlr ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to {d}\in ℝ$
122 119 121 leloed ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)\le {d}↔\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
123 118 122 bitr3d ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1↔\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
124 123 orbi2d ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)↔\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)$
125 pm5.63 ${⊢}\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)↔\left({f}={0}_{𝑝}\vee \left(¬{f}={0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
126 df-ne ${⊢}{f}\ne {0}_{𝑝}↔¬{f}={0}_{𝑝}$
127 126 anbi1i ${⊢}\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)↔\left(¬{f}={0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)$
128 127 orbi2i ${⊢}\left({f}={0}_{𝑝}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)↔\left({f}={0}_{𝑝}\vee \left(¬{f}={0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
129 125 128 bitr4i ${⊢}\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)↔\left({f}={0}_{𝑝}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
130 129 orbi2i ${⊢}\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)↔\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}={0}_{𝑝}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)$
131 or12 ${⊢}\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)↔\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
132 or12 ${⊢}\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)↔\left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}={0}_{𝑝}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)$
133 130 131 132 3bitr4i ${⊢}\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)↔\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)$
134 orass ${⊢}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)↔\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)$
135 133 134 bitr4i ${⊢}\left({f}={0}_{𝑝}\vee \left(\mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)↔\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)$
136 124 135 syl6bb ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)↔\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\right)$
137 136 imbi1d ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
138 jaob ${⊢}\left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\vee \left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
139 137 138 syl6bb ${⊢}\left(\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\wedge {f}\in \mathrm{Poly}\left({S}\right)\right)\to \left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
140 139 ralbidva ${⊢}\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
141 r19.26 ${⊢}\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)↔\left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
142 140 141 syl6bb ${⊢}\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)↔\left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\wedge \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\ne {0}_{𝑝}\wedge \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)={d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
143 107 142 sylibrd ${⊢}\left({\phi }\wedge {d}\in {ℕ}_{0}\right)\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
144 143 expcom ${⊢}{d}\in {ℕ}_{0}\to \left({\phi }\to \left(\forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
145 144 a2d ${⊢}{d}\in {ℕ}_{0}\to \left(\left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\to \left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}+1\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)\right)$
146 37 42 47 42 59 145 nn0ind ${⊢}{d}\in {ℕ}_{0}\to \left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
147 32 146 syl ${⊢}{d}\in ℕ\to \left({\phi }\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)\right)$
148 147 impcom ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \forall {f}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}={0}_{𝑝}\vee \mathrm{deg}\left({f}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)={0}_{𝑝}\vee \mathrm{deg}\left({f}{-}_{f}\left({G}{×}_{f}{q}\right)\right)<\mathrm{deg}\left({G}\right)\right)\right)$
149 5 adantr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {F}\in \mathrm{Poly}\left({S}\right)$
150 31 148 149 rspcdva ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left(\left({F}={0}_{𝑝}\vee \mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\right)\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)\right)$
151 18 150 syl5 ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left(\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)\right)$
152 151 rexlimdva ${⊢}{\phi }\to \left(\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}\mathrm{deg}\left({F}\right)-\mathrm{deg}\left({G}\right)<{d}\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)\right)$
153 17 152 mpd ${⊢}{\phi }\to \exists {q}\in \mathrm{Poly}\left({S}\right)\phantom{\rule{.4em}{0ex}}\left({R}={0}_{𝑝}\vee \mathrm{deg}\left({R}\right)<\mathrm{deg}\left({G}\right)\right)$