Theorem vieta1lem2 26275

Description: Lemma for vieta1 26276: 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 12162	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2837	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 12195	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 2999	. . . 4 ⊢ (𝜑 → (♯‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	eqnetrrid 3007	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12		dgr0 26224	. . . . . . . . . . 11 ⊢ (deg‘0𝑝) = 0
13	11, 12	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 2964	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 “ {0})
17	16	fta1 26272	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 14286	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 2976	. . . 4 ⊢ (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 232	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 4305	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 218	. 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 26274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 26194	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ0)
35	34	nn0red 12463	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 12072	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 11268	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4764	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → {𝑧} ⊆ (◡𝑄 “ {0}))
40		ssequn1 4138	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (◡𝑄 “ {0}) ↔ ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
41	39, 40	sylib 218	. . . . . . . . . 10 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
42	41	fveq2d 6838	. . . . . . . . 9 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})))
43	8	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 6041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3980	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 26159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6671	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	sseqtrid 3976	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3933	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◡𝐹 “ {0}))
52		ffn 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 7005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℂ → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
54	8, 46, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
55	51, 54	bitrid 283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0)))
56	55	simplbda 499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0)
57		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (Xp ∘f − (ℂ × {𝑧})) = (Xp ∘f − (ℂ × {𝑧}))
58	57	facth 26270	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
60	29	oveq2i 7369	. . . . . . . . . . . . . . . . 17 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))))
61	59, 60	eqtr4di 2789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
62	61	cnveqd 5824	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ◡𝐹 = ◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
63	62	imaeq1d 6018	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝐹 “ {0}) = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
64	16, 63	eqtrid 2783	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65		cnex 11107	. . . . . . . . . . . . . 14 ⊢ ℂ ∈ V
66	57	plyremlem 26268	. . . . . . . . . . . . . . . . 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 1142	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69		plyf 26159	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
71		plyf 26159	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
72	32, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
73		ofmulrt 26245	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
74	65, 70, 72, 73	mp3an2i 1468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
75	67	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) = {𝑧})
76	75	uneq1d 4119	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})) = ({𝑧} ∪ (◡𝑄 “ {0})))
77	64, 74, 76	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (◡𝑄 “ {0})))
78	77	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (◡𝑄 “ {0}))))
79	1, 2	eqtr4d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑅) = (𝐷 + 1))
80	79	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (𝐷 + 1))
81	78, 80	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (𝐷 + 1))
82	15	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0𝑝)
83	61, 82	eqnetrrd 3000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84		plymul0or 26244	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
85	68, 32, 84	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
86	85	necon3abid 2968	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
87	83, 86	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88		neanior 3025	. . . . . . . . . . . . . . . 16 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝) ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
89	87, 88	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝))
90	89	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠ 0𝑝)
91		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (◡𝑄 “ {0}) = (◡𝑄 “ {0})
92	91	fta1 26272	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄)))
93	32, 90, 92	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∈ Fin ∧ (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄)))
94	93	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ (deg‘𝑄))
95	94, 31	breqtrrd 5126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ 𝐷)
96		snfi 8980	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
97	93	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝑄 “ {0}) ∈ Fin)
98		hashun2 14306	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (◡𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
99	96, 97, 98	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
100		ax-1cn 11084	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
101	3	nncnd 12161	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
103		addcom 11319	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104	100, 102, 103	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
105	81, 104	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (1 + 𝐷))
106		hashsng 14292	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (♯‘{𝑧}) = 1)
107	106	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘{𝑧}) = 1)
108	107	oveq1d 7373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))) = (1 + (♯‘(◡𝑄 “ {0}))))
109	99, 105, 108	3brtr3d 5129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0}))))
110		hashcl 14279	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑄 “ {0}) ∈ Fin → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
111	97, 110	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
112	111	nn0red 12463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℝ)
113		1red 11133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
114	36, 112, 113	leadd2d 11732	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (♯‘(◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0})))))
115	109, 114	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (♯‘(◡𝑄 “ {0})))
116	112, 36	letri3d 11275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘(◡𝑄 “ {0})) = 𝐷 ↔ ((♯‘(◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (♯‘(◡𝑄 “ {0})))))
117	95, 115, 116	mpbir2and 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = 𝐷)
118	81, 117	eqeq12d 2752	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
119	42, 118	imbitrid 244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120	119	necon3ad 2945	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (◡𝑄 “ {0})))
121	38, 120	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (◡𝑄 “ {0}))
122		disjsn 4668	. . . . . 6 ⊢ (((◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (◡𝑄 “ {0}))
123	121, 122	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
124	26, 123	eqtrid 2783	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (◡𝑄 “ {0})) = ∅)
125	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
126	49	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
127	126	sselda 3933	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
128	124, 77, 125, 127	fsumsplit 15664	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥))
129		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
130	129	sumsn 15669	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
131	50, 50, 130	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50	negnegd 11483	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
133	131, 132	eqtr4d 2774	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134	117, 31	eqtrd 2771	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))
135		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136	135	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137		cnveq 5822	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ◡𝑓 = ◡𝑄)
138	137	imaeq1d 6018	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (◡𝑓 “ {0}) = (◡𝑄 “ {0}))
139	138	fveq2d 6838	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (♯‘(◡𝑓 “ {0})) = (♯‘(◡𝑄 “ {0})))
140	139, 135	eqeq12d 2752	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((♯‘(◡𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)))
141	136, 140	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))))
142	138	sumeq1d 15623	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (◡𝑄 “ {0})𝑥)
143		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144	135	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145	143, 144	fveq12d 6841	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146	143, 135	fveq12d 6841	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147	145, 146	oveq12d 7376	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148	147	negeqd 11374	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149	142, 148	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → (Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
150	141, 149	imbi12d 344	. . . . . . 7 ⊢ (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
151	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
152	150, 151, 32	rspcdva 3577	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
153	31, 134, 152	mp2and 699	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
154	31	fvoveq1d 7380	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
155	61	fveq2d 6838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
156	27, 155	eqtrid 2783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
157	61	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
158	67	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1)
159		ax-1ne0 11095	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
160	159	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
161	158, 160	eqnetrd 2999	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0)
162		fveq2 6834	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘0𝑝))
163	162, 12	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 0)
164	163	necon3i 2964	. . . . . . . . . . . . 13 ⊢ ((deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0 → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
165	161, 164	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
166		eqid 2736	. . . . . . . . . . . . 13 ⊢ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘(Xp ∘f − (ℂ × {𝑧})))
167		eqid 2736	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
168	166, 167	dgrmul 26232	. . . . . . . . . . . 12 ⊢ ((((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
169	68, 165, 32, 90, 168	syl22anc 838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
170	157, 169	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
171	9, 170	eqtrid 2783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	156, 171	fveq12d 6841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))))
173		eqid 2736	. . . . . . . . . 10 ⊢ (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = (coeff‘(Xp ∘f − (ℂ × {𝑧})))
174		eqid 2736	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
175	173, 174, 166, 167	coemulhi 26215	. . . . . . . . 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 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
177	158	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
178		ssid 3956	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
179		plyid 26170	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180	178, 100, 179	mp2an 692	. . . . . . . . . . . . . 14 ⊢ Xp ∈ (Poly‘ℂ)
181		plyconst 26167	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182	178, 50, 181	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (coeff‘Xp) = (coeff‘Xp)
184		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185	183, 184	coesub 26218	. . . . . . . . . . . . . 14 ⊢ ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
186	180, 182, 185	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
187	186	fveq1d 6836	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188		1nn0 12417	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
189	183	coef3 26193	. . . . . . . . . . . . . . . . 17 ⊢ (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190		ffn 6662	. . . . . . . . . . . . . . . . 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 26193	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194		ffn 6662	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195	182, 193, 194	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196		nn0ex 12407	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ∈ V
197	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ0 ∈ V)
198		inidm 4179	. . . . . . . . . . . . . . 15 ⊢ (ℕ0 ∩ ℕ0) = ℕ0
199		coeidp 26225	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
200	199	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
201		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
202	201	iftruei 4486	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
203	200, 202	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204		0lt1 11659	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
205		0re 11134	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
206		1re 11132	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
207	205, 206	ltnlei 11254	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
208	204, 207	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
209	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210		0dgr 26206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212	211	breq2d 5110	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213	208, 212	mtbiri 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215	184, 214	dgrub 26195	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
216	215	3expia 1121	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
217	182, 216	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
218	217	necon1bd 2950	. . . . . . . . . . . . . . . 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 7633	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
221	188, 220	mpan2 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222		1m0e1 12261	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
223	221, 222	eqtrdi 2787	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224	187, 223	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = 1)
225	177, 224	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = 1)
226	225	oveq1d 7373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227	174	coef3 26193	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
228	32, 227	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229	228, 34	ffvelcdmd 7030	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230	229	mullidd 11150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231	226, 230	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232	172, 176, 231	3eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233	154, 232	oveq12d 7376	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234	233	negeqd 11374	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235	153, 234	eqtr4d 2774	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
236	133, 235	oveq12d 7376	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
237	50	negcld 11479	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
238		nnm1nn0 12442	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
239	3, 238	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ0)
240	239	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ0)
241	228, 240	ffvelcdmd 7030	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242	232, 229	eqeltrd 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
243	9, 27	dgreq0 26227	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
244	43, 243	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
245	244	necon3bid 2976	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴‘𝑁) ≠ 0))
246	82, 245	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
247	241, 242, 246	divcld 11917	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
248	237, 247	negdid 11505	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
249	237, 242	mulcld 11152	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
250	249, 241, 242, 246	divdird 11955	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
251		nnm1nn0 12442	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
252	5, 251	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ0)
253	252	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ0)
254	173, 174	coemul 26213	. . . . . . . . 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 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256	156	fveq1d 6836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257		1e0p1 12649	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
258	257	oveq2i 7369	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
259	258	sumeq1i 15620	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260		0nn0 12416	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
261		nn0uz 12789	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
262	260, 261	eleqtri 2834	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ≥‘0)
263	262	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ≥‘0))
264	258	eleq2i 2828	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265	173	coef3 26193	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
266	68, 265	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267		elfznn0 13536	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268		ffvelcdm 7026	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269	266, 267, 268	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
270	2	oveq1d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271		pncan 11386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272	101, 100, 271	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273	270, 272	eqtr3d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
274	273	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
275	3	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
276	274, 275	eqeltrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
277		nnuz 12790	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
278	276, 277	eleqtrdi 2846	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ≥‘1))
279		fzss2 13480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280	278, 279	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281	280	sselda 3933	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282		fznn0sub 13472	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283		ffvelcdm 7026	. . . . . . . . . . . . . . 15 ⊢ (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
284	228, 282, 283	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
285	281, 284	syldan 591	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
286	269, 285	mulcld 11152	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
287	264, 286	sylan2br 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
288		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
289	288, 257	eqtr4di 2789	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
290	289	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
291	289	oveq2d 7374	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292	291	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293	290, 292	oveq12d 7376	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294	263, 287, 293	fsump1 15679	. . . . . . . . . 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 2783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296		eldifn 4084	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297	296	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298		eldifi 4083	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299		elfznn0 13536	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300	298, 299	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301	173, 166	dgrub 26195	. . . . . . . . . . . . . . . . 17 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))))
302	301	3expia 1121	. . . . . . . . . . . . . . . 16 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
303	68, 300, 302	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
304		elfzuz 13436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘0))
305	298, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ≥‘0))
306	305	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ≥‘0))
307		1z 12521	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
308		elfz5 13432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309	306, 307, 308	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310	158	breq2d 5110	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
311	310	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
312	309, 311	bitr4d 282	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧})))))
313	303, 312	sylibrd 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
314	313	necon1bd 2950	. . . . . . . . . . . . 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 7373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
317	298, 284	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
318	317	mul02d 11331	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319	316, 318	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320		fzfid 13896	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321	280, 286, 319, 320	fsumss 15648	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322		0z 12499	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
323	186	fveq1d 6836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324		coeidp 26225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325	159	nesymi 2989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
326	325	iffalsei 4489	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
327	324, 326	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328	327	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329	184	coefv0 26209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
330	182, 329	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
331		0cn 11124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
332		vex 3444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
333	332	fvconst2 7150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
334	331, 333	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
335	330, 334	eqtr3di 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336	335	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337	192, 195, 197, 197, 198, 328, 336	ofval 7633	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338	260, 337	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339		df-neg 11367	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
340	338, 339	eqtr4di 2789	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341	323, 340	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = -𝑧)
342	274	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343	102	subid1d 11481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
344	342, 343, 31	3eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345	344	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346	345, 232	eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
347	341, 346	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
348	347, 249	eqeltrd 2836	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0))
350		oveq2 7366	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351	350	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352	349, 351	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353	352	fsum1 15670	. . . . . . . . . . . 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 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
355	354, 347	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
356	274	fvoveq1d 7380	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357	224, 356	oveq12d 7376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358	241	mullidd 11150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359	357, 358	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360	355, 359	oveq12d 7376	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361	295, 321, 360	3eqtr3rd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362	255, 256, 361	3eqtr4rd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363	362	oveq1d 7373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
364	237, 242, 246	divcan4d 11923	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
365	364	oveq1d 7373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
366	250, 363, 365	3eqtr3rd 2780	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
367	366	negeqd 11374	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	248, 367	eqtr3d 2773	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
369	128, 236, 368	3eqtrd 2775	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
370	25, 369	exlimddv 1936	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  Vcvv 3440   ∖ cdif 3898   ∪ cun 3899   ∩ cin 3900   ⊆ wss 3901  ∅c0 4285  ifcif 4479  {csn 4580   class class class wbr 5098   × cxp 5622  ^◡ccnv 5623  dom cdm 5624   “ cima 5627   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  (class class class)co 7358   ∘_f cof 7620  Fincfn 8883  ℂcc 11024  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   · cmul 11031   < clt 11166   ≤ cle 11167   − cmin 11364  -cneg 11365   / cdiv 11794  ℕcn 12145  ℕ₀cn0 12401  ℤcz 12488  ℤ_≥cuz 12751  ...cfz 13423  ♯chash 14253  Σcsu 15609  0_𝑝c0p 25626  Polycply 26145  X_pcidp 26146  coeffccoe 26147  degcdgr 26148   quot cquot 26254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-inf2 9550  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103  ax-pre-sup 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-oadd 8401  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9813  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-2 12208  df-3 12209  df-n0 12402  df-xnn0 12475  df-z 12489  df-uz 12752  df-rp 12906  df-fz 13424  df-fzo 13571  df-fl 13712  df-seq 13925  df-exp 13985  df-hash 14254  df-cj 15022  df-re 15023  df-im 15024  df-sqrt 15158  df-abs 15159  df-clim 15411  df-rlim 15412  df-sum 15610  df-0p 25627  df-ply 26149  df-idp 26150  df-coe 26151  df-dgr 26152  df-quot 26255

This theorem is referenced by:  vieta1  26276