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 23870

Description: Lemma for vieta1 23871: 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 10914	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2689	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 10942	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 2849	. . . 4 ⊢ (𝜑 → (#‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	syl5eqner 2857	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
12		dgr0 23822	. . . . . . . . . . 11 ⊢ (deg‘0_𝑝) = 0
13	11, 12	syl6eq 2660	. . . . . . . . . 10 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 2814	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0_𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (^◡𝐹 “ {0})
17	16	fta1 23867	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0_𝑝) → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 474	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 13015	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 2826	. . . 4 ⊢ (𝜑 → ((#‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 221	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 3890	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 207	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 3767	. . . . 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 23869	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 23793	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ₀)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ₀)
35	34	nn0red 11229	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2688	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 10833	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 10051	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4280	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → {𝑧} ⊆ (^◡𝑄 “ {0}))
40		ssequn1 3745	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (^◡𝑄 “ {0}) ↔ ({𝑧} ∪ (^◡𝑄 “ {0})) = (^◡𝑄 “ {0}))
41	39, 40	sylib 207	. . . . . . . . . 10 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → ({𝑧} ∪ (^◡𝑄 “ {0})) = (^◡𝑄 “ {0}))
42	41	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (#‘(^◡𝑄 “ {0})))
43	8	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 5404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (^◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3598	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 23758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 5964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	syl5sseq 3616	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2680	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (^◡𝐹 “ {0}))
52		ffn 5958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 6246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℂ → (𝑧 ∈ (^◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
54	8, 46, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
55	51, 54	syl5bb 271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
56	55	simplbda 652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0)
57		eqid 2610	. . . . . . . . . . . . . . . . . . 19 ⊢ (X_p ∘_𝑓 − (ℂ × {𝑧})) = (X_p ∘_𝑓 − (ℂ × {𝑧}))
58	57	facth 23865	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))))
60	29	oveq2i 6560	. . . . . . . . . . . . . . . . 17 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧}))))
61	59, 60	syl6eqr 2662	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))
62	61	cnveqd 5220	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ^◡𝐹 = ^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))
63	62	imaeq1d 5384	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡𝐹 “ {0}) = (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}))
64	16, 63	syl5eq 2656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}))
65		cnex 9896	. . . . . . . . . . . . . . 15 ⊢ ℂ ∈ V
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℂ ∈ V)
67	57	plyremlem 23863	. . . . . . . . . . . . . . . . 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 1066	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
70		plyf 23758	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
71	69, 70	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
72		plyf 23758	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
73	32, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
74		ofmulrt 23841	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}) = ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})))
75	66, 71, 73, 74	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}) = ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})))
76	68	simp3d 1068	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})
77	76	uneq1d 3728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})) = ({𝑧} ∪ (^◡𝑄 “ {0})))
78	64, 75, 77	3eqtrd 2648	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (^◡𝑄 “ {0})))
79	78	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘𝑅) = (#‘({𝑧} ∪ (^◡𝑄 “ {0}))))
80	1, 2	eqtr4d 2647	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝑅) = (𝐷 + 1))
81	80	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘𝑅) = (𝐷 + 1))
82	79, 81	eqtr3d 2646	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (𝐷 + 1))
83	15	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0_𝑝)
84	61, 83	eqnetrrd 2850	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) ≠ 0_𝑝)
85		plymul0or 23840	. . . . . . . . . . . . . . . . . . 19 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = 0_𝑝 ↔ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
86	69, 32, 85	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = 0_𝑝 ↔ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
87	86	necon3abid 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) ≠ 0_𝑝 ↔ ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
88	84, 87	mpbid 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝))
89		neanior 2874	. . . . . . . . . . . . . . . 16 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝 ∧ 𝑄 ≠ 0_𝑝) ↔ ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝))
90	88, 89	sylibr 223	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝 ∧ 𝑄 ≠ 0_𝑝))
91	90	simprd 478	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠ 0_𝑝)
92		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (^◡𝑄 “ {0}) = (^◡𝑄 “ {0})
93	92	fta1 23867	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0_𝑝) → ((^◡𝑄 “ {0}) ∈ Fin ∧ (#‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄)))
94	32, 91, 93	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡𝑄 “ {0}) ∈ Fin ∧ (#‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄)))
95	94	simprd 478	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄))
96	95, 31	breqtrrd 4611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ≤ 𝐷)
97		snfi 7923	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
98	94	simpld 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡𝑄 “ {0}) ∈ Fin)
99		hashun2 13033	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (^◡𝑄 “ {0}) ∈ Fin) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(^◡𝑄 “ {0}))))
100	97, 98, 99	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(^◡𝑄 “ {0}))))
101		ax-1cn 9873	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
102	3	nncnd 10913	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
103	102	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
104		addcom 10101	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
105	101, 103, 104	sylancr 694	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
106	82, 105	eqtr4d 2647	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (1 + 𝐷))
107		hashsng 13020	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (#‘{𝑧}) = 1)
108	107	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘{𝑧}) = 1)
109	108	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((#‘{𝑧}) + (#‘(^◡𝑄 “ {0}))) = (1 + (#‘(^◡𝑄 “ {0}))))
110	100, 106, 109	3brtr3d 4614	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (#‘(^◡𝑄 “ {0}))))
111		hashcl 13009	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑄 “ {0}) ∈ Fin → (#‘(^◡𝑄 “ {0})) ∈ ℕ₀)
112	98, 111	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ∈ ℕ₀)
113	112	nn0red 11229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ∈ ℝ)
114		1red 9934	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
115	36, 113, 114	leadd2d 10501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (#‘(^◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (#‘(^◡𝑄 “ {0})))))
116	110, 115	mpbird 246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (#‘(^◡𝑄 “ {0})))
117	113, 36	letri3d 10058	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((#‘(^◡𝑄 “ {0})) = 𝐷 ↔ ((#‘(^◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (#‘(^◡𝑄 “ {0})))))
118	96, 116, 117	mpbir2and 959	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) = 𝐷)
119	82, 118	eqeq12d 2625	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (#‘(^◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
120	42, 119	syl5ib 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (^◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
121	120	necon3ad 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (^◡𝑄 “ {0})))
122	38, 121	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (^◡𝑄 “ {0}))
123		disjsn 4192	. . . . . 6 ⊢ (((^◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (^◡𝑄 “ {0}))
124	122, 123	sylibr 223	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
125	26, 124	syl5eq 2656	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (^◡𝑄 “ {0})) = ∅)
126	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
127	49	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
128	127	sselda 3568	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
129	125, 78, 126, 128	fsumsplit 14318	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥))
130		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
131	130	sumsn 14319	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50, 50, 131	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
133	50	negnegd 10262	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
134	132, 133	eqtr4d 2647	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
135	118, 31	eqtrd 2644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) = (deg‘𝑄))
136	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
137		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
138	137	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
139		cnveq 5218	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑄 → ^◡𝑓 = ^◡𝑄)
140	139	imaeq1d 5384	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (^◡𝑓 “ {0}) = (^◡𝑄 “ {0}))
141	140	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (#‘(^◡𝑓 “ {0})) = (#‘(^◡𝑄 “ {0})))
142	141, 137	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → ((#‘(^◡𝑓 “ {0})) = (deg‘𝑓) ↔ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)))
143	138, 142	anbi12d 743	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄))))
144	140	sumeq1d 14279	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥)
145		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
146	137	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
147	145, 146	fveq12d 6109	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
148	145, 137	fveq12d 6109	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
149	147, 148	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
150	149	negeqd 10154	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
151	144, 150	eqeq12d 2625	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
152	143, 151	imbi12d 333	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
153	152	rspcv 3278	. . . . . . 7 ⊢ (𝑄 ∈ (Poly‘ℂ) → (∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ((𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
154	32, 136, 153	sylc 63	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
155	31, 135, 154	mp2and 711	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
156	31	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) = ((deg‘𝑄) − 1))
157	156	fveq2d 6107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
158	61	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
159	27, 158	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
160	61	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
161	68	simp2d 1067	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 1)
162		ax-1ne0 9884	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
163	162	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
164	161, 163	eqnetrd 2849	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ≠ 0)
165		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (deg‘0_𝑝))
166	165, 12	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 0)
167	166	necon3i 2814	. . . . . . . . . . . . 13 ⊢ ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ≠ 0 → (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝)
168	164, 167	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝)
169		eqid 2610	. . . . . . . . . . . . 13 ⊢ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))
170		eqid 2610	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
171	169, 170	dgrmul 23830	. . . . . . . . . . . 12 ⊢ ((((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0_𝑝)) → (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	69, 168, 32, 91, 171	syl22anc 1319	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
173	160, 172	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
174	9, 173	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
175	159, 174	fveq12d 6109	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))))
176		eqid 2610	. . . . . . . . . 10 ⊢ (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))
177		eqid 2610	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
178	176, 177, 169, 170	coemulhi 23814	. . . . . . . . 9 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
179	69, 32, 178	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
180	161	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1))
181		ssid 3587	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
182		plyid 23769	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → X_p ∈ (Poly‘ℂ))
183	181, 101, 182	mp2an 704	. . . . . . . . . . . . . 14 ⊢ X_p ∈ (Poly‘ℂ)
184		plyconst 23766	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
185	181, 50, 184	sylancr 694	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
186		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (coeff‘X_p) = (coeff‘X_p)
187		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
188	186, 187	coesub 23817	. . . . . . . . . . . . . 14 ⊢ ((X_p ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = ((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧}))))
189	183, 185, 188	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = ((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧}))))
190	189	fveq1d 6105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) = (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1))
191		1nn0 11185	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
192	186	coef3 23792	. . . . . . . . . . . . . . . . 17 ⊢ (X_p ∈ (Poly‘ℂ) → (coeff‘X_p):ℕ₀⟶ℂ)
193		ffn 5958	. . . . . . . . . . . . . . . . 17 ⊢ ((coeff‘X_p):ℕ₀⟶ℂ → (coeff‘X_p) Fn ℕ₀)
194	183, 192, 193	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ (coeff‘X_p) Fn ℕ₀
195	194	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘X_p) Fn ℕ₀)
196	187	coef3 23792	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ₀⟶ℂ)
197		ffn 5958	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ₀⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ₀)
198	185, 196, 197	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ₀)
199		nn0ex 11175	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
200	199	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ₀ ∈ V)
201		inidm 3784	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ ℕ₀) = ℕ₀
202		coeidp 23823	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ₀ → ((coeff‘X_p)‘1) = if(1 = 1, 1, 0))
203	202	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘X_p)‘1) = if(1 = 1, 1, 0))
204		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
205	204	iftruei 4043	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
206	203, 205	syl6eq 2660	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘X_p)‘1) = 1)
207		0lt1 10429	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
208		0re 9919	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
209		1re 9918	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
210	208, 209	ltnlei 10037	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
211	207, 210	mpbi 219	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
212	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → 𝑧 ∈ ℂ)
213		0dgr 23805	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
214	212, 213	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (deg‘(ℂ × {𝑧})) = 0)
215	214	breq2d 4595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
216	211, 215	mtbiri 316	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
217		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
218	187, 217	dgrub 23794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ₀ ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
219	218	3expia 1259	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ₀) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
220	185, 219	sylan 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
221	220	necon1bd 2800	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
222	216, 221	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
223	195, 198, 200, 200, 201, 206, 222	ofval 6804	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
224	191, 223	mpan2 703	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
225		1m0e1 11008	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
226	224, 225	syl6eq 2660	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = 1)
227	190, 226	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) = 1)
228	180, 227	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) = 1)
229	228	oveq1d 6564	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
230	177	coef3 23792	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ₀⟶ℂ)
231	32, 230	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ₀⟶ℂ)
232	231, 34	ffvelrnd 6268	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
233	232	mulid2d 9937	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
234	229, 233	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
235	175, 179, 234	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
236	157, 235	oveq12d 6567	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
237	236	negeqd 10154	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
238	155, 237	eqtr4d 2647	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
239	134, 238	oveq12d 6567	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
240	50	negcld 10258	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
241		nnm1nn0 11211	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ₀)
242	3, 241	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
243	242	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ₀)
244	231, 243	ffvelrnd 6268	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
245	235, 232	eqeltrd 2688	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
246	9, 27	dgreq0 23825	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
247	43, 246	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
248	247	necon3bid 2826	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0_𝑝 ↔ (𝐴‘𝑁) ≠ 0))
249	83, 248	mpbid 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
250	244, 245, 249	divcld 10680	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
251	240, 250	negdid 10284	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
252	240, 245	mulcld 9939	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
253	252, 244, 245, 249	divdird 10718	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
254		nnm1nn0 11211	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
255	5, 254	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
256	255	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ₀)
257	176, 177	coemul 23812	. . . . . . . . 9 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
258	69, 32, 256, 257	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
259	159	fveq1d 6105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)))
260		1e0p1 11428	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
261	260	oveq2i 6560	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
262	261	sumeq1i 14276	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
263		0nn0 11184	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
264		nn0uz 11598	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
265	263, 264	eleqtri 2686	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ_≥‘0)
266	265	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ_≥‘0))
267	261	eleq2i 2680	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
268	176	coef3 23792	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ)
269	69, 268	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ)
270		elfznn0 12302	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ₀)
271		ffvelrn 6265	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
272	269, 270, 271	syl2an 493	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
273	2	oveq1d 6564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
274		pncan 10166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
275	102, 101, 274	sylancl 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
276	273, 275	eqtr3d 2646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
277	276	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
278	3	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
279	277, 278	eqeltrd 2688	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
280		nnuz 11599	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
281	279, 280	syl6eleq 2698	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ_≥‘1))
282		fzss2 12252	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
283	281, 282	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
284	283	sselda 3568	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
285		fznn0sub 12244	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ₀)
286		ffvelrn 6265	. . . . . . . . . . . . . . 15 ⊢ (((coeff‘𝑄):ℕ₀⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ₀) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
287	231, 285, 286	syl2an 493	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
288	284, 287	syldan 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
289	272, 288	mulcld 9939	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
290	267, 289	sylan2br 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
291		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
292	291, 260	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
293	292	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1))
294	292	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
295	294	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
296	293, 295	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
297	266, 290, 296	fsump1 14329	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
298	262, 297	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
299		eldifn 3695	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
300	299	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
301		eldifi 3694	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
302		elfznn0 12302	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
303	301, 302	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ₀)
304	176, 169	dgrub 23794	. . . . . . . . . . . . . . . . 17 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ₀ ∧ ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))))
305	304	3expia 1259	. . . . . . . . . . . . . . . 16 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ₀) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
306	69, 303, 305	syl2an 493	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
307		elfzuz 12209	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ_≥‘0))
308	301, 307	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ_≥‘0))
309	308	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ_≥‘0))
310		1z 11284	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
311		elfz5 12205	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
312	309, 310, 311	sylancl 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
313	161	breq2d 4595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
314	313	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
315	312, 314	bitr4d 270	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
316	306, 315	sylibrd 248	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
317	316	necon1bd 2800	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = 0))
318	300, 317	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = 0)
319	318	oveq1d 6564	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
320	301, 287	sylan2 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
321	320	mul02d 10113	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
322	319, 321	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
323		fzfid 12634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
324	283, 289, 322, 323	fsumss 14303	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
325		0z 11265	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
326	189	fveq1d 6105	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) = (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0))
327		coeidp 23823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ₀ → ((coeff‘X_p)‘0) = if(0 = 1, 1, 0))
328	162	nesymi 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
329	328	iffalsei 4046	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
330	327, 329	syl6eq 2660	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ₀ → ((coeff‘X_p)‘0) = 0)
331	330	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → ((coeff‘X_p)‘0) = 0)
332		0cn 9911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
333		vex 3176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
334	333	fvconst2 6374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
335	332, 334	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
336	187	coefv0 23808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
337	185, 336	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
338	335, 337	syl5reqr 2659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
339	338	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
340	195, 198, 200, 200, 201, 331, 339	ofval 6804	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
341	263, 340	mpan2 703	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
342		df-neg 10148	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
343	341, 342	syl6eqr 2662	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
344	326, 343	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) = -𝑧)
345	277	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
346	103	subid1d 10260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
347	345, 346, 31	3eqtrd 2648	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
348	347	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
349	348, 235	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
350	344, 349	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
351	350, 252	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
352		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0))
353		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
354	353	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
355	352, 354	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
356	355	fsum1 14320	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
357	325, 351, 356	sylancr 694	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
358	357, 350	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
359	277	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 1) = (𝐷 − 1))
360	359	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
361	227, 360	oveq12d 6567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
362	244	mulid2d 9937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
363	361, 362	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
364	358, 363	oveq12d 6567	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
365	298, 324, 364	3eqtr3rd 2653	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
366	258, 259, 365	3eqtr4rd 2655	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
367	366	oveq1d 6564	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	240, 245, 249	divcan4d 10686	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
369	368	oveq1d 6564	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
370	253, 367, 369	3eqtr3rd 2653	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
371	370	negeqd 10154	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
372	251, 371	eqtr3d 2646	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
373	129, 239, 372	3eqtrd 2648	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
374	25, 373	exlimddv 1850	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 ifcif 4036 {csn 4125 class class class wbr 4583 × cxp 5036 ^◡ccnv 5037 dom cdm 5038 “ cima 5041 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ∘_𝑓 cof 6793 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 #chash 12979 Σcsu 14264 0_𝑝c0p 23242 Polycply 23744 X_pcidp 23745 coeffccoe 23746 degcdgr 23747 quot cquot 23849

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-rlim 14068 df-sum 14265 df-0p 23243 df-ply 23748 df-idp 23749 df-coe 23750 df-dgr 23751 df-quot 23850

This theorem is referenced by: vieta1 23871

W3C validator