vieta1lem2 - Metamath Proof Explorer

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

Theorem vieta1lem2 24503

Description: Lemma for vieta1 24504: inductive step. Let 𝑧 be a root of 𝐹. Then 𝐹 = (X_p − 𝑧) · 𝑄 for some 𝑄 by the factor theorem, and 𝑄 is a degree- 𝐷 polynomial, so by the induction hypothesis Σ𝑥 ∈ (^◡𝑄 “ 0)𝑥 = -(coeff‘𝑄)‘(𝐷 − 1) / (coeff‘𝑄)‘𝐷, so Σ𝑥 ∈ 𝑅𝑥 = 𝑧 − (coeff‘𝑄)‘ (𝐷 − 1) / (coeff‘𝑄)‘𝐷. Now the coefficients of 𝐹 are 𝐴‘(𝐷 + 1) = (coeff‘𝑄)‘𝐷 and 𝐴‘𝐷 = Σ𝑘 ∈ (0...𝐷)(coeff‘X_p − 𝑧)‘𝑘 · (coeff‘𝑄) ‘(𝐷 − 𝑘), which works out to -𝑧 · (coeff‘𝑄)‘𝐷 + (coeff‘𝑄)‘(𝐷 − 1), so putting it all together we have Σ𝑥 ∈ 𝑅𝑥 = -𝐴‘𝐷 / 𝐴‘(𝐷 + 1) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.)

**Hypotheses**
Ref	Expression
vieta1.1	⊢ 𝐴 = (coeff‘𝐹)
vieta1.2	⊢ 𝑁 = (deg‘𝐹)
vieta1.3	⊢ 𝑅 = (^◡𝐹 “ {0})
vieta1.4	⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
vieta1.5	⊢ (𝜑 → (♯‘𝑅) = 𝑁)
vieta1lem.6	⊢ (𝜑 → 𝐷 ∈ ℕ)
vieta1lem.7	⊢ (𝜑 → (𝐷 + 1) = 𝑁)
vieta1lem.8	⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
vieta1lem.9	⊢ 𝑄 = (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))

**Assertion**
Ref	Expression
vieta1lem2	⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Distinct variable groups: 𝐷,𝑓 𝑓,𝐹 𝑧,𝑓,𝑁 𝑥,𝑓,𝑄 𝑅,𝑓 𝑥,𝑧,𝑅 𝐴,𝑓,𝑧 𝜑,𝑥,𝑧 Allowed substitution hints: 𝜑(𝑓) 𝐴(𝑥) 𝐷(𝑥,𝑧) 𝑄(𝑧) 𝑆(𝑥,𝑧,𝑓) 𝐹(𝑥,𝑧) 𝑁(𝑥)

