plydivlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > plydivlem4		Structured version Visualization version GIF version

Theorem plydivlem4 25800

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

**Hypotheses**
Ref	Expression
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	⊢ (𝜑 → 𝐷 ∈ ℕ₀)
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**
Ref	Expression
plydivlem4	⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0_𝑝 ∨ (deg‘𝑅) < 𝑁))

Distinct variable groups: 𝑥,𝑦,𝑧,𝐴 𝑓,𝑝,𝑞,𝑥,𝑦,𝑧,𝐹 𝑓,𝐻,𝑝,𝑞,𝑥,𝑦,𝑧 𝜑,𝑥,𝑦,𝑧 𝑥,𝐵,𝑦,𝑧 𝐷,𝑓,𝑧 𝑥,𝑀,𝑦,𝑧 𝑓,𝑁,𝑝,𝑞,𝑥,𝑦,𝑧 𝑓,𝐺,𝑝,𝑞,𝑥,𝑦,𝑧 𝑅,𝑓,𝑝,𝑥,𝑦 𝑆,𝑓,𝑝,𝑞,𝑥,𝑦,𝑧 𝜑,𝑝 Allowed substitution hints: 𝜑(𝑓,𝑞) 𝐴(𝑓,𝑞,𝑝) 𝐵(𝑓,𝑞,𝑝) 𝐷(𝑥,𝑦,𝑞,𝑝) 𝑅(𝑧,𝑞) 𝑈(𝑥,𝑦,𝑧,𝑓,𝑞,𝑝) 𝑀(𝑓,𝑞,𝑝)

