Metamath Proof Explorer

Theorem plydivlem4

Description: Lemma for plydivex . Induction step. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses plydiv.pl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plydiv.tm ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
plydiv.rc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
plydiv.m1 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
plydiv.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plydiv.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plydiv.z ⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
plydiv.r ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
plydiv.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
plydiv.e ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) = 𝐷 )
plydiv.fz ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
plydiv.u ⊢ 𝑈 = ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑝 ) )
plydiv.h ⊢ 𝐻 = ( 𝑧 ∈ ℂ ↦ ( ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) · ( 𝑧 ↑ 𝐷 ) ) )
plydiv.al ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − 𝑁 ) < 𝐷 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( 𝑈 = 0𝑝 ∨ ( deg ‘ 𝑈 ) < 𝑁 ) ) )
plydiv.a ⊢ 𝐴 = ( coeff ‘ 𝐹 )
plydiv.b ⊢ 𝐵 = ( coeff ‘ 𝐺 )
plydiv.m ⊢ 𝑀 = ( deg ‘ 𝐹 )
plydiv.n ⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion plydivlem4 ( 𝜑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < 𝑁 ) )

Proof

Step Hyp Ref Expression
1 plydiv.pl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 plydiv.tm ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
3 plydiv.rc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
4 plydiv.m1 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
5 plydiv.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6 plydiv.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
7 plydiv.z ⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
8 plydiv.r ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
9 plydiv.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
10 plydiv.e ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) = 𝐷 )
11 plydiv.fz ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
12 plydiv.u ⊢ 𝑈 = ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑝 ) )
13 plydiv.h ⊢ 𝐻 = ( 𝑧 ∈ ℂ ↦ ( ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) · ( 𝑧 ↑ 𝐷 ) ) )
14 plydiv.al ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − 𝑁 ) < 𝐷 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( 𝑈 = 0𝑝 ∨ ( deg ‘ 𝑈 ) < 𝑁 ) ) )
15 plydiv.a ⊢ 𝐴 = ( coeff ‘ 𝐹 )
16 plydiv.b ⊢ 𝐵 = ( coeff ‘ 𝐺 )
17 plydiv.m ⊢ 𝑀 = ( deg ‘ 𝐹 )
18 plydiv.n ⊢ 𝑁 = ( deg ‘ 𝐺 )
19 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
20 5 19 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
21 1 2 3 4 plydivlem1 ⊢ ( 𝜑 → 0 ∈ 𝑆 )
22 15 coef2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ 𝑆 )
23 5 21 22 syl2anc ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ 𝑆 )
24 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
25 5 24 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
26 17 25 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
27 23 26 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ 𝑆 )
28 20 27 sseldd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
29 16 coef2 ⊢ ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → 𝐵 : ℕ0 ⟶ 𝑆 )
30 6 21 29 syl2anc ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ 𝑆 )
31 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
32 6 31 syl ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 )
33 18 32 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
34 30 33 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 )
35 20 34 sseldd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑁 ) ∈ ℂ )
36 18 16 dgreq0 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐺 = 0𝑝 ↔ ( 𝐵 ‘ 𝑁 ) = 0 ) )
37 6 36 syl ⊢ ( 𝜑 → ( 𝐺 = 0𝑝 ↔ ( 𝐵 ‘ 𝑁 ) = 0 ) )
38 37 necon3bid ⊢ ( 𝜑 → ( 𝐺 ≠ 0𝑝 ↔ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) )
39 7 38 mpbid ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑁 ) ≠ 0 )
40 28 35 39 divrecd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 1 / ( 𝐵 ‘ 𝑁 ) ) ) )
41 fvex ⊢ ( 𝐵 ‘ 𝑁 ) ∈ V
42 eleq1 ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( 𝑥 ∈ 𝑆 ↔ ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 ) )
43 neeq1 ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( 𝑥 ≠ 0 ↔ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) )
44 42 43 anbi12d ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ↔ ( ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) ) )
45 44 anbi2d ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) ) ) )
46 oveq2 ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( 1 / 𝑥 ) = ( 1 / ( 𝐵 ‘ 𝑁 ) ) )
47 46 eleq1d ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( ( 1 / 𝑥 ) ∈ 𝑆 ↔ ( 1 / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 ) )
48 45 47 imbi12d ⊢ ( 𝑥 = ( 𝐵 ‘ 𝑁 ) → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝜑 ∧ ( ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) ) → ( 1 / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 ) ) )
49 41 48 3 vtocl ⊢ ( ( 𝜑 ∧ ( ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) ) → ( 1 / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 )
50 49 ex ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐵 ‘ 𝑁 ) ≠ 0 ) → ( 1 / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 ) )
51 34 39 50 mp2and ⊢ ( 𝜑 → ( 1 / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 )
52 2 27 51 caovcld ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) · ( 1 / ( 𝐵 ‘ 𝑁 ) ) ) ∈ 𝑆 )
53 40 52 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 )
54 13 ply1term ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ∈ 𝑆 ∧ 𝐷 ∈ ℕ0 ) → 𝐻 ∈ ( Poly ‘ 𝑆 ) )
55 20 53 9 54 syl3anc ⊢ ( 𝜑 → 𝐻 ∈ ( Poly ‘ 𝑆 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝐻 ∈ ( Poly ‘ 𝑆 ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝑝 ∈ ( Poly ‘ 𝑆 ) )
58 1 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
59 56 57 58 plyadd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐻 ∘f + 𝑝 ) ∈ ( Poly ‘ 𝑆 ) )
60 cnex ⊢ ℂ ∈ V
61 60 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ℂ ∈ V )
62 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
63 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
64 62 63 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 : ℂ ⟶ ℂ )
65 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
66 65 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
67 plyf ⊢ ( 𝐻 ∈ ( Poly ‘ 𝑆 ) → 𝐻 : ℂ ⟶ ℂ )
68 56 67 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝐻 : ℂ ⟶ ℂ )
69 6 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
70 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
71 69 70 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 : ℂ ⟶ ℂ )
72 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
73 66 68 71 61 61 72 off ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐻 ∘f · 𝐺 ) : ℂ ⟶ ℂ )
74 plyf ⊢ ( 𝑝 ∈ ( Poly ‘ 𝑆 ) → 𝑝 : ℂ ⟶ ℂ )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → 𝑝 : ℂ ⟶ ℂ )
76 66 71 75 61 61 72 off ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐺 ∘f · 𝑝 ) : ℂ ⟶ ℂ )
77 subsub4 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 − 𝑦 ) − 𝑧 ) = ( 𝑥 − ( 𝑦 + 𝑧 ) ) )
78 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 − 𝑦 ) − 𝑧 ) = ( 𝑥 − ( 𝑦 + 𝑧 ) ) )
79 61 64 73 76 78 caofass ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = ( 𝐹 ∘f − ( ( 𝐻 ∘f · 𝐺 ) ∘f + ( 𝐺 ∘f · 𝑝 ) ) ) )
80 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
81 80 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
82 61 68 71 81 caofcom ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐻 ∘f · 𝐺 ) = ( 𝐺 ∘f · 𝐻 ) )
83 82 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐻 ∘f · 𝐺 ) ∘f + ( 𝐺 ∘f · 𝑝 ) ) = ( ( 𝐺 ∘f · 𝐻 ) ∘f + ( 𝐺 ∘f · 𝑝 ) ) )
84 adddi ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
85 84 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
86 61 71 68 75 85 caofdi ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) = ( ( 𝐺 ∘f · 𝐻 ) ∘f + ( 𝐺 ∘f · 𝑝 ) ) )
87 83 86 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐻 ∘f · 𝐺 ) ∘f + ( 𝐺 ∘f · 𝑝 ) ) = ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) )
88 87 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f − ( ( 𝐻 ∘f · 𝐺 ) ∘f + ( 𝐺 ∘f · 𝑝 ) ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) )
89 79 88 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) )
90 89 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ↔ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) = 0𝑝 ) )
91 89 fveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) = ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) )
92 91 breq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ↔ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) < 𝑁 ) )
93 90 92 orbi12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ↔ ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) < 𝑁 ) ) )
94 93 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ) → ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) < 𝑁 ) )
95 oveq2 ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → ( 𝐺 ∘f · 𝑞 ) = ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) )
96 95 oveq2d ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) )
97 8 96 eqtrid ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) )
98 97 eqeq1d ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → ( 𝑅 = 0𝑝 ↔ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) = 0𝑝 ) )
99 97 fveq2d ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → ( deg ‘ 𝑅 ) = ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) )
100 99 breq1d ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → ( ( deg ‘ 𝑅 ) < 𝑁 ↔ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) < 𝑁 ) )
101 98 100 orbi12d ⊢ ( 𝑞 = ( 𝐻 ∘f + 𝑝 ) → ( ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < 𝑁 ) ↔ ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) < 𝑁 ) ) )
102 101 rspcev ⊢ ( ( ( 𝐻 ∘f + 𝑝 ) ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐻 ∘f + 𝑝 ) ) ) ) < 𝑁 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < 𝑁 ) )
103 59 94 102 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < 𝑁 ) )
104 55 6 1 2 plymul ⊢ ( 𝜑 → ( 𝐻 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )
105 eqid ⊢ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) = ( deg ‘ ( 𝐻 ∘f · 𝐺 ) )
106 17 105 dgrsub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐻 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ≤ if ( 𝑀 ≤ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , 𝑀 ) )
107 5 104 106 syl2anc ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ≤ if ( 𝑀 ≤ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , 𝑀 ) )
108 17 15 dgreq0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑀 ) = 0 ) )
109 5 108 syl ⊢ ( 𝜑 → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑀 ) = 0 ) )
110 109 necon3bid ⊢ ( 𝜑 → ( 𝐹 ≠ 0𝑝 ↔ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) )
111 11 110 mpbid ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ≠ 0 )
112 28 35 111 39 divne0d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ≠ 0 )
113 20 53 sseldd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ∈ ℂ )
114 13 coe1term ⊢ ( ( ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ∈ ℂ ∧ 𝐷 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) → ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) = if ( 𝐷 = 𝐷 , ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) , 0 ) )
115 113 9 9 114 syl3anc ⊢ ( 𝜑 → ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) = if ( 𝐷 = 𝐷 , ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) , 0 ) )
116 eqid ⊢ 𝐷 = 𝐷
117 116 iftruei ⊢ if ( 𝐷 = 𝐷 , ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) , 0 ) = ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) )
118 115 117 eqtrdi ⊢ ( 𝜑 → ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) = ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) )
119 c0ex ⊢ 0 ∈ V
120 119 fvconst2 ⊢ ( 𝐷 ∈ ℕ0 → ( ( ℕ0 × { 0 } ) ‘ 𝐷 ) = 0 )
121 9 120 syl ⊢ ( 𝜑 → ( ( ℕ0 × { 0 } ) ‘ 𝐷 ) = 0 )
122 112 118 121 3netr4d ⊢ ( 𝜑 → ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) ≠ ( ( ℕ0 × { 0 } ) ‘ 𝐷 ) )
123 fveq2 ⊢ ( 𝐻 = 0𝑝 → ( coeff ‘ 𝐻 ) = ( coeff ‘ 0𝑝 ) )
124 coe0 ⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )
125 123 124 eqtrdi ⊢ ( 𝐻 = 0𝑝 → ( coeff ‘ 𝐻 ) = ( ℕ0 × { 0 } ) )
126 125 fveq1d ⊢ ( 𝐻 = 0𝑝 → ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) = ( ( ℕ0 × { 0 } ) ‘ 𝐷 ) )
127 126 necon3i ⊢ ( ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) ≠ ( ( ℕ0 × { 0 } ) ‘ 𝐷 ) → 𝐻 ≠ 0𝑝 )
128 122 127 syl ⊢ ( 𝜑 → 𝐻 ≠ 0𝑝 )
129 eqid ⊢ ( deg ‘ 𝐻 ) = ( deg ‘ 𝐻 )
130 129 18 dgrmul ⊢ ( ( ( 𝐻 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐻 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) = ( ( deg ‘ 𝐻 ) + 𝑁 ) )
131 55 128 6 7 130 syl22anc ⊢ ( 𝜑 → ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) = ( ( deg ‘ 𝐻 ) + 𝑁 ) )
132 13 dgr1term ⊢ ( ( ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ∈ ℂ ∧ ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) ≠ 0 ∧ 𝐷 ∈ ℕ0 ) → ( deg ‘ 𝐻 ) = 𝐷 )
133 113 112 9 132 syl3anc ⊢ ( 𝜑 → ( deg ‘ 𝐻 ) = 𝐷 )
134 133 10 eqtr4d ⊢ ( 𝜑 → ( deg ‘ 𝐻 ) = ( 𝑀 − 𝑁 ) )
135 134 oveq1d ⊢ ( 𝜑 → ( ( deg ‘ 𝐻 ) + 𝑁 ) = ( ( 𝑀 − 𝑁 ) + 𝑁 ) )
136 26 nn0cnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
137 33 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
138 136 137 npcand ⊢ ( 𝜑 → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
139 135 138 eqtrd ⊢ ( 𝜑 → ( ( deg ‘ 𝐻 ) + 𝑁 ) = 𝑀 )
140 131 139 eqtrd ⊢ ( 𝜑 → ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) = 𝑀 )
141 140 ifeq1d ⊢ ( 𝜑 → if ( 𝑀 ≤ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , 𝑀 ) = if ( 𝑀 ≤ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , 𝑀 , 𝑀 ) )
142 ifid ⊢ if ( 𝑀 ≤ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , 𝑀 , 𝑀 ) = 𝑀
143 141 142 eqtrdi ⊢ ( 𝜑 → if ( 𝑀 ≤ ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , ( deg ‘ ( 𝐻 ∘f · 𝐺 ) ) , 𝑀 ) = 𝑀 )
144 107 143 breqtrd ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ≤ 𝑀 )
145 eqid ⊢ ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) = ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) )
146 15 145 coesub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐻 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) = ( 𝐴 ∘f − ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ) )
147 5 104 146 syl2anc ⊢ ( 𝜑 → ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) = ( 𝐴 ∘f − ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ) )
148 147 fveq1d ⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = ( ( 𝐴 ∘f − ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) )
149 15 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
150 ffn ⊢ ( 𝐴 : ℕ0 ⟶ ℂ → 𝐴 Fn ℕ0 )
151 5 149 150 3syl ⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
152 145 coef3 ⊢ ( ( 𝐻 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) : ℕ0 ⟶ ℂ )
153 ffn ⊢ ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) : ℕ0 ⟶ ℂ → ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) Fn ℕ0 )
154 104 152 153 3syl ⊢ ( 𝜑 → ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) Fn ℕ0 )
155 nn0ex ⊢ ℕ0 ∈ V
156 155 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
157 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
158 eqidd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑀 ) = ( 𝐴 ‘ 𝑀 ) )
159 eqid ⊢ ( coeff ‘ 𝐻 ) = ( coeff ‘ 𝐻 )
160 159 16 129 18 coemulhi ⊢ ( ( 𝐻 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ‘ ( ( deg ‘ 𝐻 ) + 𝑁 ) ) = ( ( ( coeff ‘ 𝐻 ) ‘ ( deg ‘ 𝐻 ) ) · ( 𝐵 ‘ 𝑁 ) ) )
161 55 6 160 syl2anc ⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ‘ ( ( deg ‘ 𝐻 ) + 𝑁 ) ) = ( ( ( coeff ‘ 𝐻 ) ‘ ( deg ‘ 𝐻 ) ) · ( 𝐵 ‘ 𝑁 ) ) )
162 139 fveq2d ⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ‘ ( ( deg ‘ 𝐻 ) + 𝑁 ) ) = ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ‘ 𝑀 ) )
163 133 fveq2d ⊢ ( 𝜑 → ( ( coeff ‘ 𝐻 ) ‘ ( deg ‘ 𝐻 ) ) = ( ( coeff ‘ 𝐻 ) ‘ 𝐷 ) )
164 163 118 eqtrd ⊢ ( 𝜑 → ( ( coeff ‘ 𝐻 ) ‘ ( deg ‘ 𝐻 ) ) = ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) )
165 164 oveq1d ⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐻 ) ‘ ( deg ‘ 𝐻 ) ) · ( 𝐵 ‘ 𝑁 ) ) = ( ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) · ( 𝐵 ‘ 𝑁 ) ) )
166 28 35 39 divcan1d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝑀 ) / ( 𝐵 ‘ 𝑁 ) ) · ( 𝐵 ‘ 𝑁 ) ) = ( 𝐴 ‘ 𝑀 ) )
167 165 166 eqtrd ⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐻 ) ‘ ( deg ‘ 𝐻 ) ) · ( 𝐵 ‘ 𝑁 ) ) = ( 𝐴 ‘ 𝑀 ) )
168 161 162 167 3eqtr3d ⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ‘ 𝑀 ) = ( 𝐴 ‘ 𝑀 ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ‘ 𝑀 ) = ( 𝐴 ‘ 𝑀 ) )
170 151 154 156 156 157 158 169 ofval ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ∘f − ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = ( ( 𝐴 ‘ 𝑀 ) − ( 𝐴 ‘ 𝑀 ) ) )
171 26 170 mpdan ⊢ ( 𝜑 → ( ( 𝐴 ∘f − ( coeff ‘ ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = ( ( 𝐴 ‘ 𝑀 ) − ( 𝐴 ‘ 𝑀 ) ) )
172 28 subidd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) − ( 𝐴 ‘ 𝑀 ) ) = 0 )
173 148 171 172 3eqtrd ⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = 0 )
174 5 104 1 2 4 plysub ⊢ ( 𝜑 → ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∈ ( Poly ‘ 𝑆 ) )
175 dgrcl ⊢ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ∈ ℕ0 )
176 174 175 syl ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ∈ ℕ0 )
177 176 nn0red ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ∈ ℝ )
178 26 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
179 33 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
180 177 178 179 ltsub1d ⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) < 𝑀 ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < ( 𝑀 − 𝑁 ) ) )
181 10 breq2d ⊢ ( 𝜑 → ( ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < ( 𝑀 − 𝑁 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) )
182 180 181 bitrd ⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) < 𝑀 ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) )
183 182 orbi2d ⊢ ( 𝜑 → ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) < 𝑀 ) ↔ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) ) )
184 eqid ⊢ ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) = ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) )
185 eqid ⊢ ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) = ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) )
186 184 185 dgrlt ⊢ ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) < 𝑀 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ≤ 𝑀 ∧ ( ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = 0 ) ) )
187 174 26 186 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) < 𝑀 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ≤ 𝑀 ∧ ( ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = 0 ) ) )
188 183 187 bitr3d ⊢ ( 𝜑 → ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ≤ 𝑀 ∧ ( ( coeff ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) ‘ 𝑀 ) = 0 ) ) )
189 144 173 188 mpbir2and ⊢ ( 𝜑 → ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) )
190 eqeq1 ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( 𝑓 = 0𝑝 ↔ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ) )
191 fveq2 ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( deg ‘ 𝑓 ) = ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) )
192 191 oveq1d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ( deg ‘ 𝑓 ) − 𝑁 ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) )
193 192 breq1d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ( ( deg ‘ 𝑓 ) − 𝑁 ) < 𝐷 ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) )
194 190 193 orbi12d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − 𝑁 ) < 𝐷 ) ↔ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) ) )
195 oveq1 ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) )
196 12 195 eqtrid ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → 𝑈 = ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) )
197 196 eqeq1d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( 𝑈 = 0𝑝 ↔ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ) )
198 196 fveq2d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( deg ‘ 𝑈 ) = ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) )
199 198 breq1d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ( deg ‘ 𝑈 ) < 𝑁 ↔ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) )
200 197 199 orbi12d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ( 𝑈 = 0𝑝 ∨ ( deg ‘ 𝑈 ) < 𝑁 ) ↔ ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ) )
201 200 rexbidv ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( 𝑈 = 0𝑝 ∨ ( deg ‘ 𝑈 ) < 𝑁 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ) )
202 194 201 imbi12d ⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − 𝑁 ) < 𝐷 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( 𝑈 = 0𝑝 ∨ ( deg ‘ 𝑈 ) < 𝑁 ) ) ↔ ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ) ) )
203 202 14 174 rspcdva ⊢ ( 𝜑 → ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) = 0𝑝 ∨ ( ( deg ‘ ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ) − 𝑁 ) < 𝐷 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) ) )
204 189 203 mpd ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( ( 𝐹 ∘f − ( 𝐻 ∘f · 𝐺 ) ) ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < 𝑁 ) )
205 103 204 r19.29a ⊢ ( 𝜑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < 𝑁 ) )