Proof of Theorem vieta1lem2 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vieta1.5	. . . . 5 ⊢ (𝜑 → (♯‘𝑅) = 𝑁)
2		vieta1lem.7	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) = 𝑁)
3		vieta1lem.6	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
4	3	peano2nnd 11393	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2859	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 11425	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 3035	. . . 4 ⊢ (𝜑 → (♯‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	syl5eqner 3043	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6446	. . . . . . . . . . 11 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
12		dgr0 24455	. . . . . . . . . . 11 ⊢ (deg‘0_𝑝) = 0
13	11, 12	syl6eq 2829	. . . . . . . . . 10 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 3000	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0_𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (^◡𝐹 “ {0})
17	16	fta1 24500	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0_𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 490	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 13469	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 3012	. . . 4 ⊢ (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 224	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 4158	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 210	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 4027	. . . . 5 ⊢ ({𝑧} ∩ (^◡𝑄 “ {0})) = ((^◡𝑄 “ {0}) ∩ {𝑧})
27		vieta1.1	. . . . . . . . . . 11 ⊢ 𝐴 = (coeff‘𝐹)
28		vieta1lem.8	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
29		vieta1lem.9	. . . . . . . . . . 11 ⊢ 𝑄 = (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))
30	27, 9, 16, 8, 1, 3, 2, 28, 29	vieta1lem1 24502	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 491	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 24426	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ₀)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ₀)
35	34	nn0red 11703	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2858	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 11308	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 10511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4570	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → {𝑧} ⊆ (^◡𝑄 “ {0}))
40		ssequn1 4005	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (^◡𝑄 “ {0}) ↔ ({𝑧} ∪ (^◡𝑄 “ {0})) = (^◡𝑄 “ {0}))
41	39, 40	sylib 210	. . . . . . . . . 10 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → ({𝑧} ∪ (^◡𝑄 “ {0})) = (^◡𝑄 “ {0}))
42	41	fveq2d 6450	. . . . . . . . 9 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → (♯‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (♯‘(^◡𝑄 “ {0})))
43	8	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 5739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (^◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3853	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 24391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	syl5sseq 3871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3820	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (^◡𝐹 “ {0}))
52		ffn 6291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 6602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℂ → (𝑧 ∈ (^◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
54	8, 46, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
55	51, 54	syl5bb 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
56	55	simplbda 495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0)
57		eqid 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ (X_p ∘_𝑓 − (ℂ × {𝑧})) = (X_p ∘_𝑓 − (ℂ × {𝑧}))
58	57	facth 24498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1439	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))))
60	29	oveq2i 6933	. . . . . . . . . . . . . . . . 17 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧}))))
61	59, 60	syl6eqr 2831	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))
62	61	cnveqd 5543	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ^◡𝐹 = ^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))
63	62	imaeq1d 5719	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡𝐹 “ {0}) = (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}))
64	16, 63	syl5eq 2825	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}))
65		cnex 10353	. . . . . . . . . . . . . . 15 ⊢ ℂ ∈ V
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℂ ∈ V)
67	57	plyremlem 24496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℂ → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 1 ∧ (^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
68	50, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 1 ∧ (^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
69	68	simp1d 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
70		plyf 24391	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
71	69, 70	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
72		plyf 24391	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
73	32, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
74		ofmulrt 24474	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}) = ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})))
75	66, 71, 73, 74	syl3anc 1439	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}) = ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})))
76	68	simp3d 1135	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})
77	76	uneq1d 3988	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})) = ({𝑧} ∪ (^◡𝑄 “ {0})))
78	64, 75, 77	3eqtrd 2817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (^◡𝑄 “ {0})))
79	78	fveq2d 6450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (^◡𝑄 “ {0}))))
80	1, 2	eqtr4d 2816	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑅) = (𝐷 + 1))
81	80	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (𝐷 + 1))
82	79, 81	eqtr3d 2815	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (𝐷 + 1))
83	15	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0_𝑝)
84	61, 83	eqnetrrd 3036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) ≠ 0_𝑝)
85		plymul0or 24473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = 0_𝑝 ↔ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
86	69, 32, 85	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = 0_𝑝 ↔ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
87	86	necon3abid 3004	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) ≠ 0_𝑝 ↔ ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
88	84, 87	mpbid 224	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝))
89		neanior 3061	. . . . . . . . . . . . . . . 16 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝 ∧ 𝑄 ≠ 0_𝑝) ↔ ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝))
90	88, 89	sylibr 226	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝 ∧ 𝑄 ≠ 0_𝑝))
91	90	simprd 491	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠ 0_𝑝)
92		eqid 2777	. . . . . . . . . . . . . . 15 ⊢ (^◡𝑄 “ {0}) = (^◡𝑄 “ {0})
93	92	fta1 24500	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0_𝑝) → ((^◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄)))
94	32, 91, 93	syl2anc 579	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄)))
95	94	simprd 491	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄))
96	95, 31	breqtrrd 4914	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(^◡𝑄 “ {0})) ≤ 𝐷)
97		snfi 8326	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
98	94	simpld 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡𝑄 “ {0}) ∈ Fin)
99		hashun2 13487	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (^◡𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (^◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(^◡𝑄 “ {0}))))
100	97, 98, 99	sylancr 581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (^◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(^◡𝑄 “ {0}))))
101		ax-1cn 10330	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
102	3	nncnd 11392	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
103	102	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
104		addcom 10562	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
105	101, 103, 104	sylancr 581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
106	82, 105	eqtr4d 2816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (1 + 𝐷))
107		hashsng 13474	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (♯‘{𝑧}) = 1)
108	107	adantl 475	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘{𝑧}) = 1)
109	108	oveq1d 6937	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘{𝑧}) + (♯‘(^◡𝑄 “ {0}))) = (1 + (♯‘(^◡𝑄 “ {0}))))
110	100, 106, 109	3brtr3d 4917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(^◡𝑄 “ {0}))))
111		hashcl 13462	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑄 “ {0}) ∈ Fin → (♯‘(^◡𝑄 “ {0})) ∈ ℕ₀)
112	98, 111	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(^◡𝑄 “ {0})) ∈ ℕ₀)
113	112	nn0red 11703	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(^◡𝑄 “ {0})) ∈ ℝ)
114		1red 10377	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
115	36, 113, 114	leadd2d 10970	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (♯‘(^◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(^◡𝑄 “ {0})))))
116	110, 115	mpbird 249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (♯‘(^◡𝑄 “ {0})))
117	113, 36	letri3d 10518	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘(^◡𝑄 “ {0})) = 𝐷 ↔ ((♯‘(^◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (♯‘(^◡𝑄 “ {0})))))
118	96, 116, 117	mpbir2and 703	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(^◡𝑄 “ {0})) = 𝐷)
119	82, 118	eqeq12d 2792	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (♯‘(^◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
120	42, 119	syl5ib 236	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (^◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
121	120	necon3ad 2981	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (^◡𝑄 “ {0})))
122	38, 121	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (^◡𝑄 “ {0}))
123		disjsn 4477	. . . . . 6 ⊢ (((^◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (^◡𝑄 “ {0}))
124	122, 123	sylibr 226	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
125	26, 124	syl5eq 2825	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (^◡𝑄 “ {0})) = ∅)
126	19	adantr 474	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
127	49	adantr 474	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
128	127	sselda 3820	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
129	125, 78, 126, 128	fsumsplit 14878	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥))
130		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
131	130	sumsn 14882	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50, 50, 131	syl2anc 579	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
133	50	negnegd 10725	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
134	132, 133	eqtr4d 2816	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
135	118, 31	eqtrd 2813	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(^◡𝑄 “ {0})) = (deg‘𝑄))
136		fveq2 6446	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
137	136	eqeq2d 2787	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
138		cnveq 5541	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ^◡𝑓 = ^◡𝑄)
139	138	imaeq1d 5719	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (^◡𝑓 “ {0}) = (^◡𝑄 “ {0}))
140	139	fveq2d 6450	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (♯‘(^◡𝑓 “ {0})) = (♯‘(^◡𝑄 “ {0})))
141	140, 136	eqeq12d 2792	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((♯‘(^◡𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(^◡𝑄 “ {0})) = (deg‘𝑄)))
142	137, 141	anbi12d 624	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(^◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(^◡𝑄 “ {0})) = (deg‘𝑄))))
143	139	sumeq1d 14839	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥)
144		fveq2 6446	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
145	136	oveq1d 6937	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
146	144, 145	fveq12d 6453	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
147	144, 136	fveq12d 6453	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
148	146, 147	oveq12d 6940	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149	148	negeqd 10616	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
150	143, 149	eqeq12d 2792	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → (Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
151	142, 150	imbi12d 336	. . . . . . 7 ⊢ (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (♯‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (♯‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
152	28	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
153	151, 152, 32	rspcdva 3516	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
154	31, 135, 153	mp2and 689	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
155	31	fvoveq1d 6944	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
156	61	fveq2d 6450	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
157	27, 156	syl5eq 2825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
158	61	fveq2d 6450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
159	68	simp2d 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 1)
160		ax-1ne0 10341	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
161	160	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
162	159, 161	eqnetrd 3035	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ≠ 0)
163		fveq2 6446	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (deg‘0_𝑝))
164	163, 12	syl6eq 2829	. . . . . . . . . . . . . 14 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 0)
165	164	necon3i 3000	. . . . . . . . . . . . 13 ⊢ ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ≠ 0 → (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝)
166	162, 165	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝)
167		eqid 2777	. . . . . . . . . . . . 13 ⊢ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))
168		eqid 2777	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
169	167, 168	dgrmul 24463	. . . . . . . . . . . 12 ⊢ ((((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0_𝑝)) → (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
170	69, 166, 32, 91, 169	syl22anc 829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
171	158, 170	eqtrd 2813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	9, 171	syl5eq 2825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
173	157, 172	fveq12d 6453	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))))
174		eqid 2777	. . . . . . . . . 10 ⊢ (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))
175		eqid 2777	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
176	174, 175, 167, 168	coemulhi 24447	. . . . . . . . 9 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
177	69, 32, 176	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
178	159	fveq2d 6450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1))
179		ssid 3841	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
180		plyid 24402	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → X_p ∈ (Poly‘ℂ))
181	179, 101, 180	mp2an 682	. . . . . . . . . . . . . 14 ⊢ X_p ∈ (Poly‘ℂ)
182		plyconst 24399	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183	179, 50, 182	sylancr 581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
184		eqid 2777	. . . . . . . . . . . . . . 15 ⊢ (coeff‘X_p) = (coeff‘X_p)
185		eqid 2777	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
186	184, 185	coesub 24450	. . . . . . . . . . . . . 14 ⊢ ((X_p ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = ((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧}))))
187	181, 183, 186	sylancr 581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = ((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧}))))
188	187	fveq1d 6448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) = (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1))
189		1nn0 11660	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
190	184	coef3 24425	. . . . . . . . . . . . . . . . 17 ⊢ (X_p ∈ (Poly‘ℂ) → (coeff‘X_p):ℕ₀⟶ℂ)
191		ffn 6291	. . . . . . . . . . . . . . . . 17 ⊢ ((coeff‘X_p):ℕ₀⟶ℂ → (coeff‘X_p) Fn ℕ₀)
192	181, 190, 191	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ (coeff‘X_p) Fn ℕ₀
193	192	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘X_p) Fn ℕ₀)
194	185	coef3 24425	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ₀⟶ℂ)
195		ffn 6291	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ₀⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ₀)
196	183, 194, 195	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ₀)
197		nn0ex 11649	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
198	197	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ₀ ∈ V)
199		inidm 4042	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ ℕ₀) = ℕ₀
200		coeidp 24456	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ₀ → ((coeff‘X_p)‘1) = if(1 = 1, 1, 0))
201	200	adantl 475	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘X_p)‘1) = if(1 = 1, 1, 0))
202		eqid 2777	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
203	202	iftruei 4313	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
204	201, 203	syl6eq 2829	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘X_p)‘1) = 1)
205		0lt1 10897	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
206		0re 10378	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
207		1re 10376	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
208	206, 207	ltnlei 10497	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
209	205, 208	mpbi 222	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
210	50	adantr 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → 𝑧 ∈ ℂ)
211		0dgr 24438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (deg‘(ℂ × {𝑧})) = 0)
213	212	breq2d 4898	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
214	209, 213	mtbiri 319	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
215		eqid 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
216	185, 215	dgrub 24427	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ₀ ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
217	216	3expia 1111	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ₀) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
218	183, 217	sylan 575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
219	218	necon1bd 2986	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
220	214, 219	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
221	193, 196, 198, 198, 199, 204, 220	ofval 7183	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222	189, 221	mpan2 681	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
223		1m0e1 11503	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
224	222, 223	syl6eq 2829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = 1)
225	188, 224	eqtrd 2813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) = 1)
226	178, 225	eqtrd 2813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) = 1)
227	226	oveq1d 6937	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
228	175	coef3 24425	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ₀⟶ℂ)
229	32, 228	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ₀⟶ℂ)
230	229, 34	ffvelrnd 6624	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
231	230	mulid2d 10395	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232	227, 231	eqtrd 2813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
233	173, 177, 232	3eqtrd 2817	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
234	155, 233	oveq12d 6940	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235	234	negeqd 10616	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
236	154, 235	eqtr4d 2816	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
237	134, 236	oveq12d 6940	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
238	50	negcld 10721	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
239		nnm1nn0 11685	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ₀)
240	3, 239	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
241	240	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ₀)
242	229, 241	ffvelrnd 6624	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
243	233, 230	eqeltrd 2858	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
244	9, 27	dgreq0 24458	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
245	43, 244	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
246	245	necon3bid 3012	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0_𝑝 ↔ (𝐴‘𝑁) ≠ 0))
247	83, 246	mpbid 224	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
248	242, 243, 247	divcld 11151	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
249	238, 248	negdid 10747	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
250	238, 243	mulcld 10397	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
251	250, 242, 243, 247	divdird 11189	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
252		nnm1nn0 11685	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
253	5, 252	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
254	253	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ₀)
255	174, 175	coemul 24445	. . . . . . . . 9 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256	69, 32, 254, 255	syl3anc 1439	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
257	157	fveq1d 6448	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)))
258		1e0p1 11888	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
259	258	oveq2i 6933	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
260	259	sumeq1i 14836	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
261		0nn0 11659	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
262		nn0uz 12028	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
263	261, 262	eleqtri 2856	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ_≥‘0)
264	263	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ_≥‘0))
265	259	eleq2i 2850	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
266	174	coef3 24425	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ)
267	69, 266	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ)
268		elfznn0 12751	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ₀)
269		ffvelrn 6621	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
270	267, 268, 269	syl2an 589	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
271	2	oveq1d 6937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
272		pncan 10628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
273	102, 101, 272	sylancl 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
274	271, 273	eqtr3d 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
275	274	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
276	3	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
277	275, 276	eqeltrd 2858	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
278		nnuz 12029	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
279	277, 278	syl6eleq 2868	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ_≥‘1))
280		fzss2 12698	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
281	279, 280	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
282	281	sselda 3820	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
283		fznn0sub 12690	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ₀)
284		ffvelrn 6621	. . . . . . . . . . . . . . 15 ⊢ (((coeff‘𝑄):ℕ₀⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ₀) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
285	229, 283, 284	syl2an 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
286	282, 285	syldan 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
287	270, 286	mulcld 10397	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
288	265, 287	sylan2br 588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
289		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
290	289, 258	syl6eqr 2831	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
291	290	fveq2d 6450	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1))
292	290	oveq2d 6938	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
293	292	fveq2d 6450	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
294	291, 293	oveq12d 6940	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
295	264, 288, 294	fsump1 14892	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296	260, 295	syl5eq 2825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
297		eldifn 3955	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
298	297	adantl 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
299		eldifi 3954	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
300		elfznn0 12751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
301	299, 300	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ₀)
302	174, 167	dgrub 24427	. . . . . . . . . . . . . . . . 17 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ₀ ∧ ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))))
303	302	3expia 1111	. . . . . . . . . . . . . . . 16 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ₀) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
304	69, 301, 303	syl2an 589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
305		elfzuz 12655	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ_≥‘0))
306	299, 305	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ_≥‘0))
307	306	adantl 475	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ_≥‘0))
308		1z 11759	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
309		elfz5 12651	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310	307, 308, 309	sylancl 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
311	159	breq2d 4898	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
312	311	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
313	310, 312	bitr4d 274	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
314	304, 313	sylibrd 251	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
315	314	necon1bd 2986	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = 0))
316	298, 315	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = 0)
317	316	oveq1d 6937	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
318	299, 285	sylan2 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
319	318	mul02d 10574	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320	317, 319	eqtrd 2813	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
321		fzfid 13091	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
322	281, 287, 320, 321	fsumss 14863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
323		0z 11739	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
324	187	fveq1d 6448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) = (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0))
325		coeidp 24456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ₀ → ((coeff‘X_p)‘0) = if(0 = 1, 1, 0))
326	160	nesymi 3025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
327	326	iffalsei 4316	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
328	325, 327	syl6eq 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ₀ → ((coeff‘X_p)‘0) = 0)
329	328	adantl 475	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → ((coeff‘X_p)‘0) = 0)
330		0cn 10368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
331		vex 3400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
332	331	fvconst2 6741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
333	330, 332	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
334	185	coefv0 24441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
335	183, 334	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
336	333, 335	syl5reqr 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337	336	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
338	193, 196, 198, 198, 199, 329, 337	ofval 7183	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339	261, 338	mpan2 681	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
340		df-neg 10609	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
341	339, 340	syl6eqr 2831	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
342	324, 341	eqtrd 2813	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) = -𝑧)
343	275	oveq1d 6937	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
344	103	subid1d 10723	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
345	343, 344, 31	3eqtrd 2817	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
346	345	fveq2d 6450	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
347	346, 233	eqtr4d 2816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
348	342, 347	oveq12d 6940	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
349	348, 250	eqeltrd 2858	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
350		fveq2 6446	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0))
351		oveq2 6930	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
352	351	fveq2d 6450	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
353	350, 352	oveq12d 6940	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
354	353	fsum1 14883	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
355	323, 349, 354	sylancr 581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
356	355, 348	eqtrd 2813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
357	275	fvoveq1d 6944	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
358	225, 357	oveq12d 6940	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
359	242	mulid2d 10395	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360	358, 359	eqtrd 2813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
361	356, 360	oveq12d 6940	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
362	296, 322, 361	3eqtr3rd 2822	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
363	256, 257, 362	3eqtr4rd 2824	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
364	363	oveq1d 6937	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
365	238, 243, 247	divcan4d 11157	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
366	365	oveq1d 6937	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
367	251, 364, 366	3eqtr3rd 2822	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	367	negeqd 10616	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
369	249, 368	eqtr3d 2815	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
370	129, 237, 369	3eqtrd 2817	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
371	25, 370	exlimddv 1978	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 836 ∧ w3a 1071 = wceq 1601 ∃wex 1823 ∈ wcel 2106 ≠ wne 2968 ∀wral 3089 Vcvv 3397 ∖ cdif 3788 ∪ cun 3789 ∩ cin 3790 ⊆ wss 3791 ∅c0 4140 ifcif 4306 {csn 4397 class class class wbr 4886 × cxp 5353 ^◡ccnv 5354 dom cdm 5355 “ cima 5358 Fn wfn 6130 ⟶wf 6131 ‘cfv 6135 (class class class)co 6922 ∘_𝑓 cof 7172 Fincfn 8241 ℂcc 10270 ℝcr 10271 0cc0 10272 1c1 10273 + caddc 10275 · cmul 10277 < clt 10411 ≤ cle 10412 − cmin 10606 -cneg 10607 / cdiv 11032 ℕcn 11374 ℕ₀cn0 11642 ℤcz 11728 ℤ_≥cuz 11992 ...cfz 12643 ♯chash 13435 Σcsu 14824 0_𝑝c0p 23873 Polycply 24377 X_pcidp 24378 coeffccoe 24379 degcdgr 24380 quot cquot 24482

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-8 2108 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-rep 5006 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-inf2 8835 ax-cnex 10328 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-addrcl 10333 ax-mulcl 10334 ax-mulrcl 10335 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-i2m1 10340 ax-1ne0 10341 ax-1rid 10342 ax-rnegex 10343 ax-rrecex 10344 ax-cnre 10345 ax-pre-lttri 10346 ax-pre-lttrn 10347 ax-pre-ltadd 10348 ax-pre-mulgt0 10349 ax-pre-sup 10350 ax-addf 10351

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-fal 1615 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2550 df-eu 2586 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3399 df-sbc 3652 df-csb 3751 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-pss 3807 df-nul 4141 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-tp 4402 df-op 4404 df-uni 4672 df-int 4711 df-iun 4755 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-se 5315 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-isom 6144 df-riota 6883 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-of 7174 df-om 7344 df-1st 7445 df-2nd 7446 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-1o 7843 df-oadd 7847 df-er 8026 df-map 8142 df-pm 8143 df-en 8242 df-dom 8243 df-sdom 8244 df-fin 8245 df-sup 8636 df-inf 8637 df-oi 8704 df-card 9098 df-cda 9325 df-pnf 10413 df-mnf 10414 df-xr 10415 df-ltxr 10416 df-le 10417 df-sub 10608 df-neg 10609 df-div 11033 df-nn 11375 df-2 11438 df-3 11439 df-n0 11643 df-xnn0 11715 df-z 11729 df-uz 11993 df-rp 12138 df-fz 12644 df-fzo 12785 df-fl 12912 df-seq 13120 df-exp 13179 df-hash 13436 df-cj 14246 df-re 14247 df-im 14248 df-sqrt 14382 df-abs 14383 df-clim 14627 df-rlim 14628 df-sum 14825 df-0p 23874 df-ply 24381 df-idp 24382 df-coe 24383 df-dgr 24384 df-quot 24483

This theorem is referenced by: vieta1 24504

W3C validator