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 24066

Description: Lemma for vieta1 24067: 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 11037	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2702	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 11065	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 2861	. . . 4 ⊢ (𝜑 → (#‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	syl5eqner 2869	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
12		dgr0 24018	. . . . . . . . . . 11 ⊢ (deg‘0_𝑝) = 0
13	11, 12	syl6eq 2672	. . . . . . . . . 10 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 2826	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0_𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (^◡𝐹 “ {0})
17	16	fta1 24063	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0_𝑝) → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 475	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 13154	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 2838	. . . 4 ⊢ (𝜑 → ((#‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 222	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 3931	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 208	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 3805	. . . . 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 24065	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 475	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 23989	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ₀)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ₀)
35	34	nn0red 11352	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2701	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 10954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 10172	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4339	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → {𝑧} ⊆ (^◡𝑄 “ {0}))
40		ssequn1 3783	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (^◡𝑄 “ {0}) ↔ ({𝑧} ∪ (^◡𝑄 “ {0})) = (^◡𝑄 “ {0}))
41	39, 40	sylib 208	. . . . . . . . . 10 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → ({𝑧} ∪ (^◡𝑄 “ {0})) = (^◡𝑄 “ {0}))
42	41	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑧 ∈ (^◡𝑄 “ {0}) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (#‘(^◡𝑄 “ {0})))
43	8	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 5485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (^◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3635	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 23954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	syl5sseq 3653	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3603	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (^◡𝐹 “ {0}))
52		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℂ → (𝑧 ∈ (^◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
54	8, 46, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
55	51, 54	syl5bb 272	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
56	55	simplbda 654	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0)
57		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (X_p ∘_𝑓 − (ℂ × {𝑧})) = (X_p ∘_𝑓 − (ℂ × {𝑧}))
58	57	facth 24061	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧})))))
60	29	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · (𝐹 quot (X_p ∘_𝑓 − (ℂ × {𝑧}))))
61	59, 60	syl6eqr 2674	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))
62	61	cnveqd 5298	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ^◡𝐹 = ^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))
63	62	imaeq1d 5465	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡𝐹 “ {0}) = (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}))
64	16, 63	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}))
65		cnex 10017	. . . . . . . . . . . . . . 15 ⊢ ℂ ∈ V
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℂ ∈ V)
67	57	plyremlem 24059	. . . . . . . . . . . . . . . . 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 1073	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
70		plyf 23954	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
71	69, 70	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
72		plyf 23954	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
73	32, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
74		ofmulrt 24037	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (X_p ∘_𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}) = ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})))
75	66, 71, 73, 74	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) “ {0}) = ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})))
76	68	simp3d 1075	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})
77	76	uneq1d 3766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡(X_p ∘_𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (^◡𝑄 “ {0})) = ({𝑧} ∪ (^◡𝑄 “ {0})))
78	64, 75, 77	3eqtrd 2660	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (^◡𝑄 “ {0})))
79	78	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘𝑅) = (#‘({𝑧} ∪ (^◡𝑄 “ {0}))))
80	1, 2	eqtr4d 2659	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝑅) = (𝐷 + 1))
81	80	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘𝑅) = (𝐷 + 1))
82	79, 81	eqtr3d 2658	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (𝐷 + 1))
83	15	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0_𝑝)
84	61, 83	eqnetrrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) ≠ 0_𝑝)
85		plymul0or 24036	. . . . . . . . . . . . . . . . . . 19 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = 0_𝑝 ↔ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
86	69, 32, 85	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) = 0_𝑝 ↔ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
87	86	necon3abid 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄) ≠ 0_𝑝 ↔ ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝)))
88	84, 87	mpbid 222	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝))
89		neanior 2886	. . . . . . . . . . . . . . . 16 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝 ∧ 𝑄 ≠ 0_𝑝) ↔ ¬ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 ∨ 𝑄 = 0_𝑝))
90	88, 89	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝 ∧ 𝑄 ≠ 0_𝑝))
91	90	simprd 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠ 0_𝑝)
92		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (^◡𝑄 “ {0}) = (^◡𝑄 “ {0})
93	92	fta1 24063	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0_𝑝) → ((^◡𝑄 “ {0}) ∈ Fin ∧ (#‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄)))
94	32, 91, 93	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡𝑄 “ {0}) ∈ Fin ∧ (#‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄)))
95	94	simprd 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ≤ (deg‘𝑄))
96	95, 31	breqtrrd 4681	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ≤ 𝐷)
97		snfi 8038	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
98	94	simpld 475	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (^◡𝑄 “ {0}) ∈ Fin)
99		hashun2 13172	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (^◡𝑄 “ {0}) ∈ Fin) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(^◡𝑄 “ {0}))))
100	97, 98, 99	sylancr 695	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(^◡𝑄 “ {0}))))
101		ax-1cn 9994	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
102	3	nncnd 11036	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
103	102	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
104		addcom 10222	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
105	101, 103, 104	sylancr 695	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
106	82, 105	eqtr4d 2659	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (1 + 𝐷))
107		hashsng 13159	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (#‘{𝑧}) = 1)
108	107	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘{𝑧}) = 1)
109	108	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((#‘{𝑧}) + (#‘(^◡𝑄 “ {0}))) = (1 + (#‘(^◡𝑄 “ {0}))))
110	100, 106, 109	3brtr3d 4684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (#‘(^◡𝑄 “ {0}))))
111		hashcl 13147	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑄 “ {0}) ∈ Fin → (#‘(^◡𝑄 “ {0})) ∈ ℕ₀)
112	98, 111	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ∈ ℕ₀)
113	112	nn0red 11352	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) ∈ ℝ)
114		1red 10055	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
115	36, 113, 114	leadd2d 10622	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (#‘(^◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (#‘(^◡𝑄 “ {0})))))
116	110, 115	mpbird 247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (#‘(^◡𝑄 “ {0})))
117	113, 36	letri3d 10179	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((#‘(^◡𝑄 “ {0})) = 𝐷 ↔ ((#‘(^◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (#‘(^◡𝑄 “ {0})))))
118	96, 116, 117	mpbir2and 957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) = 𝐷)
119	82, 118	eqeq12d 2637	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((#‘({𝑧} ∪ (^◡𝑄 “ {0}))) = (#‘(^◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
120	42, 119	syl5ib 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (^◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
121	120	necon3ad 2807	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (^◡𝑄 “ {0})))
122	38, 121	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (^◡𝑄 “ {0}))
123		disjsn 4246	. . . . . 6 ⊢ (((^◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (^◡𝑄 “ {0}))
124	122, 123	sylibr 224	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((^◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
125	26, 124	syl5eq 2668	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (^◡𝑄 “ {0})) = ∅)
126	19	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
127	49	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
128	127	sselda 3603	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
129	125, 78, 126, 128	fsumsplit 14471	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥))
130		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
131	130	sumsn 14475	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50, 50, 131	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
133	50	negnegd 10383	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
134	132, 133	eqtr4d 2659	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
135	118, 31	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (#‘(^◡𝑄 “ {0})) = (deg‘𝑄))
136	28	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
137		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
138	137	eqeq2d 2632	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
139		cnveq 5296	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑄 → ^◡𝑓 = ^◡𝑄)
140	139	imaeq1d 5465	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (^◡𝑓 “ {0}) = (^◡𝑄 “ {0}))
141	140	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (#‘(^◡𝑓 “ {0})) = (#‘(^◡𝑄 “ {0})))
142	141, 137	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → ((#‘(^◡𝑓 “ {0})) = (deg‘𝑓) ↔ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)))
143	138, 142	anbi12d 747	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄))))
144	140	sumeq1d 14431	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥)
145		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
146	137	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
147	145, 146	fveq12d 6197	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
148	145, 137	fveq12d 6197	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
149	147, 148	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
150	149	negeqd 10275	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
151	144, 150	eqeq12d 2637	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
152	143, 151	imbi12d 334	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (#‘(^◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (^◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
153	152	rspcv 3305	. . . . . . 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 65	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 = (deg‘𝑄) ∧ (#‘(^◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
155	31, 135, 154	mp2and 715	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
156	31	oveq1d 6665	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) = ((deg‘𝑄) − 1))
157	156	fveq2d 6195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
158	61	fveq2d 6195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
159	27, 158	syl5eq 2668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
160	61	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)))
161	68	simp2d 1074	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 1)
162		ax-1ne0 10005	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
163	162	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
164	161, 163	eqnetrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ≠ 0)
165		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (deg‘0_𝑝))
166	165, 12	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) = 0_𝑝 → (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = 0)
167	166	necon3i 2826	. . . . . . . . . . . . 13 ⊢ ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ≠ 0 → (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝)
168	164, 167	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝)
169		eqid 2622	. . . . . . . . . . . . 13 ⊢ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))
170		eqid 2622	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
171	169, 170	dgrmul 24026	. . . . . . . . . . . 12 ⊢ ((((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (X_p ∘_𝑓 − (ℂ × {𝑧})) ≠ 0_𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0_𝑝)) → (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	69, 168, 32, 91, 171	syl22anc 1327	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄)) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
173	160, 172	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
174	9, 173	syl5eq 2668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
175	159, 174	fveq12d 6197	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))))
176		eqid 2622	. . . . . . . . . 10 ⊢ (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))
177		eqid 2622	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
178	176, 177, 169, 170	coemulhi 24010	. . . . . . . . 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 693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘((deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
180	161	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1))
181		ssid 3624	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
182		plyid 23965	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → X_p ∈ (Poly‘ℂ))
183	181, 101, 182	mp2an 708	. . . . . . . . . . . . . 14 ⊢ X_p ∈ (Poly‘ℂ)
184		plyconst 23962	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
185	181, 50, 184	sylancr 695	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
186		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (coeff‘X_p) = (coeff‘X_p)
187		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
188	186, 187	coesub 24013	. . . . . . . . . . . . . 14 ⊢ ((X_p ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = ((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧}))))
189	183, 185, 188	sylancr 695	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) = ((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧}))))
190	189	fveq1d 6193	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) = (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1))
191		1nn0 11308	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
192	186	coef3 23988	. . . . . . . . . . . . . . . . 17 ⊢ (X_p ∈ (Poly‘ℂ) → (coeff‘X_p):ℕ₀⟶ℂ)
193		ffn 6045	. . . . . . . . . . . . . . . . 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 23988	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ₀⟶ℂ)
197		ffn 6045	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ₀⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ₀)
198	185, 196, 197	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ₀)
199		nn0ex 11298	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ∈ V
200	199	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ₀ ∈ V)
201		inidm 3822	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ ℕ₀) = ℕ₀
202		coeidp 24019	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ₀ → ((coeff‘X_p)‘1) = if(1 = 1, 1, 0))
203	202	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘X_p)‘1) = if(1 = 1, 1, 0))
204		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
205	204	iftruei 4093	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
206	203, 205	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ((coeff‘X_p)‘1) = 1)
207		0lt1 10550	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
208		0re 10040	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
209		1re 10039	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
210	208, 209	ltnlei 10158	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
211	207, 210	mpbi 220	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
212	50	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → 𝑧 ∈ ℂ)
213		0dgr 24001	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
214	212, 213	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (deg‘(ℂ × {𝑧})) = 0)
215	214	breq2d 4665	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
216	211, 215	mtbiri 317	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
217		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
218	187, 217	dgrub 23990	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ₀ ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
219	218	3expia 1267	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ₀) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
220	185, 219	sylan 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
221	220	necon1bd 2812	. . . . . . . . . . . . . . . 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 6906	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ₀) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
224	191, 223	mpan2 707	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
225		1m0e1 11131	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
226	224, 225	syl6eq 2672	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = 1)
227	190, 226	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) = 1)
228	180, 227	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) = 1)
229	228	oveq1d 6665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
230	177	coef3 23988	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ₀⟶ℂ)
231	32, 230	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ₀⟶ℂ)
232	231, 34	ffvelrnd 6360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
233	232	mulid2d 10058	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
234	229, 233	eqtrd 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘(deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
235	175, 179, 234	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
236	157, 235	oveq12d 6668	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
237	236	negeqd 10275	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
238	155, 237	eqtr4d 2659	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
239	134, 238	oveq12d 6668	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (^◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
240	50	negcld 10379	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
241		nnm1nn0 11334	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ₀)
242	3, 241	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
243	242	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ₀)
244	231, 243	ffvelrnd 6360	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
245	235, 232	eqeltrd 2701	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
246	9, 27	dgreq0 24021	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
247	43, 246	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
248	247	necon3bid 2838	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0_𝑝 ↔ (𝐴‘𝑁) ≠ 0))
249	83, 248	mpbid 222	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
250	244, 245, 249	divcld 10801	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
251	240, 250	negdid 10405	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
252	240, 245	mulcld 10060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
253	252, 244, 245, 249	divdird 10839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
254		nnm1nn0 11334	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
255	5, 254	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
256	255	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ₀)
257	176, 177	coemul 24008	. . . . . . . . 9 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
258	69, 32, 256, 257	syl3anc 1326	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
259	159	fveq1d 6193	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((X_p ∘_𝑓 − (ℂ × {𝑧})) ∘_𝑓 · 𝑄))‘(𝑁 − 1)))
260		1e0p1 11552	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
261	260	oveq2i 6661	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
262	261	sumeq1i 14428	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
263		0nn0 11307	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
264		nn0uz 11722	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
265	263, 264	eleqtri 2699	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ_≥‘0)
266	265	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ_≥‘0))
267	261	eleq2i 2693	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
268	176	coef3 23988	. . . . . . . . . . . . . . 15 ⊢ ((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ)
269	69, 268	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ)
270		elfznn0 12433	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ₀)
271		ffvelrn 6357	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧}))):ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
272	269, 270, 271	syl2an 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
273	2	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
274		pncan 10287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
275	102, 101, 274	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
276	273, 275	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
277	276	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
278	3	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
279	277, 278	eqeltrd 2701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
280		nnuz 11723	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
281	279, 280	syl6eleq 2711	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ_≥‘1))
282		fzss2 12381	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
283	281, 282	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
284	283	sselda 3603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
285		fznn0sub 12373	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ₀)
286		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ (((coeff‘𝑄):ℕ₀⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ₀) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
287	231, 285, 286	syl2an 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
288	284, 287	syldan 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
289	272, 288	mulcld 10060	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
290	267, 289	sylan2br 493	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
291		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
292	291, 260	syl6eqr 2674	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
293	292	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1))
294	292	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
295	294	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
296	293, 295	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
297	266, 290, 296	fsump1 14487	. . . . . . . . . 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 2668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
299		eldifn 3733	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
300	299	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
301		eldifi 3732	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
302		elfznn0 12433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
303	301, 302	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ₀)
304	176, 169	dgrub 23990	. . . . . . . . . . . . . . . . 17 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ₀ ∧ ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))))
305	304	3expia 1267	. . . . . . . . . . . . . . . 16 ⊢ (((X_p ∘_𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ₀) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
306	69, 303, 305	syl2an 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
307		elfzuz 12338	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ_≥‘0))
308	301, 307	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ_≥‘0))
309	308	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ_≥‘0))
310		1z 11407	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
311		elfz5 12334	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
312	309, 310, 311	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
313	161	breq2d 4665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
314	313	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
315	312, 314	bitr4d 271	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(X_p ∘_𝑓 − (ℂ × {𝑧})))))
316	306, 315	sylibrd 249	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
317	316	necon1bd 2812	. . . . . . . . . . . . 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 6665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
320	301, 287	sylan2 491	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
321	320	mul02d 10234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
322	319, 321	eqtrd 2656	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
323		fzfid 12772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
324	283, 289, 322, 323	fsumss 14456	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
325		0z 11388	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
326	189	fveq1d 6193	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) = (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0))
327		coeidp 24019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ₀ → ((coeff‘X_p)‘0) = if(0 = 1, 1, 0))
328	162	nesymi 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
329	328	iffalsei 4096	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
330	327, 329	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ₀ → ((coeff‘X_p)‘0) = 0)
331	330	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → ((coeff‘X_p)‘0) = 0)
332		0cn 10032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
333		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
334	333	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
335	332, 334	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
336	187	coefv0 24004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
337	185, 336	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
338	335, 337	syl5reqr 2671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
339	338	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
340	195, 198, 200, 200, 201, 331, 339	ofval 6906	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ₀) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
341	263, 340	mpan2 707	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
342		df-neg 10269	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
343	341, 342	syl6eqr 2674	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘X_p) ∘_𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
344	326, 343	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) = -𝑧)
345	277	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
346	103	subid1d 10381	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
347	345, 346, 31	3eqtrd 2660	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
348	347	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
349	348, 235	eqtr4d 2659	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
350	344, 349	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
351	350, 252	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
352		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0))
353		oveq2 6658	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
354	353	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
355	352, 354	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
356	355	fsum1 14476	. . . . . . . . . . . 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 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
358	357, 350	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
359	277	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 1) = (𝐷 − 1))
360	359	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
361	227, 360	oveq12d 6668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
362	244	mulid2d 10058	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
363	361, 362	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
364	358, 363	oveq12d 6668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
365	298, 324, 364	3eqtr3rd 2665	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(X_p ∘_𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
366	258, 259, 365	3eqtr4rd 2667	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
367	366	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	240, 245, 249	divcan4d 10807	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
369	368	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
370	253, 367, 369	3eqtr3rd 2665	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
371	370	negeqd 10275	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
372	251, 371	eqtr3d 2658	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
373	129, 239, 372	3eqtrd 2660	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
374	25, 373	exlimddv 1863	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 ifcif 4086 {csn 4177 class class class wbr 4653 × cxp 5112 ^◡ccnv 5113 dom cdm 5114 “ cima 5117 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ∘_𝑓 cof 6895 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 #chash 13117 Σcsu 14416 0_𝑝c0p 23436 Polycply 23940 X_pcidp 23941 coeffccoe 23942 degcdgr 23943 quot cquot 24045

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-0p 23437 df-ply 23944 df-idp 23945 df-coe 23946 df-dgr 23947 df-quot 24046

This theorem is referenced by: vieta1 24067

W3C validator