Theorem vieta1lem2 26375

Description: Lemma for vieta1 26376: 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 (Xp ∘f − (ℂ × {𝑧})))

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 12227	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2863	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 12263	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 3024	. . . 4 ⊢ (𝜑 → (♯‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	eqnetrrid 3032	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12		dgr0 26322	. . . . . . . . . . 11 ⊢ (deg‘0𝑝) = 0
13	11, 12	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 2989	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 “ {0})
17	16	fta1 26372	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 593	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 498	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 14376	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 3001	. . . 4 ⊢ (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 234	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 4305	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 220	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 4161	. . . . 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 (Xp ∘f − (ℂ × {𝑧})))
30	27, 9, 16, 8, 1, 3, 2, 28, 29	vieta1lem1 26374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 498	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 26293	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ0)
35	34	nn0red 12543	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 12122	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 11318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4744	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → {𝑧} ⊆ (◡𝑄 “ {0}))
40		ssequn1 4138	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (◡𝑄 “ {0}) ↔ ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
41	39, 40	sylib 220	. . . . . . . . . 10 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
42	41	fveq2d 6871	. . . . . . . . 9 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})))
43	8	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 6071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3982	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 26258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	sseqtrid 3978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3936	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2854	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◡𝐹 “ {0}))
52		ffn 6691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 7041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℂ → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
54	8, 46, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
55	51, 54	bitrid 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
56	55	simplbda 503	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0)
57		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (Xp ∘f − (ℂ × {𝑧})) = (Xp ∘f − (ℂ × {𝑧}))
58	57	facth 26370	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1390	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
60	29	oveq2i 7407	. . . . . . . . . . . . . . . . 17 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))))
61	59, 60	eqtr4di 2815	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
62	61	cnveqd 5847	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ◡𝐹 = ◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
63	62	imaeq1d 6048	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝐹 “ {0}) = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
64	16, 63	eqtrid 2809	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65		cnex 11154	. . . . . . . . . . . . . 14 ⊢ ℂ ∈ V
66	57	plyremlem 26368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℂ → ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1 ∧ (◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) = {𝑧}))
67	50, 66	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1 ∧ (◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) = {𝑧}))
68	67	simp1d 1155	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69		plyf 26258	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
71		plyf 26258	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
72	32, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
73		ofmulrt 26343	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
74	65, 70, 72, 73	mp3an2i 1487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
75	67	simp3d 1157	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) = {𝑧})
76	75	uneq1d 4120	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})) = ({𝑧} ∪ (◡𝑄 “ {0})))
77	64, 74, 76	3eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (◡𝑄 “ {0})))
78	77	fveq2d 6871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (◡𝑄 “ {0}))))
79	1, 2	eqtr4d 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑅) = (𝐷 + 1))
80	79	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (𝐷 + 1))
81	78, 80	eqtr3d 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (𝐷 + 1))
82	15	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0𝑝)
83	61, 82	eqnetrrd 3025	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84		plymul0or 26342	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
85	68, 32, 84	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
86	85	necon3abid 2993	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
87	83, 86	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88		neanior 3050	. . . . . . . . . . . . . . . 16 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝) ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
89	87, 88	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝))
90	89	simprd 499	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠ 0𝑝)
91		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (◡𝑄 “ {0}) = (◡𝑄 “ {0})
92	91	fta1 26372	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄)))
93	32, 90, 92	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄)))
94	93	simprd 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄))
95	94, 31	breqtrrd 5128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ 𝐷)
96		snfi 9024	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
97	93	simpld 498	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝑄 “ {0}) ∈ Fin)
98		hashun2 14396	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (◡𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
99	96, 97, 98	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
100		ax-1cn 11131	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
101	3	nncnd 12226	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
102	101	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
103		addcom 11369	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104	100, 102, 103	sylancr 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
105	81, 104	eqtr4d 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (1 + 𝐷))
106		hashsng 14382	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (♯‘{𝑧}) = 1)
107	106	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘{𝑧}) = 1)
108	107	oveq1d 7411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))) = (1 + (♯‘(◡𝑄 “ {0}))))
109	99, 105, 108	3brtr3d 5131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0}))))
110		hashcl 14369	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑄 “ {0}) ∈ Fin → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
111	97, 110	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
112	111	nn0red 12543	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℝ)
113		1red 11182	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
114	36, 112, 113	leadd2d 11782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (♯‘(◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0})))))
115	109, 114	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (♯‘(◡𝑄 “ {0})))
116	112, 36	letri3d 11325	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘(◡𝑄 “ {0})) = 𝐷 ↔ ((♯‘(◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (♯‘(◡𝑄 “ {0})))))
117	95, 115, 116	mpbir2and 723	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = 𝐷)
118	81, 117	eqeq12d 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
119	42, 118	imbitrid 246	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120	119	necon3ad 2970	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (◡𝑄 “ {0})))
121	38, 120	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (◡𝑄 “ {0}))
122		disjsn 4670	. . . . . 6 ⊢ (((◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (◡𝑄 “ {0}))
123	121, 122	sylibr 236	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
124	26, 123	eqtrid 2809	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (◡𝑄 “ {0})) = ∅)
125	19	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
126	49	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
127	126	sselda 3936	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
128	124, 77, 125, 127	fsumsplit 15768	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥))
129		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
130	129	sumsn 15773	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
131	50, 50, 130	syl2anc 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50	negnegd 11533	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
133	131, 132	eqtr4d 2800	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134	117, 31	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))
135		fveq2 6867	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136	135	eqeq2d 2773	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137		cnveq 5845	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ◡𝑓 = ◡𝑄)
138	137	imaeq1d 6048	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (◡𝑓 “ {0}) = (◡𝑄 “ {0}))
139	138	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (♯‘(◡𝑓 “ {0})) = (♯‘(◡𝑄 “ {0})))
140	139, 135	eqeq12d 2778	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((♯‘(◡𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)))
141	136, 140	anbi12d 641	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))))
142	138	sumeq1d 15727	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (◡𝑄 “ {0})𝑥)
143		fveq2 6867	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144	135	oveq1d 7411	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145	143, 144	fveq12d 6874	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146	143, 135	fveq12d 6874	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147	145, 146	oveq12d 7414	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148	147	negeqd 11424	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149	142, 148	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → (Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
150	141, 149	imbi12d 346	. . . . . . 7 ⊢ (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
151	28	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
152	150, 151, 32	rspcdva 3582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
153	31, 134, 152	mp2and 709	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
154	31	fvoveq1d 7418	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
155	61	fveq2d 6871	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
156	27, 155	eqtrid 2809	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
157	61	fveq2d 6871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
158	67	simp2d 1156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1)
159		ax-1ne0 11142	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
160	159	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
161	158, 160	eqnetrd 3024	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0)
162		fveq2 6867	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘0𝑝))
163	162, 12	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 0)
164	163	necon3i 2989	. . . . . . . . . . . . 13 ⊢ ((deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0 → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
165	161, 164	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
166		eqid 2762	. . . . . . . . . . . . 13 ⊢ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘(Xp ∘f − (ℂ × {𝑧})))
167		eqid 2762	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
168	166, 167	dgrmul 26330	. . . . . . . . . . . 12 ⊢ ((((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
169	68, 165, 32, 90, 168	syl22anc 849	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
170	157, 169	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
171	9, 170	eqtrid 2809	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	156, 171	fveq12d 6874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))))
173		eqid 2762	. . . . . . . . . 10 ⊢ (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = (coeff‘(Xp ∘f − (ℂ × {𝑧})))
174		eqid 2762	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
175	173, 174, 166, 167	coemulhi 26314	. . . . . . . . 9 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
176	68, 32, 175	syl2anc 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
177	158	fveq2d 6871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
178		ssid 3958	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
179		plyid 26269	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180	178, 100, 179	mp2an 702	. . . . . . . . . . . . . 14 ⊢ Xp ∈ (Poly‘ℂ)
181		plyconst 26266	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182	178, 50, 181	sylancr 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (coeff‘Xp) = (coeff‘Xp)
184		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185	183, 184	coesub 26317	. . . . . . . . . . . . . 14 ⊢ ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
186	180, 182, 185	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
187	186	fveq1d 6869	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188		1nn0 12497	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
189	183	coef3 26292	. . . . . . . . . . . . . . . . 17 ⊢ (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190		ffn 6691	. . . . . . . . . . . . . . . . 17 ⊢ ((coeff‘Xp):ℕ0⟶ℂ → (coeff‘Xp) Fn ℕ0)
191	180, 189, 190	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ (coeff‘Xp) Fn ℕ0
192	191	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘Xp) Fn ℕ0)
193	184	coef3 26292	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194		ffn 6691	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195	182, 193, 194	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196		nn0ex 12487	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ∈ V
197	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ0 ∈ V)
198		inidm 4178	. . . . . . . . . . . . . . 15 ⊢ (ℕ0 ∩ ℕ0) = ℕ0
199		coeidp 26323	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
200	199	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
201		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
202	201	iftruei 4487	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
203	200, 202	eqtrdi 2813	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204		0lt1 11709	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
205		0re 11183	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
206		1re 11181	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
207	205, 206	ltnlei 11304	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
208	204, 207	mpbi 232	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
209	50	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210		0dgr 26305	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212	211	breq2d 5112	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213	208, 212	mtbiri 329	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214		eqid 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215	184, 214	dgrub 26294	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
216	215	3expia 1134	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
217	182, 216	sylan 589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
218	217	necon1bd 2975	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
219	213, 218	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
220	192, 195, 197, 197, 198, 203, 219	ofval 7671	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
221	188, 220	mpan2 701	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222		1m0e1 12337	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
223	221, 222	eqtrdi 2813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224	187, 223	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = 1)
225	177, 224	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = 1)
226	225	oveq1d 7411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227	174	coef3 26292	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
228	32, 227	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229	228, 34	ffvelcdmd 7066	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230	229	mullidd 11200	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231	226, 230	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232	172, 176, 231	3eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233	154, 232	oveq12d 7414	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234	233	negeqd 11424	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235	153, 234	eqtr4d 2800	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
236	133, 235	oveq12d 7414	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
237	50	negcld 11529	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
238		nnm1nn0 12522	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
239	3, 238	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ0)
240	239	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ0)
241	228, 240	ffvelcdmd 7066	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242	232, 229	eqeltrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
243	9, 27	dgreq0 26325	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
244	43, 243	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
245	244	necon3bid 3001	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴‘𝑁) ≠ 0))
246	82, 245	mpbid 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
247	241, 242, 246	divcld 11967	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
248	237, 247	negdid 11555	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
249	237, 242	mulcld 11202	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
250	249, 241, 242, 246	divdird 12005	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
251		nnm1nn0 12522	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
252	5, 251	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ0)
253	252	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ0)
254	173, 174	coemul 26312	. . . . . . . . 9 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
255	68, 32, 253, 254	syl3anc 1390	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256	156	fveq1d 6869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257		1e0p1 12735	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
258	257	oveq2i 7407	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
259	258	sumeq1i 15724	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260		0nn0 12496	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
261		nn0uz 12877	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
262	260, 261	eleqtri 2860	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ≥‘0)
263	262	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ≥‘0))
264	258	eleq2i 2854	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265	173	coef3 26292	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
266	68, 265	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267		elfznn0 13625	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268		ffvelcdm 7062	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269	266, 267, 268	syl2an 605	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
270	2	oveq1d 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271		pncan 11436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272	101, 100, 271	sylancl 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273	270, 272	eqtr3d 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
274	273	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
275	3	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
276	274, 275	eqeltrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
277		nnuz 12878	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
278	276, 277	eleqtrdi 2872	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ≥‘1))
279		fzss2 13569	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280	278, 279	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281	280	sselda 3936	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282		fznn0sub 13561	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283		ffvelcdm 7062	. . . . . . . . . . . . . . 15 ⊢ (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
284	228, 282, 283	syl2an 605	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
285	281, 284	syldan 600	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
286	269, 285	mulcld 11202	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
287	264, 286	sylan2br 604	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
288		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
289	288, 257	eqtr4di 2815	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
290	289	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
291	289	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292	291	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293	290, 292	oveq12d 7414	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294	263, 287, 293	fsump1 15783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
295	259, 294	eqtrid 2809	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296		eldifn 4085	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297	296	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298		eldifi 4084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299		elfznn0 13625	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300	298, 299	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301	173, 166	dgrub 26294	. . . . . . . . . . . . . . . . 17 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))))
302	301	3expia 1134	. . . . . . . . . . . . . . . 16 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
303	68, 300, 302	syl2an 605	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
304		elfzuz 13525	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘0))
305	298, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ≥‘0))
306	305	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ≥‘0))
307		1z 12601	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
308		elfz5 13521	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309	306, 307, 308	sylancl 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310	158	breq2d 5112	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
311	310	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
312	309, 311	bitr4d 284	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
313	303, 312	sylibrd 261	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
314	313	necon1bd 2975	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = 0))
315	297, 314	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = 0)
316	315	oveq1d 7411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
317	298, 284	sylan2 602	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
318	317	mul02d 11381	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319	316, 318	eqtrd 2797	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320		fzfid 13986	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321	280, 286, 319, 320	fsumss 15752	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322		0z 12579	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
323	186	fveq1d 6869	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324		coeidp 26323	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325	159	nesymi 3014	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
326	325	iffalsei 4490	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
327	324, 326	eqtrdi 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328	327	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329	184	coefv0 26308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
330	182, 329	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
331		0cn 11171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
332		vex 3458	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
333	332	fvconst2 7188	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
334	331, 333	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
335	330, 334	eqtr3di 2812	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336	335	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337	192, 195, 197, 197, 198, 328, 336	ofval 7671	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338	260, 337	mpan2 701	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339		df-neg 11417	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
340	338, 339	eqtr4di 2815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341	323, 340	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = -𝑧)
342	274	oveq1d 7411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343	102	subid1d 11531	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
344	342, 343, 31	3eqtrd 2801	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345	344	fveq2d 6871	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346	345, 232	eqtr4d 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
347	341, 346	oveq12d 7414	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
348	347, 249	eqeltrd 2862	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349		fveq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0))
350		oveq2 7404	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351	350	fveq2d 6871	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352	349, 351	oveq12d 7414	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353	352	fsum1 15774	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
354	322, 348, 353	sylancr 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
355	354, 347	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
356	274	fvoveq1d 7418	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357	224, 356	oveq12d 7414	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358	241	mullidd 11200	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359	357, 358	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360	355, 359	oveq12d 7414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361	295, 321, 360	3eqtr3rd 2806	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362	255, 256, 361	3eqtr4rd 2808	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363	362	oveq1d 7411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
364	237, 242, 246	divcan4d 11973	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
365	364	oveq1d 7411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
366	250, 363, 365	3eqtr3rd 2806	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
367	366	negeqd 11424	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	248, 367	eqtr3d 2799	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
369	128, 236, 368	3eqtrd 2801	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
370	25, 369	exlimddv 1955	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1098   = wceq 1560  ∃wex 1799   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  ifcif 4480  {csn 4582   class class class wbr 5100   × cxp 5645  ^◡ccnv 5646  dom cdm 5647   “ cima 5650   Fn wfn 6516  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396   ∘_f cof 7658  Fincfn 8927  ℂcc 11071  ℝcr 11072  0cc0 11073  1c1 11074   + caddc 11076   · cmul 11078   < clt 11216   ≤ cle 11217   − cmin 11414  -cneg 11415   / cdiv 11844  ℕcn 12210  ℕ₀cn0 12481  ℤcz 12568  ℤ_≥cuz 12839  ...cfz 13512  ♯chash 14343  Σcsu 15713  0_𝑝c0p 25731  Polycply 26244  X_pcidp 26245  coeffccoe 26246  degcdgr 26247   quot cquot 26354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-inf2 9596  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150  ax-pre-sup 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7660  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-oadd 8441  df-er 8678  df-map 8810  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-sup 9388  df-inf 9389  df-oi 9458  df-dju 9859  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-div 11845  df-nn 12211  df-2 12280  df-3 12281  df-n0 12482  df-xnn0 12555  df-z 12569  df-uz 12840  df-rp 12994  df-fz 13513  df-fzo 13660  df-fl 13802  df-seq 14015  df-exp 14075  df-hash 14344  df-cj 15126  df-re 15127  df-im 15128  df-sqrt 15262  df-abs 15263  df-clim 15515  df-rlim 15516  df-sum 15714  df-0p 25732  df-ply 26248  df-idp 26249  df-coe 26250  df-dgr 26251  df-quot 26355

This theorem is referenced by:  vieta1  26376