Theorem vieta1lem2 24892

Description: Lemma for vieta1 24893: 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 11647	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2912	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 11679	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 3081	. . . 4 ⊢ (𝜑 → (♯‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	eqnetrrid 3089	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6663	. . . . . . . . . . 11 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12		dgr0 24844	. . . . . . . . . . 11 ⊢ (deg‘0𝑝) = 0
13	11, 12	syl6eq 2870	. . . . . . . . . 10 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 3046	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 “ {0})
17	16	fta1 24889	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 497	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 13716	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 3058	. . . 4 ⊢ (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 234	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 4308	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 220	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 4176	. . . . 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 24891	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 498	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 497	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 24815	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ0)
35	34	nn0red 11948	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2911	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 11562	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 10767	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4733	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → {𝑧} ⊆ (◡𝑄 “ {0}))
40		ssequn1 4154	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (◡𝑄 “ {0}) ↔ ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
41	39, 40	sylib 220	. . . . . . . . . 10 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
42	41	fveq2d 6667	. . . . . . . . 9 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})))
43	8	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 5942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3999	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 24780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	sseqtrid 4017	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3965	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◡𝐹 “ {0}))
52		ffn 6507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 6823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℂ → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
54	8, 46, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
55	51, 54	syl5bb 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
56	55	simplbda 502	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0)
57		eqid 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (Xp ∘f − (ℂ × {𝑧})) = (Xp ∘f − (ℂ × {𝑧}))
58	57	facth 24887	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1366	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
60	29	oveq2i 7159	. . . . . . . . . . . . . . . . 17 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))))
61	59, 60	syl6eqr 2872	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
62	61	cnveqd 5739	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ◡𝐹 = ◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
63	62	imaeq1d 5921	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝐹 “ {0}) = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
64	16, 63	syl5eq 2866	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65		cnex 10610	. . . . . . . . . . . . . 14 ⊢ ℂ ∈ V
66	57	plyremlem 24885	. . . . . . . . . . . . . . . . 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 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69		plyf 24780	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
71		plyf 24780	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
72	32, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
73		ofmulrt 24863	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
74	65, 70, 72, 73	mp3an2i 1460	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
75	67	simp3d 1139	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) = {𝑧})
76	75	uneq1d 4136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})) = ({𝑧} ∪ (◡𝑄 “ {0})))
77	64, 74, 76	3eqtrd 2858	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (◡𝑄 “ {0})))
78	77	fveq2d 6667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (◡𝑄 “ {0}))))
79	1, 2	eqtr4d 2857	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑅) = (𝐷 + 1))
80	79	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (𝐷 + 1))
81	78, 80	eqtr3d 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (𝐷 + 1))
82	15	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0𝑝)
83	61, 82	eqnetrrd 3082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84		plymul0or 24862	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
85	68, 32, 84	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
86	85	necon3abid 3050	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
87	83, 86	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88		neanior 3107	. . . . . . . . . . . . . . . 16 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝) ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
89	87, 88	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝))
90	89	simprd 498	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠ 0𝑝)
91		eqid 2819	. . . . . . . . . . . . . . 15 ⊢ (◡𝑄 “ {0}) = (◡𝑄 “ {0})
92	91	fta1 24889	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄)))
93	32, 90, 92	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄)))
94	93	simprd 498	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄))
95	94, 31	breqtrrd 5085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ 𝐷)
96		snfi 8586	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
97	93	simpld 497	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝑄 “ {0}) ∈ Fin)
98		hashun2 13736	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (◡𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
99	96, 97, 98	sylancr 589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
100		ax-1cn 10587	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
101	3	nncnd 11646	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
102	101	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
103		addcom 10818	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104	100, 102, 103	sylancr 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
105	81, 104	eqtr4d 2857	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (1 + 𝐷))
106		hashsng 13722	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (♯‘{𝑧}) = 1)
107	106	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘{𝑧}) = 1)
108	107	oveq1d 7163	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))) = (1 + (♯‘(◡𝑄 “ {0}))))
109	99, 105, 108	3brtr3d 5088	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0}))))
110		hashcl 13709	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑄 “ {0}) ∈ Fin → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
111	97, 110	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
112	111	nn0red 11948	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℝ)
113		1red 10634	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
114	36, 112, 113	leadd2d 11227	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (♯‘(◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0})))))
115	109, 114	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (♯‘(◡𝑄 “ {0})))
116	112, 36	letri3d 10774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘(◡𝑄 “ {0})) = 𝐷 ↔ ((♯‘(◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (♯‘(◡𝑄 “ {0})))))
117	95, 115, 116	mpbir2and 711	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = 𝐷)
118	81, 117	eqeq12d 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
119	42, 118	syl5ib 246	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120	119	necon3ad 3027	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (◡𝑄 “ {0})))
121	38, 120	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (◡𝑄 “ {0}))
122		disjsn 4639	. . . . . 6 ⊢ (((◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (◡𝑄 “ {0}))
123	121, 122	sylibr 236	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
124	26, 123	syl5eq 2866	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (◡𝑄 “ {0})) = ∅)
125	19	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
126	49	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
127	126	sselda 3965	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
128	124, 77, 125, 127	fsumsplit 15089	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥))
129		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
130	129	sumsn 15093	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
131	50, 50, 130	syl2anc 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50	negnegd 10980	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
133	131, 132	eqtr4d 2857	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134	117, 31	eqtrd 2854	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))
135		fveq2 6663	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136	135	eqeq2d 2830	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137		cnveq 5737	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ◡𝑓 = ◡𝑄)
138	137	imaeq1d 5921	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (◡𝑓 “ {0}) = (◡𝑄 “ {0}))
139	138	fveq2d 6667	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (♯‘(◡𝑓 “ {0})) = (♯‘(◡𝑄 “ {0})))
140	139, 135	eqeq12d 2835	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((♯‘(◡𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)))
141	136, 140	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))))
142	138	sumeq1d 15050	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (◡𝑄 “ {0})𝑥)
143		fveq2 6663	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144	135	oveq1d 7163	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145	143, 144	fveq12d 6670	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146	143, 135	fveq12d 6670	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147	145, 146	oveq12d 7166	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148	147	negeqd 10872	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149	142, 148	eqeq12d 2835	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → (Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
150	141, 149	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
151	28	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
152	150, 151, 32	rspcdva 3623	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
153	31, 134, 152	mp2and 697	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
154	31	fvoveq1d 7170	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
155	61	fveq2d 6667	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
156	27, 155	syl5eq 2866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
157	61	fveq2d 6667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
158	67	simp2d 1138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1)
159		ax-1ne0 10598	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
160	159	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
161	158, 160	eqnetrd 3081	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0)
162		fveq2 6663	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘0𝑝))
163	162, 12	syl6eq 2870	. . . . . . . . . . . . . 14 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 0)
164	163	necon3i 3046	. . . . . . . . . . . . 13 ⊢ ((deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0 → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
165	161, 164	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
166		eqid 2819	. . . . . . . . . . . . 13 ⊢ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘(Xp ∘f − (ℂ × {𝑧})))
167		eqid 2819	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
168	166, 167	dgrmul 24852	. . . . . . . . . . . 12 ⊢ ((((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
169	68, 165, 32, 90, 168	syl22anc 836	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
170	157, 169	eqtrd 2854	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
171	9, 170	syl5eq 2866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	156, 171	fveq12d 6670	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))))
173		eqid 2819	. . . . . . . . . 10 ⊢ (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = (coeff‘(Xp ∘f − (ℂ × {𝑧})))
174		eqid 2819	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
175	173, 174, 166, 167	coemulhi 24836	. . . . . . . . 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 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
177	158	fveq2d 6667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
178		ssid 3987	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
179		plyid 24791	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180	178, 100, 179	mp2an 690	. . . . . . . . . . . . . 14 ⊢ Xp ∈ (Poly‘ℂ)
181		plyconst 24788	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182	178, 50, 181	sylancr 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183		eqid 2819	. . . . . . . . . . . . . . 15 ⊢ (coeff‘Xp) = (coeff‘Xp)
184		eqid 2819	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185	183, 184	coesub 24839	. . . . . . . . . . . . . 14 ⊢ ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
186	180, 182, 185	sylancr 589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
187	186	fveq1d 6665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188		1nn0 11905	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
189	183	coef3 24814	. . . . . . . . . . . . . . . . 17 ⊢ (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190		ffn 6507	. . . . . . . . . . . . . . . . 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 24814	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194		ffn 6507	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195	182, 193, 194	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196		nn0ex 11895	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ∈ V
197	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ0 ∈ V)
198		inidm 4193	. . . . . . . . . . . . . . 15 ⊢ (ℕ0 ∩ ℕ0) = ℕ0
199		coeidp 24845	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
200	199	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
201		eqid 2819	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
202	201	iftruei 4472	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
203	200, 202	syl6eq 2870	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204		0lt1 11154	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
205		0re 10635	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
206		1re 10633	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
207	205, 206	ltnlei 10753	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
208	204, 207	mpbi 232	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
209	50	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210		0dgr 24827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212	211	breq2d 5069	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213	208, 212	mtbiri 329	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214		eqid 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215	184, 214	dgrub 24816	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
216	215	3expia 1116	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
217	182, 216	sylan 582	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
218	217	necon1bd 3032	. . . . . . . . . . . . . . . 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 7410	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
221	188, 220	mpan2 689	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222		1m0e1 11750	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
223	221, 222	syl6eq 2870	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224	187, 223	eqtrd 2854	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = 1)
225	177, 224	eqtrd 2854	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = 1)
226	225	oveq1d 7163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227	174	coef3 24814	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
228	32, 227	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229	228, 34	ffvelrnd 6845	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230	229	mulid2d 10651	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231	226, 230	eqtrd 2854	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232	172, 176, 231	3eqtrd 2858	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233	154, 232	oveq12d 7166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234	233	negeqd 10872	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235	153, 234	eqtr4d 2857	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
236	133, 235	oveq12d 7166	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
237	50	negcld 10976	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
238		nnm1nn0 11930	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
239	3, 238	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ0)
240	239	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ0)
241	228, 240	ffvelrnd 6845	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242	232, 229	eqeltrd 2911	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
243	9, 27	dgreq0 24847	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
244	43, 243	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
245	244	necon3bid 3058	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴‘𝑁) ≠ 0))
246	82, 245	mpbid 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
247	241, 242, 246	divcld 11408	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
248	237, 247	negdid 11002	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
249	237, 242	mulcld 10653	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
250	249, 241, 242, 246	divdird 11446	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
251		nnm1nn0 11930	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
252	5, 251	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ0)
253	252	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ0)
254	173, 174	coemul 24834	. . . . . . . . 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 1366	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256	156	fveq1d 6665	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257		1e0p1 12132	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
258	257	oveq2i 7159	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
259	258	sumeq1i 15047	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260		0nn0 11904	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
261		nn0uz 12272	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
262	260, 261	eleqtri 2909	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ≥‘0)
263	262	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ≥‘0))
264	258	eleq2i 2902	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265	173	coef3 24814	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
266	68, 265	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267		elfznn0 12992	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268		ffvelrn 6842	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269	266, 267, 268	syl2an 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
270	2	oveq1d 7163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271		pncan 10884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272	101, 100, 271	sylancl 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273	270, 272	eqtr3d 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
274	273	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
275	3	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
276	274, 275	eqeltrd 2911	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
277		nnuz 12273	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
278	276, 277	eleqtrdi 2921	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ≥‘1))
279		fzss2 12939	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280	278, 279	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281	280	sselda 3965	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282		fznn0sub 12931	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283		ffvelrn 6842	. . . . . . . . . . . . . . 15 ⊢ (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
284	228, 282, 283	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
285	281, 284	syldan 593	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
286	269, 285	mulcld 10653	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
287	264, 286	sylan2br 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
288		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
289	288, 257	syl6eqr 2872	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
290	289	fveq2d 6667	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
291	289	oveq2d 7164	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292	291	fveq2d 6667	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293	290, 292	oveq12d 7166	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294	263, 287, 293	fsump1 15103	. . . . . . . . . 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	syl5eq 2866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296		eldifn 4102	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297	296	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298		eldifi 4101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299		elfznn0 12992	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300	298, 299	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301	173, 166	dgrub 24816	. . . . . . . . . . . . . . . . 17 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))))
302	301	3expia 1116	. . . . . . . . . . . . . . . 16 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
303	68, 300, 302	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
304		elfzuz 12896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘0))
305	298, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ≥‘0))
306	305	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ≥‘0))
307		1z 12004	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
308		elfz5 12892	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309	306, 307, 308	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310	158	breq2d 5069	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
311	310	adantr 483	. . . . . . . . . . . . . . . 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 3032	. . . . . . . . . . . . 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 7163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
317	298, 284	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
318	317	mul02d 10830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319	316, 318	eqtrd 2854	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320		fzfid 13333	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321	280, 286, 319, 320	fsumss 15074	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322		0z 11984	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
323	186	fveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324		coeidp 24845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325	159	nesymi 3071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
326	325	iffalsei 4475	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
327	324, 326	syl6eq 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328	327	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329		0cn 10625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
330		vex 3496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
331	330	fvconst2 6959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
332	329, 331	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
333	184	coefv0 24830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
334	182, 333	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
335	332, 334	syl5reqr 2869	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336	335	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337	192, 195, 197, 197, 198, 328, 336	ofval 7410	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338	260, 337	mpan2 689	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339		df-neg 10865	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
340	338, 339	syl6eqr 2872	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341	323, 340	eqtrd 2854	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = -𝑧)
342	274	oveq1d 7163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343	102	subid1d 10978	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
344	342, 343, 31	3eqtrd 2858	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345	344	fveq2d 6667	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346	345, 232	eqtr4d 2857	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
347	341, 346	oveq12d 7166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
348	347, 249	eqeltrd 2911	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349		fveq2 6663	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0))
350		oveq2 7156	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351	350	fveq2d 6667	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352	349, 351	oveq12d 7166	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353	352	fsum1 15094	. . . . . . . . . . . 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 589	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
355	354, 347	eqtrd 2854	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
356	274	fvoveq1d 7170	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357	224, 356	oveq12d 7166	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358	241	mulid2d 10651	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359	357, 358	eqtrd 2854	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360	355, 359	oveq12d 7166	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361	295, 321, 360	3eqtr3rd 2863	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362	255, 256, 361	3eqtr4rd 2865	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363	362	oveq1d 7163	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
364	237, 242, 246	divcan4d 11414	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
365	364	oveq1d 7163	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
366	250, 363, 365	3eqtr3rd 2863	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
367	366	negeqd 10872	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	248, 367	eqtr3d 2856	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
369	128, 236, 368	3eqtrd 2858	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
370	25, 369	exlimddv 1930	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1082   = wceq 1531  ∃wex 1774   ∈ wcel 2108   ≠ wne 3014  ∀wral 3136  Vcvv 3493   ∖ cdif 3931   ∪ cun 3932   ∩ cin 3933   ⊆ wss 3934  ∅c0 4289  ifcif 4465  {csn 4559   class class class wbr 5057   × cxp 5546  ^◡ccnv 5547  dom cdm 5548   “ cima 5551   Fn wfn 6343  ⟶wf 6344  ‘cfv 6348  (class class class)co 7148   ∘_f cof 7399  Fincfn 8501  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668   − cmin 10862  -cneg 10863   / cdiv 11289  ℕcn 11630  ℕ₀cn0 11889  ℤcz 11973  ℤ_≥cuz 12235  ...cfz 12884  ♯chash 13682  Σcsu 15034  0_𝑝c0p 24262  Polycply 24766  X_pcidp 24767  coeffccoe 24768  degcdgr 24769   quot cquot 24871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-fal 1544  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-oi 8966  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12885  df-fzo 13026  df-fl 13154  df-seq 13362  df-exp 13422  df-hash 13683  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-rlim 14838  df-sum 15035  df-0p 24263  df-ply 24770  df-idp 24771  df-coe 24772  df-dgr 24773  df-quot 24872

This theorem is referenced by:  vieta1  24893