Theorem vieta1lem2 26367

Description: Lemma for vieta1 26368: 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 12280	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2839	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 12313	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 3005	. . . 4 ⊢ (𝜑 → (♯‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	eqnetrrid 3013	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12		dgr0 26316	. . . . . . . . . . 11 ⊢ (deg‘0𝑝) = 0
13	11, 12	eqtrdi 2790	. . . . . . . . . 10 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 2970	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 “ {0})
17	16	fta1 26364	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 14398	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 2982	. . . 4 ⊢ (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 232	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 4358	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 218	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 4216	. . . . 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 26366	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 26286	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ0)
35	34	nn0red 12585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 12195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 11393	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4812	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → {𝑧} ⊆ (◡𝑄 “ {0}))
40		ssequn1 4195	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (◡𝑄 “ {0}) ↔ ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
41	39, 40	sylib 218	. . . . . . . . . 10 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
42	41	fveq2d 6910	. . . . . . . . 9 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})))
43	8	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 6101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 4029	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 26251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	sseqtrid 4047	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3994	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◡𝐹 “ {0}))
52		ffn 6736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 7079	. . . . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (Xp ∘f − (ℂ × {𝑧})) = (Xp ∘f − (ℂ × {𝑧}))
58	57	facth 26362	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
59	43, 50, 56, 58	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))))
60	29	oveq2i 7441	. . . . . . . . . . . . . . . . 17 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))))
61	59, 60	eqtr4di 2792	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
62	61	cnveqd 5888	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ◡𝐹 = ◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
63	62	imaeq1d 6078	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝐹 “ {0}) = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
64	16, 63	eqtrid 2786	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65		cnex 11233	. . . . . . . . . . . . . 14 ⊢ ℂ ∈ V
66	57	plyremlem 26360	. . . . . . . . . . . . . . . . 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 1141	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69		plyf 26251	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
71		plyf 26251	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
72	32, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
73		ofmulrt 26337	. . . . . . . . . . . . . 14 ⊢ ((ℂ ∈ V ∧ (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
74	65, 70, 72, 73	mp3an2i 1465	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})))
75	67	simp3d 1143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) = {𝑧})
76	75	uneq1d 4176	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})) = ({𝑧} ∪ (◡𝑄 “ {0})))
77	64, 74, 76	3eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (◡𝑄 “ {0})))
78	77	fveq2d 6910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (◡𝑄 “ {0}))))
79	1, 2	eqtr4d 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑅) = (𝐷 + 1))
80	79	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (𝐷 + 1))
81	78, 80	eqtr3d 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (𝐷 + 1))
82	15	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0𝑝)
83	61, 82	eqnetrrd 3006	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84		plymul0or 26336	. . . . . . . . . . . . . . . . . . 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 2974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
87	83, 86	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88		neanior 3032	. . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . 15 ⊢ (◡𝑄 “ {0}) = (◡𝑄 “ {0})
92	91	fta1 26364	. . . . . . . . . . . . . 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 5175	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ 𝐷)
96		snfi 9081	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
97	93	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝑄 “ {0}) ∈ Fin)
98		hashun2 14418	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (◡𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
99	96, 97, 98	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
100		ax-1cn 11210	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
101	3	nncnd 12279	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
103		addcom 11444	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104	100, 102, 103	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
105	81, 104	eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (1 + 𝐷))
106		hashsng 14404	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (♯‘{𝑧}) = 1)
107	106	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘{𝑧}) = 1)
108	107	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))) = (1 + (♯‘(◡𝑄 “ {0}))))
109	99, 105, 108	3brtr3d 5178	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0}))))
110		hashcl 14391	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑄 “ {0}) ∈ Fin → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
111	97, 110	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
112	111	nn0red 12585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℝ)
113		1red 11259	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
114	36, 112, 113	leadd2d 11855	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (♯‘(◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0})))))
115	109, 114	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (♯‘(◡𝑄 “ {0})))
116	112, 36	letri3d 11400	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘(◡𝑄 “ {0})) = 𝐷 ↔ ((♯‘(◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (♯‘(◡𝑄 “ {0})))))
117	95, 115, 116	mpbir2and 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = 𝐷)
118	81, 117	eqeq12d 2750	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
119	42, 118	imbitrid 244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120	119	necon3ad 2950	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (◡𝑄 “ {0})))
121	38, 120	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (◡𝑄 “ {0}))
122		disjsn 4715	. . . . . 6 ⊢ (((◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (◡𝑄 “ {0}))
123	121, 122	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
124	26, 123	eqtrid 2786	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (◡𝑄 “ {0})) = ∅)
125	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
126	49	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
127	126	sselda 3994	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
128	124, 77, 125, 127	fsumsplit 15773	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥))
129		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
130	129	sumsn 15778	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
131	50, 50, 130	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50	negnegd 11608	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
133	131, 132	eqtr4d 2777	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134	117, 31	eqtrd 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))
135		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136	135	eqeq2d 2745	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137		cnveq 5886	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ◡𝑓 = ◡𝑄)
138	137	imaeq1d 6078	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (◡𝑓 “ {0}) = (◡𝑄 “ {0}))
139	138	fveq2d 6910	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (♯‘(◡𝑓 “ {0})) = (♯‘(◡𝑄 “ {0})))
140	139, 135	eqeq12d 2750	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((♯‘(◡𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)))
141	136, 140	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))))
142	138	sumeq1d 15732	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (◡𝑄 “ {0})𝑥)
143		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144	135	oveq1d 7445	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145	143, 144	fveq12d 6913	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146	143, 135	fveq12d 6913	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147	145, 146	oveq12d 7448	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148	147	negeqd 11499	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149	142, 148	eqeq12d 2750	. . . . . . . 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 3622	. . . . . 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 7452	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
155	61	fveq2d 6910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
156	27, 155	eqtrid 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
157	61	fveq2d 6910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
158	67	simp2d 1142	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1)
159		ax-1ne0 11221	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
160	159	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
161	158, 160	eqnetrd 3005	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0)
162		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘0𝑝))
163	162, 12	eqtrdi 2790	. . . . . . . . . . . . . 14 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 0)
164	163	necon3i 2970	. . . . . . . . . . . . 13 ⊢ ((deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0 → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
165	161, 164	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
166		eqid 2734	. . . . . . . . . . . . 13 ⊢ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘(Xp ∘f − (ℂ × {𝑧})))
167		eqid 2734	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
168	166, 167	dgrmul 26324	. . . . . . . . . . . 12 ⊢ ((((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
169	68, 165, 32, 90, 168	syl22anc 839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
170	157, 169	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
171	9, 170	eqtrid 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	156, 171	fveq12d 6913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))))
173		eqid 2734	. . . . . . . . . 10 ⊢ (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = (coeff‘(Xp ∘f − (ℂ × {𝑧})))
174		eqid 2734	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
175	173, 174, 166, 167	coemulhi 26307	. . . . . . . . 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 6910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
178		ssid 4017	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
179		plyid 26262	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180	178, 100, 179	mp2an 692	. . . . . . . . . . . . . 14 ⊢ Xp ∈ (Poly‘ℂ)
181		plyconst 26259	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182	178, 50, 181	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (coeff‘Xp) = (coeff‘Xp)
184		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185	183, 184	coesub 26310	. . . . . . . . . . . . . 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 6908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188		1nn0 12539	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
189	183	coef3 26285	. . . . . . . . . . . . . . . . 17 ⊢ (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190		ffn 6736	. . . . . . . . . . . . . . . . 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 26285	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194		ffn 6736	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195	182, 193, 194	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196		nn0ex 12529	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ∈ V
197	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ0 ∈ V)
198		inidm 4234	. . . . . . . . . . . . . . 15 ⊢ (ℕ0 ∩ ℕ0) = ℕ0
199		coeidp 26317	. . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
202	201	iftruei 4537	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
203	200, 202	eqtrdi 2790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204		0lt1 11782	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
205		0re 11260	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
206		1re 11258	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
207	205, 206	ltnlei 11379	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
208	204, 207	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
209	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210		0dgr 26298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212	211	breq2d 5159	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213	208, 212	mtbiri 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214		eqid 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215	184, 214	dgrub 26287	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
216	215	3expia 1120	. . . . . . . . . . . . . . . . . 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 2955	. . . . . . . . . . . . . . . 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 7707	. . . . . . . . . . . . . 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 12384	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
223	221, 222	eqtrdi 2790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224	187, 223	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = 1)
225	177, 224	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = 1)
226	225	oveq1d 7445	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227	174	coef3 26285	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
228	32, 227	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229	228, 34	ffvelcdmd 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230	229	mullidd 11276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231	226, 230	eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232	172, 176, 231	3eqtrd 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233	154, 232	oveq12d 7448	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234	233	negeqd 11499	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235	153, 234	eqtr4d 2777	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
236	133, 235	oveq12d 7448	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
237	50	negcld 11604	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
238		nnm1nn0 12564	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
239	3, 238	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ0)
240	239	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ0)
241	228, 240	ffvelcdmd 7104	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242	232, 229	eqeltrd 2838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
243	9, 27	dgreq0 26319	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
244	43, 243	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
245	244	necon3bid 2982	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴‘𝑁) ≠ 0))
246	82, 245	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
247	241, 242, 246	divcld 12040	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
248	237, 247	negdid 11630	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
249	237, 242	mulcld 11278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
250	249, 241, 242, 246	divdird 12078	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
251		nnm1nn0 12564	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
252	5, 251	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ0)
253	252	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ0)
254	173, 174	coemul 26305	. . . . . . . . 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 1370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256	156	fveq1d 6908	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257		1e0p1 12772	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
258	257	oveq2i 7441	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
259	258	sumeq1i 15729	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260		0nn0 12538	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
261		nn0uz 12917	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
262	260, 261	eleqtri 2836	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ≥‘0)
263	262	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ≥‘0))
264	258	eleq2i 2830	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265	173	coef3 26285	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
266	68, 265	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267		elfznn0 13656	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268		ffvelcdm 7100	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269	266, 267, 268	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
270	2	oveq1d 7445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271		pncan 11511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272	101, 100, 271	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273	270, 272	eqtr3d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
274	273	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
275	3	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
276	274, 275	eqeltrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
277		nnuz 12918	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
278	276, 277	eleqtrdi 2848	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ≥‘1))
279		fzss2 13600	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280	278, 279	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281	280	sselda 3994	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282		fznn0sub 13592	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283		ffvelcdm 7100	. . . . . . . . . . . . . . 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 11278	. . . . . . . . . . . 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 2792	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
290	289	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
291	289	oveq2d 7446	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292	291	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293	290, 292	oveq12d 7448	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294	263, 287, 293	fsump1 15788	. . . . . . . . . 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 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296		eldifn 4141	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297	296	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298		eldifi 4140	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299		elfznn0 13656	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300	298, 299	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301	173, 166	dgrub 26287	. . . . . . . . . . . . . . . . 17 ⊢ (((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xp ∘f − (ℂ × {𝑧}))))
302	301	3expia 1120	. . . . . . . . . . . . . . . 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 13556	. . . . . . . . . . . . . . . . . . 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 12644	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
308		elfz5 13552	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309	306, 307, 308	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310	158	breq2d 5159	. . . . . . . . . . . . . . . . 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 2955	. . . . . . . . . . . . 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 7445	. . . . . . . . . . 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 11456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319	316, 318	eqtrd 2774	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320		fzfid 14010	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321	280, 286, 319, 320	fsumss 15757	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322		0z 12621	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
323	186	fveq1d 6908	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324		coeidp 26317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325	159	nesymi 2995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
326	325	iffalsei 4540	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
327	324, 326	eqtrdi 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328	327	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329	184	coefv0 26301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
330	182, 329	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
331		0cn 11250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
332		vex 3481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
333	332	fvconst2 7223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
334	331, 333	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
335	330, 334	eqtr3di 2789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336	335	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337	192, 195, 197, 197, 198, 328, 336	ofval 7707	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338	260, 337	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339		df-neg 11492	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
340	338, 339	eqtr4di 2792	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341	323, 340	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = -𝑧)
342	274	oveq1d 7445	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343	102	subid1d 11606	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
344	342, 343, 31	3eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345	344	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346	345, 232	eqtr4d 2777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
347	341, 346	oveq12d 7448	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
348	347, 249	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0))
350		oveq2 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351	350	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352	349, 351	oveq12d 7448	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353	352	fsum1 15779	. . . . . . . . . . . 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 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
356	274	fvoveq1d 7452	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357	224, 356	oveq12d 7448	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358	241	mullidd 11276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359	357, 358	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360	355, 359	oveq12d 7448	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361	295, 321, 360	3eqtr3rd 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362	255, 256, 361	3eqtr4rd 2785	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363	362	oveq1d 7445	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
364	237, 242, 246	divcan4d 12046	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
365	364	oveq1d 7445	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
366	250, 363, 365	3eqtr3rd 2783	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
367	366	negeqd 11499	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	248, 367	eqtr3d 2776	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
369	128, 236, 368	3eqtrd 2778	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
370	25, 369	exlimddv 1932	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  Vcvv 3477   ∖ cdif 3959   ∪ cun 3960   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  ifcif 4530  {csn 4630   class class class wbr 5147   × cxp 5686  ^◡ccnv 5687  dom cdm 5688   “ cima 5691   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430   ∘_f cof 7694  Fincfn 8983  ℂcc 11150  ℝcr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292   ≤ cle 11293   − cmin 11489  -cneg 11490   / cdiv 11917  ℕcn 12263  ℕ₀cn0 12523  ℤcz 12610  ℤ_≥cuz 12875  ...cfz 13543  ♯chash 14365  Σcsu 15718  0_𝑝c0p 25717  Polycply 26237  X_pcidp 26238  coeffccoe 26239  degcdgr 26240   quot cquot 26346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-rlim 15521  df-sum 15719  df-0p 25718  df-ply 26241  df-idp 26242  df-coe 26243  df-dgr 26244  df-quot 26347

This theorem is referenced by:  vieta1  26368