Metamath Proof Explorer

Theorem plydivex

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

Ref Expression
Hypotheses plydiv.pl ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
plydiv.tm ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
plydiv.rc ⊢ φ ∧ x ∈ S ∧ x ≠ 0 → 1 x ∈ S
plydiv.m1 ⊢ φ → − 1 ∈ S
plydiv.f ⊢ φ → F ∈ Poly ⁡ S
plydiv.g ⊢ φ → G ∈ Poly ⁡ S
plydiv.z ⊢ φ → G ≠ 0 𝑝
plydiv.r ⊢ R = F − f G × f q
Assertion plydivex ⊢ φ → ∃ q ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G

Proof

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