Theorem vieta1lem2 26219

Description: Lemma for vieta1 26220: 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 12203	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 1) ∈ ℕ)
5	2, 4	eqeltrrd 2829	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnne0d 12236	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
7	1, 6	eqnetrd 2992	. . . 4 ⊢ (𝜑 → (♯‘𝑅) ≠ 0)
8		vieta1.4	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
9		vieta1.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
10	9, 6	eqnetrrid 3000	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝐹) ≠ 0)
11		fveq2 6858	. . . . . . . . . . 11 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12		dgr0 26168	. . . . . . . . . . 11 ⊢ (deg‘0𝑝) = 0
13	11, 12	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
14	13	necon3i 2957	. . . . . . . . 9 ⊢ ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
15	10, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ≠ 0𝑝)
16		vieta1.3	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 “ {0})
17	16	fta1 26216	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
18	8, 15, 17	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
19	18	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Fin)
20		hasheq0 14328	. . . . . 6 ⊢ (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
21	19, 20	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
22	21	necon3bid 2969	. . . 4 ⊢ (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
23	7, 22	mpbid 232	. . 3 ⊢ (𝜑 → 𝑅 ≠ ∅)
24		n0 4316	. . 3 ⊢ (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑅)
25	23, 24	sylib 218	. 2 ⊢ (𝜑 → ∃𝑧 𝑧 ∈ 𝑅)
26		incom 4172	. . . . 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 26218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
31	30	simprd 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄))
32	30	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈ (Poly‘ℂ))
33		dgrcl 26138	. . . . . . . . . . 11 ⊢ (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℕ0)
35	34	nn0red 12504	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℝ)
36	31, 35	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℝ)
37	36	ltp1d 12113	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 < (𝐷 + 1))
38	36, 37	gtned 11309	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) ≠ 𝐷)
39		snssi 4772	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → {𝑧} ⊆ (◡𝑄 “ {0}))
40		ssequn1 4149	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ (◡𝑄 “ {0}) ↔ ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
41	39, 40	sylib 218	. . . . . . . . . 10 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → ({𝑧} ∪ (◡𝑄 “ {0})) = (◡𝑄 “ {0}))
42	41	fveq2d 6862	. . . . . . . . 9 ⊢ (𝑧 ∈ (◡𝑄 “ {0}) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})))
43	8	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆))
44		cnvimass 6053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐹 “ {0}) ⊆ dom 𝐹
45	16, 44	eqsstri 3993	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑅 ⊆ dom 𝐹
46		plyf 26103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47		fdm 6697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
48	8, 46, 47	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = ℂ)
49	45, 48	sseqtrid 3989	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑅 ⊆ ℂ)
50	49	sselda 3946	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ)
51	16	eleq2i 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◡𝐹 “ {0}))
52		ffn 6688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53		fniniseg 7032	. . . . . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (Xp ∘f − (ℂ × {𝑧})) = (Xp ∘f − (ℂ × {𝑧}))
58	57	facth 26214	. . . . . . . . . . . . . . . . . 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 7398	. . . . . . . . . . . . . . . . 17 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xp ∘f − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))))
61	59, 60	eqtr4di 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
62	61	cnveqd 5839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ◡𝐹 = ◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))
63	62	imaeq1d 6030	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝐹 “ {0}) = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
64	16, 63	eqtrid 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = (◡((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65		cnex 11149	. . . . . . . . . . . . . 14 ⊢ ℂ ∈ V
66	57	plyremlem 26212	. . . . . . . . . . . . . . . . 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 26103	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})):ℂ⟶ℂ)
71		plyf 26103	. . . . . . . . . . . . . . 15 ⊢ (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
72	32, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄:ℂ⟶ℂ)
73		ofmulrt 26189	. . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡(Xp ∘f − (ℂ × {𝑧})) “ {0}) ∪ (◡𝑄 “ {0})) = ({𝑧} ∪ (◡𝑄 “ {0})))
77	64, 74, 76	3eqtrd 2768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 = ({𝑧} ∪ (◡𝑄 “ {0})))
78	77	fveq2d 6862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (◡𝑄 “ {0}))))
79	1, 2	eqtr4d 2767	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑅) = (𝐷 + 1))
80	79	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘𝑅) = (𝐷 + 1))
81	78, 80	eqtr3d 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (𝐷 + 1))
82	15	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠ 0𝑝)
83	61, 82	eqnetrrd 2993	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84		plymul0or 26188	. . . . . . . . . . . . . . . . . . 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 2961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
87	83, 86	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88		neanior 3018	. . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . 15 ⊢ (◡𝑄 “ {0}) = (◡𝑄 “ {0})
92	91	fta1 26216	. . . . . . . . . . . . . 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 5135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ≤ 𝐷)
96		snfi 9014	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
97	93	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (◡𝑄 “ {0}) ∈ Fin)
98		hashun2 14348	. . . . . . . . . . . . . 14 ⊢ (({𝑧} ∈ Fin ∧ (◡𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
99	96, 97, 98	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))))
100		ax-1cn 11126	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
101	3	nncnd 12202	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ)
103		addcom 11360	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104	100, 102, 103	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1))
105	81, 104	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (1 + 𝐷))
106		hashsng 14334	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑅 → (♯‘{𝑧}) = 1)
107	106	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘{𝑧}) = 1)
108	107	oveq1d 7402	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘{𝑧}) + (♯‘(◡𝑄 “ {0}))) = (1 + (♯‘(◡𝑄 “ {0}))))
109	99, 105, 108	3brtr3d 5138	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0}))))
110		hashcl 14321	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑄 “ {0}) ∈ Fin → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
111	97, 110	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℕ0)
112	111	nn0red 12504	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) ∈ ℝ)
113		1red 11175	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℝ)
114	36, 112, 113	leadd2d 11773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 ≤ (♯‘(◡𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(◡𝑄 “ {0})))))
115	109, 114	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ≤ (♯‘(◡𝑄 “ {0})))
116	112, 36	letri3d 11316	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘(◡𝑄 “ {0})) = 𝐷 ↔ ((♯‘(◡𝑄 “ {0})) ≤ 𝐷 ∧ 𝐷 ≤ (♯‘(◡𝑄 “ {0})))))
117	95, 115, 116	mpbir2and 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = 𝐷)
118	81, 117	eqeq12d 2745	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((♯‘({𝑧} ∪ (◡𝑄 “ {0}))) = (♯‘(◡𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
119	42, 118	imbitrid 244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑧 ∈ (◡𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120	119	necon3ad 2938	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (◡𝑄 “ {0})))
121	38, 120	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ 𝑧 ∈ (◡𝑄 “ {0}))
122		disjsn 4675	. . . . . 6 ⊢ (((◡𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (◡𝑄 “ {0}))
123	121, 122	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((◡𝑄 “ {0}) ∩ {𝑧}) = ∅)
124	26, 123	eqtrid 2776	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ({𝑧} ∩ (◡𝑄 “ {0})) = ∅)
125	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ∈ Fin)
126	49	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑅 ⊆ ℂ)
127	126	sselda 3946	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ ℂ)
128	124, 77, 125, 127	fsumsplit 15707	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥))
129		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
130	129	sumsn 15712	. . . . . 6 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
131	50, 50, 130	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
132	50	negnegd 11524	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → --𝑧 = 𝑧)
133	131, 132	eqtr4d 2767	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134	117, 31	eqtrd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))
135		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136	135	eqeq2d 2740	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137		cnveq 5837	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ◡𝑓 = ◡𝑄)
138	137	imaeq1d 6030	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → (◡𝑓 “ {0}) = (◡𝑄 “ {0}))
139	138	fveq2d 6862	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (♯‘(◡𝑓 “ {0})) = (♯‘(◡𝑄 “ {0})))
140	139, 135	eqeq12d 2745	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → ((♯‘(◡𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄)))
141	136, 140	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(◡𝑄 “ {0})) = (deg‘𝑄))))
142	138	sumeq1d 15666	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = Σ𝑥 ∈ (◡𝑄 “ {0})𝑥)
143		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144	135	oveq1d 7402	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145	143, 144	fveq12d 6865	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146	143, 135	fveq12d 6865	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147	145, 146	oveq12d 7405	. . . . . . . . . 10 ⊢ (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148	147	negeqd 11415	. . . . . . . . 9 ⊢ (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149	142, 148	eqeq12d 2745	. . . . . . . 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 3589	. . . . . 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 7409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
155	61	fveq2d 6862	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝐹) = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
156	27, 155	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐴 = (coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
157	61	fveq2d 6862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄)))
158	67	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 1)
159		ax-1ne0 11137	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
160	159	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0)
161	158, 160	eqnetrd 2992	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0)
162		fveq2 6858	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘0𝑝))
163	162, 12	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ ((Xp ∘f − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp ∘f − (ℂ × {𝑧}))) = 0)
164	163	necon3i 2957	. . . . . . . . . . . . 13 ⊢ ((deg‘(Xp ∘f − (ℂ × {𝑧}))) ≠ 0 → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
165	161, 164	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp ∘f − (ℂ × {𝑧})) ≠ 0𝑝)
166		eqid 2729	. . . . . . . . . . . . 13 ⊢ (deg‘(Xp ∘f − (ℂ × {𝑧}))) = (deg‘(Xp ∘f − (ℂ × {𝑧})))
167		eqid 2729	. . . . . . . . . . . . 13 ⊢ (deg‘𝑄) = (deg‘𝑄)
168	166, 167	dgrmul 26176	. . . . . . . . . . . 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 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
171	9, 170	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑁 = ((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄)))
172	156, 171	fveq12d 6865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xp ∘f − (ℂ × {𝑧}))) + (deg‘𝑄))))
173		eqid 2729	. . . . . . . . . 10 ⊢ (coeff‘(Xp ∘f − (ℂ × {𝑧}))) = (coeff‘(Xp ∘f − (ℂ × {𝑧})))
174		eqid 2729	. . . . . . . . . 10 ⊢ (coeff‘𝑄) = (coeff‘𝑄)
175	173, 174, 166, 167	coemulhi 26159	. . . . . . . . 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 6862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
178		ssid 3969	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
179		plyid 26114	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180	178, 100, 179	mp2an 692	. . . . . . . . . . . . . 14 ⊢ Xp ∈ (Poly‘ℂ)
181		plyconst 26111	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182	178, 50, 181	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (coeff‘Xp) = (coeff‘Xp)
184		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185	183, 184	coesub 26162	. . . . . . . . . . . . . 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 6860	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188		1nn0 12458	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
189	183	coef3 26137	. . . . . . . . . . . . . . . . 17 ⊢ (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190		ffn 6688	. . . . . . . . . . . . . . . . 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 26137	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194		ffn 6688	. . . . . . . . . . . . . . . 16 ⊢ ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195	182, 193, 194	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196		nn0ex 12448	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ∈ V
197	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ℕ0 ∈ V)
198		inidm 4190	. . . . . . . . . . . . . . 15 ⊢ (ℕ0 ∩ ℕ0) = ℕ0
199		coeidp 26169	. . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . 17 ⊢ 1 = 1
202	201	iftruei 4495	. . . . . . . . . . . . . . . 16 ⊢ if(1 = 1, 1, 0) = 1
203	200, 202	eqtrdi 2780	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204		0lt1 11700	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 1
205		0re 11176	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
206		1re 11174	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
207	205, 206	ltnlei 11295	. . . . . . . . . . . . . . . . . 18 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
208	204, 207	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1 ≤ 0
209	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210		0dgr 26150	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212	211	breq2d 5119	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213	208, 212	mtbiri 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215	184, 214	dgrub 26139	. . . . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . . . . 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 7664	. . . . . . . . . . . . . 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 12302	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
223	221, 222	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224	187, 223	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) = 1)
225	177, 224	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) = 1)
226	225	oveq1d 7402	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227	174	coef3 26137	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
228	32, 227	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229	228, 34	ffvelcdmd 7057	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230	229	mullidd 11192	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231	226, 230	eqtrd 2764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘(deg‘(Xp ∘f − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232	172, 176, 231	3eqtrd 2768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233	154, 232	oveq12d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234	233	negeqd 11415	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235	153, 234	eqtr4d 2767	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ (◡𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)))
236	133, 235	oveq12d 7405	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (◡𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
237	50	negcld 11520	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -𝑧 ∈ ℂ)
238		nnm1nn0 12483	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
239	3, 238	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ0)
240	239	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 1) ∈ ℕ0)
241	228, 240	ffvelcdmd 7057	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242	232, 229	eqeltrd 2828	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ∈ ℂ)
243	9, 27	dgreq0 26171	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
244	43, 243	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
245	244	necon3bid 2969	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴‘𝑁) ≠ 0))
246	82, 245	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘𝑁) ≠ 0)
247	241, 242, 246	divcld 11958	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁)) ∈ ℂ)
248	237, 247	negdid 11546	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
249	237, 242	mulcld 11194	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 · (𝐴‘𝑁)) ∈ ℂ)
250	249, 241, 242, 246	divdird 11996	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
251		nnm1nn0 12483	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
252	5, 251	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ0)
253	252	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ0)
254	173, 174	coemul 26157	. . . . . . . . 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 6860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp ∘f − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257		1e0p1 12691	. . . . . . . . . . . 12 ⊢ 1 = (0 + 1)
258	257	oveq2i 7398	. . . . . . . . . . 11 ⊢ (0...1) = (0...(0 + 1))
259	258	sumeq1i 15663	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260		0nn0 12457	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
261		nn0uz 12835	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
262	260, 261	eleqtri 2826	. . . . . . . . . . . 12 ⊢ 0 ∈ (ℤ≥‘0)
263	262	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 0 ∈ (ℤ≥‘0))
264	258	eleq2i 2820	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265	173	coef3 26137	. . . . . . . . . . . . . . 15 ⊢ ((Xp ∘f − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
266	68, 265	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267		elfznn0 13581	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268		ffvelcdm 7053	. . . . . . . . . . . . . 14 ⊢ (((coeff‘(Xp ∘f − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269	266, 267, 268	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
270	2	oveq1d 7402	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271		pncan 11427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272	101, 100, 271	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273	270, 272	eqtr3d 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) = 𝐷)
274	273	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) = 𝐷)
275	3	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℕ)
276	274, 275	eqeltrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ ℕ)
277		nnuz 12836	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ≥‘1)
278	276, 277	eleqtrdi 2838	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑁 − 1) ∈ (ℤ≥‘1))
279		fzss2 13525	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280	278, 279	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281	280	sselda 3946	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282		fznn0sub 13517	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283		ffvelcdm 7053	. . . . . . . . . . . . . . 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 11194	. . . . . . . . . . . 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 2782	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → 𝑘 = 1)
290	289	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1))
291	289	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292	291	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293	290, 292	oveq12d 7405	. . . . . . . . . . 11 ⊢ (𝑘 = (0 + 1) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294	263, 287, 293	fsump1 15722	. . . . . . . . . 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 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296		eldifn 4095	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297	296	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298		eldifi 4094	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299		elfznn0 13581	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300	298, 299	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301	173, 166	dgrub 26139	. . . . . . . . . . . . . . . . 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 13481	. . . . . . . . . . . . . . . . . . 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 12563	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
308		elfz5 13477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (ℤ≥‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309	306, 307, 308	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310	158	breq2d 5119	. . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . 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 7402	. . . . . . . . . . 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 11372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319	316, 318	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320		fzfid 13938	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321	280, 286, 319, 320	fsumss 15691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322		0z 12540	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
323	186	fveq1d 6860	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324		coeidp 26169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325	159	nesymi 2982	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 0 = 1
326	325	iffalsei 4498	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(0 = 1, 1, 0) = 0
327	324, 326	eqtrdi 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328	327	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329	184	coefv0 26153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
330	182, 329	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
331		0cn 11166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
332		vex 3451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
333	332	fvconst2 7178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
334	331, 333	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℂ × {𝑧})‘0) = 𝑧
335	330, 334	eqtr3di 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336	335	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337	192, 195, 197, 197, 198, 328, 336	ofval 7664	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338	260, 337	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339		df-neg 11408	. . . . . . . . . . . . . . . 16 ⊢ -𝑧 = (0 − 𝑧)
340	338, 339	eqtr4di 2782	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341	323, 340	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) = -𝑧)
342	274	oveq1d 7402	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343	102	subid1d 11522	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 − 0) = 𝐷)
344	342, 343, 31	3eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345	344	fveq2d 6862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346	345, 232	eqtr4d 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴‘𝑁))
347	341, 346	oveq12d 7405	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴‘𝑁)))
348	347, 249	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0))
350		oveq2 7395	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351	350	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352	349, 351	oveq12d 7405	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353	352	fsum1 15713	. . . . . . . . . . . 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 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴‘𝑁)))
356	274	fvoveq1d 7409	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357	224, 356	oveq12d 7405	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358	241	mullidd 11192	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359	357, 358	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360	355, 359	oveq12d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361	295, 321, 360	3eqtr3rd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp ∘f − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362	255, 256, 361	3eqtr4rd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363	362	oveq1d 7402	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴‘𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
364	237, 242, 246	divcan4d 11964	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) = -𝑧)
365	364	oveq1d 7402	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((-𝑧 · (𝐴‘𝑁)) / (𝐴‘𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))))
366	250, 363, 365	3eqtr3rd 2773	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
367	366	negeqd 11415	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
368	248, 367	eqtr3d 2766	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴‘𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
369	128, 236, 368	3eqtrd 2768	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
370	25, 369	exlimddv 1935	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  ifcif 4488  {csn 4589   class class class wbr 5107   × cxp 5636  ^◡ccnv 5637  dom cdm 5638   “ cima 5641   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387   ∘_f cof 7651  Fincfn 8918  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069   + caddc 11071   · cmul 11073   < clt 11208   ≤ cle 11209   − cmin 11405  -cneg 11406   / cdiv 11835  ℕcn 12186  ℕ₀cn0 12442  ℤcz 12529  ℤ_≥cuz 12793  ...cfz 13468  ♯chash 14295  Σcsu 15652  0_𝑝c0p 25570  Polycply 26089  X_pcidp 26090  coeffccoe 26091  degcdgr 26092   quot cquot 26198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-oadd 8438  df-er 8671  df-map 8801  df-pm 8802  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-sup 9393  df-inf 9394  df-oi 9463  df-dju 9854  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443  df-xnn0 12516  df-z 12530  df-uz 12794  df-rp 12952  df-fz 13469  df-fzo 13616  df-fl 13754  df-seq 13967  df-exp 14027  df-hash 14296  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-clim 15454  df-rlim 15455  df-sum 15653  df-0p 25571  df-ply 26093  df-idp 26094  df-coe 26095  df-dgr 26096  df-quot 26199

This theorem is referenced by:  vieta1  26220