**Proof of Theorem plydivlem4**
Step	Hyp	Ref	Expression
1		plydiv.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
2		plybss 25699	. . . . . . 7 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
4		plydiv.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
5		plydiv.tm	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)
6		plydiv.rc	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)
7		plydiv.m1	. . . . . . . . . . . 12 ⊢ (𝜑 → -1 ∈ 𝑆)
8	4, 5, 6, 7	plydivlem1 25797	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ 𝑆)
9		plydiv.a	. . . . . . . . . . . 12 ⊢ 𝐴 = (coeff‘𝐹)
10	9	coef2 25736	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ₀⟶𝑆)
11	1, 8, 10	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:ℕ₀⟶𝑆)
12		plydiv.m	. . . . . . . . . . 11 ⊢ 𝑀 = (deg‘𝐹)
13		dgrcl 25738	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ₀)
14	1, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (deg‘𝐹) ∈ ℕ₀)
15	12, 14	eqeltrid 2837	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
16	11, 15	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘𝑀) ∈ 𝑆)
17	3, 16	sseldd 3982	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ)
18		plydiv.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
19		plydiv.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (coeff‘𝐺)
20	19	coef2 25736	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐵:ℕ₀⟶𝑆)
21	18, 8, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵:ℕ₀⟶𝑆)
22		plydiv.n	. . . . . . . . . . 11 ⊢ 𝑁 = (deg‘𝐺)
23		dgrcl 25738	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈ ℕ₀)
24	18, 23	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (deg‘𝐺) ∈ ℕ₀)
25	22, 24	eqeltrid 2837	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
26	21, 25	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (𝐵‘𝑁) ∈ 𝑆)
27	3, 26	sseldd 3982	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝑁) ∈ ℂ)
28		plydiv.z	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ≠ 0_𝑝)
29	22, 19	dgreq0 25770	. . . . . . . . . . 11 ⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0_𝑝 ↔ (𝐵‘𝑁) = 0))
30	18, 29	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 = 0_𝑝 ↔ (𝐵‘𝑁) = 0))
31	30	necon3bid 2985	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 ≠ 0_𝑝 ↔ (𝐵‘𝑁) ≠ 0))
32	28, 31	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝑁) ≠ 0)
33	17, 27, 32	divrecd 11989	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) = ((𝐴‘𝑀) · (1 / (𝐵‘𝑁))))
34		fvex 6901	. . . . . . . . . . 11 ⊢ (𝐵‘𝑁) ∈ V
35		eleq1 2821	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐵‘𝑁) → (𝑥 ∈ 𝑆 ↔ (𝐵‘𝑁) ∈ 𝑆))
36		neeq1 3003	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐵‘𝑁) → (𝑥 ≠ 0 ↔ (𝐵‘𝑁) ≠ 0))
37	35, 36	anbi12d 631	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵‘𝑁) → ((𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0) ↔ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0)))
38	37	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵‘𝑁) → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) ↔ (𝜑 ∧ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0))))
39		oveq2 7413	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵‘𝑁) → (1 / 𝑥) = (1 / (𝐵‘𝑁)))
40	39	eleq1d 2818	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵‘𝑁) → ((1 / 𝑥) ∈ 𝑆 ↔ (1 / (𝐵‘𝑁)) ∈ 𝑆))
41	38, 40	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵‘𝑁) → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) ↔ ((𝜑 ∧ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0)) → (1 / (𝐵‘𝑁)) ∈ 𝑆)))
42	34, 41, 6	vtocl 3549	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0)) → (1 / (𝐵‘𝑁)) ∈ 𝑆)
43	42	ex 413	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0) → (1 / (𝐵‘𝑁)) ∈ 𝑆))
44	26, 32, 43	mp2and 697	. . . . . . . 8 ⊢ (𝜑 → (1 / (𝐵‘𝑁)) ∈ 𝑆)
45	5, 16, 44	caovcld 7596	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘𝑀) · (1 / (𝐵‘𝑁))) ∈ 𝑆)
46	33, 45	eqeltrd 2833	. . . . . 6 ⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ 𝑆)
47		plydiv.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
48		plydiv.h	. . . . . . 7 ⊢ 𝐻 = (𝑧 ∈ ℂ ↦ (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝑧↑𝐷)))
49	48	ply1term 25709	. . . . . 6 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ 𝑆 ∧ 𝐷 ∈ ℕ₀) → 𝐻 ∈ (Poly‘𝑆))
50	3, 46, 47, 49	syl3anc 1371	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (Poly‘𝑆))
51	50	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐻 ∈ (Poly‘𝑆))
52		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝑝 ∈ (Poly‘𝑆))
53	4	adantlr 713	. . . 4 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
54	51, 52, 53	plyadd 25722	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐻 ∘_f + 𝑝) ∈ (Poly‘𝑆))
55		cnex 11187	. . . . . . . . 9 ⊢ ℂ ∈ V
56	55	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ℂ ∈ V)
57	1	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐹 ∈ (Poly‘𝑆))
58		plyf 25703	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
59	57, 58	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ)
60		mulcl 11190	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
61	60	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
62		plyf 25703	. . . . . . . . . 10 ⊢ (𝐻 ∈ (Poly‘𝑆) → 𝐻:ℂ⟶ℂ)
63	51, 62	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐻:ℂ⟶ℂ)
64	18	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐺 ∈ (Poly‘𝑆))
65		plyf 25703	. . . . . . . . . 10 ⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ)
66	64, 65	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐺:ℂ⟶ℂ)
67		inidm 4217	. . . . . . . . 9 ⊢ (ℂ ∩ ℂ) = ℂ
68	61, 63, 66, 56, 56, 67	off 7684	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐻 ∘_f · 𝐺):ℂ⟶ℂ)
69		plyf 25703	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Poly‘𝑆) → 𝑝:ℂ⟶ℂ)
70	69	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝑝:ℂ⟶ℂ)
71	61, 66, 70, 56, 56, 67	off 7684	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐺 ∘_f · 𝑝):ℂ⟶ℂ)
72		subsub4 11489	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 − 𝑦) − 𝑧) = (𝑥 − (𝑦 + 𝑧)))
73	72	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 − 𝑦) − 𝑧) = (𝑥 − (𝑦 + 𝑧)))
74	56, 59, 68, 71, 73	caofass 7703	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = (𝐹 ∘_f − ((𝐻 ∘_f · 𝐺) ∘_f + (𝐺 ∘_f · 𝑝))))
75		mulcom 11192	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
76	75	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
77	56, 63, 66, 76	caofcom 7701	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐻 ∘_f · 𝐺) = (𝐺 ∘_f · 𝐻))
78	77	oveq1d 7420	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐻 ∘_f · 𝐺) ∘_f + (𝐺 ∘_f · 𝑝)) = ((𝐺 ∘_f · 𝐻) ∘_f + (𝐺 ∘_f · 𝑝)))
79		adddi 11195	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
80	79	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
81	56, 66, 63, 70, 80	caofdi 7705	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)) = ((𝐺 ∘_f · 𝐻) ∘_f + (𝐺 ∘_f · 𝑝)))
82	78, 81	eqtr4d 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐻 ∘_f · 𝐺) ∘_f + (𝐺 ∘_f · 𝑝)) = (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))
83	82	oveq2d 7421	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐹 ∘_f − ((𝐻 ∘_f · 𝐺) ∘_f + (𝐺 ∘_f · 𝑝))) = (𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))))
84	74, 83	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = (𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))))
85	84	eqeq1d 2734	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ↔ (𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))) = 0_𝑝))
86	84	fveq2d 6892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) = (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))))
87	86	breq1d 5157	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁 ↔ (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))) < 𝑁))
88	85, 87	orbi12d 917	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁) ↔ ((𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))) < 𝑁)))
89	88	biimpa 477	. . 3 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁)) → ((𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))) < 𝑁))
90		plydiv.r	. . . . . . 7 ⊢ 𝑅 = (𝐹 ∘_f − (𝐺 ∘_f · 𝑞))
91		oveq2 7413	. . . . . . . 8 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → (𝐺 ∘_f · 𝑞) = (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))
92	91	oveq2d 7421	. . . . . . 7 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → (𝐹 ∘_f − (𝐺 ∘_f · 𝑞)) = (𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))))
93	90, 92	eqtrid 2784	. . . . . 6 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → 𝑅 = (𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))))
94	93	eqeq1d 2734	. . . . 5 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → (𝑅 = 0_𝑝 ↔ (𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))) = 0_𝑝))
95	93	fveq2d 6892	. . . . . 6 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → (deg‘𝑅) = (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))))
96	95	breq1d 5157	. . . . 5 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → ((deg‘𝑅) < 𝑁 ↔ (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))) < 𝑁))
97	94, 96	orbi12d 917	. . . 4 ⊢ (𝑞 = (𝐻 ∘_f + 𝑝) → ((𝑅 = 0_𝑝 ∨ (deg‘𝑅) < 𝑁) ↔ ((𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))) < 𝑁)))
98	97	rspcev 3612	. . 3 ⊢ (((𝐻 ∘_f + 𝑝) ∈ (Poly‘𝑆) ∧ ((𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝))) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐺 ∘_f · (𝐻 ∘_f + 𝑝)))) < 𝑁)) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0_𝑝 ∨ (deg‘𝑅) < 𝑁))
99	54, 89, 98	syl2an2r 683	. 2 ⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁)) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0_𝑝 ∨ (deg‘𝑅) < 𝑁))
100	50, 18, 4, 5	plymul 25723	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘_f · 𝐺) ∈ (Poly‘𝑆))
101		eqid 2732	. . . . . . 7 ⊢ (deg‘(𝐻 ∘_f · 𝐺)) = (deg‘(𝐻 ∘_f · 𝐺))
102	12, 101	dgrsub 25777	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐻 ∘_f · 𝐺) ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ≤ if(𝑀 ≤ (deg‘(𝐻 ∘_f · 𝐺)), (deg‘(𝐻 ∘_f · 𝐺)), 𝑀))
103	1, 100, 102	syl2anc 584	. . . . 5 ⊢ (𝜑 → (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ≤ if(𝑀 ≤ (deg‘(𝐻 ∘_f · 𝐺)), (deg‘(𝐻 ∘_f · 𝐺)), 𝑀))
104		plydiv.fz	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
105	12, 9	dgreq0 25770	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑀) = 0))
106	1, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑀) = 0))
107	106	necon3bid 2985	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ≠ 0_𝑝 ↔ (𝐴‘𝑀) ≠ 0))
108	104, 107	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑀) ≠ 0)
109	17, 27, 108, 32	divne0d 12002	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) ≠ 0)
110	3, 46	sseldd 3982	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ ℂ)
111	48	coe1term 25764	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ ℂ ∧ 𝐷 ∈ ℕ₀ ∧ 𝐷 ∈ ℕ₀) → ((coeff‘𝐻)‘𝐷) = if(𝐷 = 𝐷, ((𝐴‘𝑀) / (𝐵‘𝑁)), 0))
112	110, 47, 47, 111	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coeff‘𝐻)‘𝐷) = if(𝐷 = 𝐷, ((𝐴‘𝑀) / (𝐵‘𝑁)), 0))
113		eqid 2732	. . . . . . . . . . . . 13 ⊢ 𝐷 = 𝐷
114	113	iftruei 4534	. . . . . . . . . . . 12 ⊢ if(𝐷 = 𝐷, ((𝐴‘𝑀) / (𝐵‘𝑁)), 0) = ((𝐴‘𝑀) / (𝐵‘𝑁))
115	112, 114	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (𝜑 → ((coeff‘𝐻)‘𝐷) = ((𝐴‘𝑀) / (𝐵‘𝑁)))
116		c0ex 11204	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
117	116	fvconst2 7201	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ ℕ₀ → ((ℕ₀ × {0})‘𝐷) = 0)
118	47, 117	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℕ₀ × {0})‘𝐷) = 0)
119	109, 115, 118	3netr4d 3018	. . . . . . . . . 10 ⊢ (𝜑 → ((coeff‘𝐻)‘𝐷) ≠ ((ℕ₀ × {0})‘𝐷))
120		fveq2 6888	. . . . . . . . . . . . 13 ⊢ (𝐻 = 0_𝑝 → (coeff‘𝐻) = (coeff‘0_𝑝))
121		coe0 25761	. . . . . . . . . . . . 13 ⊢ (coeff‘0_𝑝) = (ℕ₀ × {0})
122	120, 121	eqtrdi 2788	. . . . . . . . . . . 12 ⊢ (𝐻 = 0_𝑝 → (coeff‘𝐻) = (ℕ₀ × {0}))
123	122	fveq1d 6890	. . . . . . . . . . 11 ⊢ (𝐻 = 0_𝑝 → ((coeff‘𝐻)‘𝐷) = ((ℕ₀ × {0})‘𝐷))
124	123	necon3i 2973	. . . . . . . . . 10 ⊢ (((coeff‘𝐻)‘𝐷) ≠ ((ℕ₀ × {0})‘𝐷) → 𝐻 ≠ 0_𝑝)
125	119, 124	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ≠ 0_𝑝)
126		eqid 2732	. . . . . . . . . 10 ⊢ (deg‘𝐻) = (deg‘𝐻)
127	126, 22	dgrmul 25775	. . . . . . . . 9 ⊢ (((𝐻 ∈ (Poly‘𝑆) ∧ 𝐻 ≠ 0_𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0_𝑝)) → (deg‘(𝐻 ∘_f · 𝐺)) = ((deg‘𝐻) + 𝑁))
128	50, 125, 18, 28, 127	syl22anc 837	. . . . . . . 8 ⊢ (𝜑 → (deg‘(𝐻 ∘_f · 𝐺)) = ((deg‘𝐻) + 𝑁))
129	48	dgr1term 25765	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ ℂ ∧ ((𝐴‘𝑀) / (𝐵‘𝑁)) ≠ 0 ∧ 𝐷 ∈ ℕ₀) → (deg‘𝐻) = 𝐷)
130	110, 109, 47, 129	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → (deg‘𝐻) = 𝐷)
131		plydiv.e	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − 𝑁) = 𝐷)
132	130, 131	eqtr4d 2775	. . . . . . . . . 10 ⊢ (𝜑 → (deg‘𝐻) = (𝑀 − 𝑁))
133	132	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → ((deg‘𝐻) + 𝑁) = ((𝑀 − 𝑁) + 𝑁))
134	15	nn0cnd 12530	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
135	25	nn0cnd 12530	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℂ)
136	134, 135	npcand 11571	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 − 𝑁) + 𝑁) = 𝑀)
137	133, 136	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → ((deg‘𝐻) + 𝑁) = 𝑀)
138	128, 137	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (deg‘(𝐻 ∘_f · 𝐺)) = 𝑀)
139	138	ifeq1d 4546	. . . . . 6 ⊢ (𝜑 → if(𝑀 ≤ (deg‘(𝐻 ∘_f · 𝐺)), (deg‘(𝐻 ∘_f · 𝐺)), 𝑀) = if(𝑀 ≤ (deg‘(𝐻 ∘_f · 𝐺)), 𝑀, 𝑀))
140		ifid 4567	. . . . . 6 ⊢ if(𝑀 ≤ (deg‘(𝐻 ∘_f · 𝐺)), 𝑀, 𝑀) = 𝑀
141	139, 140	eqtrdi 2788	. . . . 5 ⊢ (𝜑 → if(𝑀 ≤ (deg‘(𝐻 ∘_f · 𝐺)), (deg‘(𝐻 ∘_f · 𝐺)), 𝑀) = 𝑀)
142	103, 141	breqtrd 5173	. . . 4 ⊢ (𝜑 → (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ≤ 𝑀)
143		eqid 2732	. . . . . . . 8 ⊢ (coeff‘(𝐻 ∘_f · 𝐺)) = (coeff‘(𝐻 ∘_f · 𝐺))
144	9, 143	coesub 25762	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐻 ∘_f · 𝐺) ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) = (𝐴 ∘_f − (coeff‘(𝐻 ∘_f · 𝐺))))
145	1, 100, 144	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) = (𝐴 ∘_f − (coeff‘(𝐻 ∘_f · 𝐺))))
146	145	fveq1d 6890	. . . . 5 ⊢ (𝜑 → ((coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))‘𝑀) = ((𝐴 ∘_f − (coeff‘(𝐻 ∘_f · 𝐺)))‘𝑀))
147	9	coef3 25737	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ₀⟶ℂ)
148		ffn 6714	. . . . . . . 8 ⊢ (𝐴:ℕ₀⟶ℂ → 𝐴 Fn ℕ₀)
149	1, 147, 148	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐴 Fn ℕ₀)
150	143	coef3 25737	. . . . . . . 8 ⊢ ((𝐻 ∘_f · 𝐺) ∈ (Poly‘𝑆) → (coeff‘(𝐻 ∘_f · 𝐺)):ℕ₀⟶ℂ)
151		ffn 6714	. . . . . . . 8 ⊢ ((coeff‘(𝐻 ∘_f · 𝐺)):ℕ₀⟶ℂ → (coeff‘(𝐻 ∘_f · 𝐺)) Fn ℕ₀)
152	100, 150, 151	3syl 18	. . . . . . 7 ⊢ (𝜑 → (coeff‘(𝐻 ∘_f · 𝐺)) Fn ℕ₀)
153		nn0ex 12474	. . . . . . . 8 ⊢ ℕ₀ ∈ V
154	153	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ₀ ∈ V)
155		inidm 4217	. . . . . . 7 ⊢ (ℕ₀ ∩ ℕ₀) = ℕ₀
156		eqidd 2733	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ₀) → (𝐴‘𝑀) = (𝐴‘𝑀))
157		eqid 2732	. . . . . . . . . . 11 ⊢ (coeff‘𝐻) = (coeff‘𝐻)
158	157, 19, 126, 22	coemulhi 25759	. . . . . . . . . 10 ⊢ ((𝐻 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐻 ∘_f · 𝐺))‘((deg‘𝐻) + 𝑁)) = (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁)))
159	50, 18, 158	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((coeff‘(𝐻 ∘_f · 𝐺))‘((deg‘𝐻) + 𝑁)) = (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁)))
160	137	fveq2d 6892	. . . . . . . . 9 ⊢ (𝜑 → ((coeff‘(𝐻 ∘_f · 𝐺))‘((deg‘𝐻) + 𝑁)) = ((coeff‘(𝐻 ∘_f · 𝐺))‘𝑀))
161	130	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coeff‘𝐻)‘(deg‘𝐻)) = ((coeff‘𝐻)‘𝐷))
162	161, 115	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → ((coeff‘𝐻)‘(deg‘𝐻)) = ((𝐴‘𝑀) / (𝐵‘𝑁)))
163	162	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝜑 → (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁)) = (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝐵‘𝑁)))
164	17, 27, 32	divcan1d 11987	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝐵‘𝑁)) = (𝐴‘𝑀))
165	163, 164	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁)) = (𝐴‘𝑀))
166	159, 160, 165	3eqtr3d 2780	. . . . . . . 8 ⊢ (𝜑 → ((coeff‘(𝐻 ∘_f · 𝐺))‘𝑀) = (𝐴‘𝑀))
167	166	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ₀) → ((coeff‘(𝐻 ∘_f · 𝐺))‘𝑀) = (𝐴‘𝑀))
168	149, 152, 154, 154, 155, 156, 167	ofval 7677	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ₀) → ((𝐴 ∘_f − (coeff‘(𝐻 ∘_f · 𝐺)))‘𝑀) = ((𝐴‘𝑀) − (𝐴‘𝑀)))
169	15, 168	mpdan 685	. . . . 5 ⊢ (𝜑 → ((𝐴 ∘_f − (coeff‘(𝐻 ∘_f · 𝐺)))‘𝑀) = ((𝐴‘𝑀) − (𝐴‘𝑀)))
170	17	subidd 11555	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝑀) − (𝐴‘𝑀)) = 0)
171	146, 169, 170	3eqtrd 2776	. . . 4 ⊢ (𝜑 → ((coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))‘𝑀) = 0)
172	1, 100, 4, 5, 7	plysub 25724	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∈ (Poly‘𝑆))
173		dgrcl 25738	. . . . . . . . . 10 ⊢ ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∈ (Poly‘𝑆) → (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ∈ ℕ₀)
174	172, 173	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ∈ ℕ₀)
175	174	nn0red 12529	. . . . . . . 8 ⊢ (𝜑 → (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ∈ ℝ)
176	15	nn0red 12529	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
177	25	nn0red 12529	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℝ)
178	175, 176, 177	ltsub1d 11819	. . . . . . 7 ⊢ (𝜑 → ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) < 𝑀 ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < (𝑀 − 𝑁)))
179	131	breq2d 5159	. . . . . . 7 ⊢ (𝜑 → (((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < (𝑀 − 𝑁) ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷))
180	178, 179	bitrd 278	. . . . . 6 ⊢ (𝜑 → ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) < 𝑀 ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷))
181	180	orbi2d 914	. . . . 5 ⊢ (𝜑 → (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) < 𝑀) ↔ ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷)))
182		eqid 2732	. . . . . . 7 ⊢ (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) = (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))
183		eqid 2732	. . . . . . 7 ⊢ (coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) = (coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))
184	182, 183	dgrlt 25771	. . . . . 6 ⊢ (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ₀) → (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) < 𝑀) ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))‘𝑀) = 0)))
185	172, 15, 184	syl2anc 584	. . . . 5 ⊢ (𝜑 → (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) < 𝑀) ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))‘𝑀) = 0)))
186	181, 185	bitr3d 280	. . . 4 ⊢ (𝜑 → (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷) ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺)))‘𝑀) = 0)))
187	142, 171, 186	mpbir2and 711	. . 3 ⊢ (𝜑 → ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷))
188		eqeq1 2736	. . . . . 6 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (𝑓 = 0_𝑝 ↔ (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝))
189		fveq2 6888	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (deg‘𝑓) = (deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))))
190	189	oveq1d 7420	. . . . . . 7 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → ((deg‘𝑓) − 𝑁) = ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁))
191	190	breq1d 5157	. . . . . 6 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (((deg‘𝑓) − 𝑁) < 𝐷 ↔ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷))
192	188, 191	orbi12d 917	. . . . 5 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → ((𝑓 = 0_𝑝 ∨ ((deg‘𝑓) − 𝑁) < 𝐷) ↔ ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷)))
193		plydiv.u	. . . . . . . . 9 ⊢ 𝑈 = (𝑓 ∘_f − (𝐺 ∘_f · 𝑝))
194		oveq1 7412	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (𝑓 ∘_f − (𝐺 ∘_f · 𝑝)) = ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)))
195	193, 194	eqtrid 2784	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → 𝑈 = ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)))
196	195	eqeq1d 2734	. . . . . . 7 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (𝑈 = 0_𝑝 ↔ ((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝))
197	195	fveq2d 6892	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (deg‘𝑈) = (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))))
198	197	breq1d 5157	. . . . . . 7 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → ((deg‘𝑈) < 𝑁 ↔ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁))
199	196, 198	orbi12d 917	. . . . . 6 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → ((𝑈 = 0_𝑝 ∨ (deg‘𝑈) < 𝑁) ↔ (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁)))
200	199	rexbidv 3178	. . . . 5 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0_𝑝 ∨ (deg‘𝑈) < 𝑁) ↔ ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁)))
201	192, 200	imbi12d 344	. . . 4 ⊢ (𝑓 = (𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) → (((𝑓 = 0_𝑝 ∨ ((deg‘𝑓) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0_𝑝 ∨ (deg‘𝑈) < 𝑁)) ↔ (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁))))
202		plydiv.al	. . . 4 ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0_𝑝 ∨ ((deg‘𝑓) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0_𝑝 ∨ (deg‘𝑈) < 𝑁)))
203	201, 202, 172	rspcdva 3613	. . 3 ⊢ (𝜑 → (((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) = 0_𝑝 ∨ ((deg‘(𝐹 ∘_f − (𝐻 ∘_f · 𝐺))) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁)))
204	187, 203	mpd 15	. 2 ⊢ (𝜑 → ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝)) = 0_𝑝 ∨ (deg‘((𝐹 ∘_f − (𝐻 ∘_f · 𝐺)) ∘_f − (𝐺 ∘_f · 𝑝))) < 𝑁))
205	99, 204	r19.29a 3162	1 ⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0_𝑝 ∨ (deg‘𝑅) < 𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ⊆ wss 3947 ifcif 4527 {csn 4627 class class class wbr 5147 ↦ cmpt 5230 × cxp 5673 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ∘_f cof 7664 ℂcc 11104 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 < clt 11244 ≤ cle 11245 − cmin 11440 -cneg 11441 / cdiv 11867 ℕ₀cn0 12468 ↑cexp 14023 0_𝑝c0p 25177 Polycply 25689 coeffccoe 25691 degcdgr 25692

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7666 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-map 8818 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-oi 9501 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-z 12555 df-uz 12819 df-rp 12971 df-fz 13481 df-fzo 13624 df-fl 13753 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-rlim 15429 df-sum 15629 df-0p 25178 df-ply 25693 df-coe 25695 df-dgr 25696

This theorem is referenced by: plydivex 25801

W3C validator