vieta1lem2

Description: Lemma for vieta1 : inductive step. Let z be a root of F . Then F = ( Xp - z ) x. Q for some Q by the factor theorem, and Q is a degree- D polynomial, so by the induction hypothesis sum_ x e. (`' Q " 0 ) x = -u ( coeff `Q )( D - 1 ) / ( coeffQ )D , so sum_ x e. R x = z - ( coeffQ )` ` ( D - 1 ) / ( coeffQ )D . Now the coefficients of F are A( D + 1 ) = ( coeffQ )D and AD = sum_ k e. ( 0 ... D ) ( coeffXp - z )k x. ( coeffQ ) ` `( D - k ) , which works out to -u z x. ( coeffQ )D + ( coeffQ )( D - 1 ) , so putting it all together we have sum_ x e. R x = -u AD / A( D + 1 ) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	vieta1.1	$⊢ A = coeff (F)$
	vieta1.2	$⊢ N = \deg (F)$
	vieta1.3	$⊢ R = F^{-1} [\{0\}]$
	vieta1.4	$⊢ φ \to F \in Poly (S)$
	vieta1.5	$⊢ φ \to \|R\| = N$
	vieta1lem.6	$⊢ φ \to D \in ℕ$
	vieta1lem.7	$⊢ φ \to D + 1 = N$
	vieta1lem.8	$⊢ φ \to \forall f \in Poly (ℂ) ((D = \deg (f) \land \|f^{-1} [\{0\}]\| = \deg (f)) \to \sum_{x \in f^{-1} [\{0\}]} x = - \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))})$
	vieta1lem.9	$⊢ Q = F quot (X^{p} -_{f} (ℂ \times \{z\}))$
Assertion	vieta1lem2	$⊢ φ \to \sum_{x \in R} x = - \frac{A (N - 1)}{A (N)}$

Proof

Step	Hyp	Ref	Expression
1		vieta1.1	$⊢ A = coeff (F)$
2		vieta1.2	$⊢ N = \deg (F)$
3		vieta1.3	$⊢ R = F^{-1} [\{0\}]$
4		vieta1.4	$⊢ φ \to F \in Poly (S)$
5		vieta1.5	$⊢ φ \to \|R\| = N$
6		vieta1lem.6	$⊢ φ \to D \in ℕ$
7		vieta1lem.7	$⊢ φ \to D + 1 = N$
8		vieta1lem.8	$⊢ φ \to \forall f \in Poly (ℂ) ((D = \deg (f) \land \|f^{-1} [\{0\}]\| = \deg (f)) \to \sum_{x \in f^{-1} [\{0\}]} x = - \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))})$
9		vieta1lem.9	$⊢ Q = F quot (X^{p} -_{f} (ℂ \times \{z\}))$
10	6	peano2nnd	$⊢ φ \to D + 1 \in ℕ$
11	7 10	eqeltrrd	$⊢ φ \to N \in ℕ$
12	11	nnne0d	$⊢ φ \to N \neq 0$
13	5 12	eqnetrd	$⊢ φ \to \|R\| \neq 0$
14	2 12	eqnetrrid	$⊢ φ \to \deg (F) \neq 0$
15		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
16		dgr0	$⊢ \deg (0_{𝑝}) = 0$
17	15 16	eqtrdi	$⊢ F = 0_{𝑝} \to \deg (F) = 0$
18	17	necon3i	$⊢ \deg (F) \neq 0 \to F \neq 0_{𝑝}$
19	14 18	syl	$⊢ φ \to F \neq 0_{𝑝}$
20	3	fta1	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to (R \in Fin \land \|R\| \leq \deg (F))$
21	4 19 20	syl2anc	$⊢ φ \to (R \in Fin \land \|R\| \leq \deg (F))$
22	21	simpld	$⊢ φ \to R \in Fin$
23		hasheq0	$⊢ R \in Fin \to (\|R\| = 0 \leftrightarrow R = \emptyset)$
24	22 23	syl	$⊢ φ \to (\|R\| = 0 \leftrightarrow R = \emptyset)$
25	24	necon3bid	$⊢ φ \to (\|R\| \neq 0 \leftrightarrow R \neq \emptyset)$
26	13 25	mpbid	$⊢ φ \to R \neq \emptyset$
27		n0	$⊢ R \neq \emptyset \leftrightarrow \exists z z \in R$
28	26 27	sylib	$⊢ φ \to \exists z z \in R$
29		incom	$⊢ \{z\} \cap Q^{-1} [\{0\}] = Q^{-1} [\{0\}] \cap \{z\}$
30	1 2 3 4 5 6 7 8 9	vieta1lem1	$⊢ (φ \land z \in R) \to (Q \in Poly (ℂ) \land D = \deg (Q))$
31	30	simprd	$⊢ (φ \land z \in R) \to D = \deg (Q)$
32	30	simpld	$⊢ (φ \land z \in R) \to Q \in Poly (ℂ)$
33		dgrcl	$⊢ Q \in Poly (ℂ) \to \deg (Q) \in ℕ_{0}$
34	32 33	syl	$⊢ (φ \land z \in R) \to \deg (Q) \in ℕ_{0}$
35	34	nn0red	$⊢ (φ \land z \in R) \to \deg (Q) \in ℝ$
36	31 35	eqeltrd	$⊢ (φ \land z \in R) \to D \in ℝ$
37	36	ltp1d	$⊢ (φ \land z \in R) \to D < D + 1$
38	36 37	gtned	$⊢ (φ \land z \in R) \to D + 1 \neq D$
39		snssi	$⊢ z \in Q^{-1} [\{0\}] \to \{z\} \subseteq Q^{-1} [\{0\}]$
40		ssequn1	$⊢ \{z\} \subseteq Q^{-1} [\{0\}] \leftrightarrow \{z\} \cup Q^{-1} [\{0\}] = Q^{-1} [\{0\}]$
41	39 40	sylib	$⊢ z \in Q^{-1} [\{0\}] \to \{z\} \cup Q^{-1} [\{0\}] = Q^{-1} [\{0\}]$
42	41	fveq2d	$⊢ z \in Q^{-1} [\{0\}] \to \|\{z\} \cup Q^{-1} [\{0\}]\| = \|Q^{-1} [\{0\}]\|$
43	4	adantr	$⊢ (φ \land z \in R) \to F \in Poly (S)$
44		cnvimass	$⊢ F^{-1} [\{0\}] \subseteq dom F$
45	3 44	eqsstri	$⊢ R \subseteq dom F$
46		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
47		fdm	$⊢ F : ℂ ⟶ ℂ \to dom F = ℂ$
48	4 46 47	3syl	$⊢ φ \to dom F = ℂ$
49	45 48	sseqtrid	$⊢ φ \to R \subseteq ℂ$
50	49	sselda	$⊢ (φ \land z \in R) \to z \in ℂ$
51	3	eleq2i	$⊢ z \in R \leftrightarrow z \in F^{-1} [\{0\}]$
52		ffn	$⊢ F : ℂ ⟶ ℂ \to F Fn ℂ$
53		fniniseg	$⊢ F Fn ℂ \to (z \in F^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land F (z) = 0))$
54	4 46 52 53	4syl	$⊢ φ \to (z \in F^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land F (z) = 0))$
55	51 54	syl5bb	$⊢ φ \to (z \in R \leftrightarrow (z \in ℂ \land F (z) = 0))$
56	55	simplbda	$⊢ (φ \land z \in R) \to F (z) = 0$
57		eqid	$⊢ X^{p} -_{f} (ℂ \times \{z\}) = X^{p} -_{f} (ℂ \times \{z\})$
58	57	facth	$⊢ (F \in Poly (S) \land z \in ℂ \land F (z) = 0) \to F = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} (F quot (X^{p} -_{f} (ℂ \times \{z\})))$
59	43 50 56 58	syl3anc	$⊢ (φ \land z \in R) \to F = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} (F quot (X^{p} -_{f} (ℂ \times \{z\})))$
60	9	oveq2i	$⊢ (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} (F quot (X^{p} -_{f} (ℂ \times \{z\})))$
61	59 60	eqtr4di	$⊢ (φ \land z \in R) \to F = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q$
62	61	cnveqd	$⊢ (φ \land z \in R) \to F^{-1} = {((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)}^{-1}$
63	62	imaeq1d	$⊢ (φ \land z \in R) \to F^{-1} [\{0\}] = {((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)}^{-1} [\{0\}]$
64	3 63	eqtrid	$⊢ (φ \land z \in R) \to R = {((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)}^{-1} [\{0\}]$
65		cnex	$⊢ ℂ \in V$
66	57	plyremlem	$⊢ z \in ℂ \to (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land \deg (X^{p} -_{f} (ℂ \times \{z\})) = 1 \land {(X^{p} -_{f} (ℂ \times \{z\}))}^{-1} [\{0\}] = \{z\})$
67	50 66	syl	$⊢ (φ \land z \in R) \to (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land \deg (X^{p} -_{f} (ℂ \times \{z\})) = 1 \land {(X^{p} -_{f} (ℂ \times \{z\}))}^{-1} [\{0\}] = \{z\})$
68	67	simp1d	$⊢ (φ \land z \in R) \to X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ)$
69		plyf	$⊢ X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \to (X^{p} -_{f} (ℂ \times \{z\})) : ℂ ⟶ ℂ$
70	68 69	syl	$⊢ (φ \land z \in R) \to (X^{p} -_{f} (ℂ \times \{z\})) : ℂ ⟶ ℂ$
71		plyf	$⊢ Q \in Poly (ℂ) \to Q : ℂ ⟶ ℂ$
72	32 71	syl	$⊢ (φ \land z \in R) \to Q : ℂ ⟶ ℂ$
73		ofmulrt	$⊢ (ℂ \in V \land (X^{p} -_{f} (ℂ \times \{z\})) : ℂ ⟶ ℂ \land Q : ℂ ⟶ ℂ) \to {((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)}^{-1} [\{0\}] = {(X^{p} -_{f} (ℂ \times \{z\}))}^{-1} [\{0\}] \cup Q^{-1} [\{0\}]$
74	65 70 72 73	mp3an2i	$⊢ (φ \land z \in R) \to {((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)}^{-1} [\{0\}] = {(X^{p} -_{f} (ℂ \times \{z\}))}^{-1} [\{0\}] \cup Q^{-1} [\{0\}]$
75	67	simp3d	$⊢ (φ \land z \in R) \to {(X^{p} -_{f} (ℂ \times \{z\}))}^{-1} [\{0\}] = \{z\}$
76	75	uneq1d	$⊢ (φ \land z \in R) \to {(X^{p} -_{f} (ℂ \times \{z\}))}^{-1} [\{0\}] \cup Q^{-1} [\{0\}] = \{z\} \cup Q^{-1} [\{0\}]$
77	64 74 76	3eqtrd	$⊢ (φ \land z \in R) \to R = \{z\} \cup Q^{-1} [\{0\}]$
78	77	fveq2d	$⊢ (φ \land z \in R) \to \|R\| = \|\{z\} \cup Q^{-1} [\{0\}]\|$
79	5 7	eqtr4d	$⊢ φ \to \|R\| = D + 1$
80	79	adantr	$⊢ (φ \land z \in R) \to \|R\| = D + 1$
81	78 80	eqtr3d	$⊢ (φ \land z \in R) \to \|\{z\} \cup Q^{-1} [\{0\}]\| = D + 1$
82	19	adantr	$⊢ (φ \land z \in R) \to F \neq 0_{𝑝}$
83	61 82	eqnetrrd	$⊢ (φ \land z \in R) \to (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q \neq 0_{𝑝}$
84		plymul0or	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land Q \in Poly (ℂ)) \to ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q = 0_{𝑝} \leftrightarrow (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝}))$
85	68 32 84	syl2anc	$⊢ (φ \land z \in R) \to ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q = 0_{𝑝} \leftrightarrow (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝}))$
86	85	necon3abid	$⊢ (φ \land z \in R) \to ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q \neq 0_{𝑝} \leftrightarrow \neg (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝}))$
87	83 86	mpbid	$⊢ (φ \land z \in R) \to \neg (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝})$
88		neanior	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝} \land Q \neq 0_{𝑝}) \leftrightarrow \neg (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝})$
89	87 88	sylibr	$⊢ (φ \land z \in R) \to (X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝} \land Q \neq 0_{𝑝})$
90	89	simprd	$⊢ (φ \land z \in R) \to Q \neq 0_{𝑝}$
91		eqid	$⊢ Q^{-1} [\{0\}] = Q^{-1} [\{0\}]$
92	91	fta1	$⊢ (Q \in Poly (ℂ) \land Q \neq 0_{𝑝}) \to (Q^{-1} [\{0\}] \in Fin \land \|Q^{-1} [\{0\}]\| \leq \deg (Q))$
93	32 90 92	syl2anc	$⊢ (φ \land z \in R) \to (Q^{-1} [\{0\}] \in Fin \land \|Q^{-1} [\{0\}]\| \leq \deg (Q))$
94	93	simprd	$⊢ (φ \land z \in R) \to \|Q^{-1} [\{0\}]\| \leq \deg (Q)$
95	94 31	breqtrrd	$⊢ (φ \land z \in R) \to \|Q^{-1} [\{0\}]\| \leq D$
96		snfi	$⊢ \{z\} \in Fin$
97	93	simpld	$⊢ (φ \land z \in R) \to Q^{-1} [\{0\}] \in Fin$
98		hashun2	$⊢ (\{z\} \in Fin \land Q^{-1} [\{0\}] \in Fin) \to \|\{z\} \cup Q^{-1} [\{0\}]\| \leq \|\{z\}\| + \|Q^{-1} [\{0\}]\|$
99	96 97 98	sylancr	$⊢ (φ \land z \in R) \to \|\{z\} \cup Q^{-1} [\{0\}]\| \leq \|\{z\}\| + \|Q^{-1} [\{0\}]\|$
100		ax-1cn	$⊢ 1 \in ℂ$
101	6	nncnd	$⊢ φ \to D \in ℂ$
102	101	adantr	$⊢ (φ \land z \in R) \to D \in ℂ$
103		addcom	$⊢ (1 \in ℂ \land D \in ℂ) \to 1 + D = D + 1$
104	100 102 103	sylancr	$⊢ (φ \land z \in R) \to 1 + D = D + 1$
105	81 104	eqtr4d	$⊢ (φ \land z \in R) \to \|\{z\} \cup Q^{-1} [\{0\}]\| = 1 + D$
106		hashsng	$⊢ z \in R \to \|\{z\}\| = 1$
107	106	adantl	$⊢ (φ \land z \in R) \to \|\{z\}\| = 1$
108	107	oveq1d	$⊢ (φ \land z \in R) \to \|\{z\}\| + \|Q^{-1} [\{0\}]\| = 1 + \|Q^{-1} [\{0\}]\|$
109	99 105 108	3brtr3d	$⊢ (φ \land z \in R) \to 1 + D \leq 1 + \|Q^{-1} [\{0\}]\|$
110		hashcl	$⊢ Q^{-1} [\{0\}] \in Fin \to \|Q^{-1} [\{0\}]\| \in ℕ_{0}$
111	97 110	syl	$⊢ (φ \land z \in R) \to \|Q^{-1} [\{0\}]\| \in ℕ_{0}$
112	111	nn0red	$⊢ (φ \land z \in R) \to \|Q^{-1} [\{0\}]\| \in ℝ$
113		1red	$⊢ (φ \land z \in R) \to 1 \in ℝ$
114	36 112 113	leadd2d	$⊢ (φ \land z \in R) \to (D \leq \|Q^{-1} [\{0\}]\| \leftrightarrow 1 + D \leq 1 + \|Q^{-1} [\{0\}]\|)$
115	109 114	mpbird	$⊢ (φ \land z \in R) \to D \leq \|Q^{-1} [\{0\}]\|$
116	112 36	letri3d	$⊢ (φ \land z \in R) \to (\|Q^{-1} [\{0\}]\| = D \leftrightarrow (\|Q^{-1} [\{0\}]\| \leq D \land D \leq \|Q^{-1} [\{0\}]\|))$
117	95 115 116	mpbir2and	$⊢ (φ \land z \in R) \to \|Q^{-1} [\{0\}]\| = D$
118	81 117	eqeq12d	$⊢ (φ \land z \in R) \to (\|\{z\} \cup Q^{-1} [\{0\}]\| = \|Q^{-1} [\{0\}]\| \leftrightarrow D + 1 = D)$
119	42 118	syl5ib	$⊢ (φ \land z \in R) \to (z \in Q^{-1} [\{0\}] \to D + 1 = D)$
120	119	necon3ad	$⊢ (φ \land z \in R) \to (D + 1 \neq D \to \neg z \in Q^{-1} [\{0\}])$
121	38 120	mpd	$⊢ (φ \land z \in R) \to \neg z \in Q^{-1} [\{0\}]$
122		disjsn	$⊢ Q^{-1} [\{0\}] \cap \{z\} = \emptyset \leftrightarrow \neg z \in Q^{-1} [\{0\}]$
123	121 122	sylibr	$⊢ (φ \land z \in R) \to Q^{-1} [\{0\}] \cap \{z\} = \emptyset$
124	29 123	eqtrid	$⊢ (φ \land z \in R) \to \{z\} \cap Q^{-1} [\{0\}] = \emptyset$
125	22	adantr	$⊢ (φ \land z \in R) \to R \in Fin$
126	49	adantr	$⊢ (φ \land z \in R) \to R \subseteq ℂ$
127	126	sselda	$⊢ ((φ \land z \in R) \land x \in R) \to x \in ℂ$
128	124 77 125 127	fsumsplit	$⊢ (φ \land z \in R) \to \sum_{x \in R} x = \sum_{x \in \{z\}} x + \sum_{x \in Q^{-1} [\{0\}]} x$
129		id	$⊢ x = z \to x = z$
130	129	sumsn	$⊢ (z \in ℂ \land z \in ℂ) \to \sum_{x \in \{z\}} x = z$
131	50 50 130	syl2anc	$⊢ (φ \land z \in R) \to \sum_{x \in \{z\}} x = z$
132	50	negnegd	$⊢ (φ \land z \in R) \to - (- z) = z$
133	131 132	eqtr4d	$⊢ (φ \land z \in R) \to \sum_{x \in \{z\}} x = - (- z)$
134	117 31	eqtrd	$⊢ (φ \land z \in R) \to \|Q^{-1} [\{0\}]\| = \deg (Q)$
135		fveq2	$⊢ f = Q \to \deg (f) = \deg (Q)$
136	135	eqeq2d	$⊢ f = Q \to (D = \deg (f) \leftrightarrow D = \deg (Q))$
137		cnveq	$⊢ f = Q \to f^{-1} = Q^{-1}$
138	137	imaeq1d	$⊢ f = Q \to f^{-1} [\{0\}] = Q^{-1} [\{0\}]$
139	138	fveq2d	$⊢ f = Q \to \|f^{-1} [\{0\}]\| = \|Q^{-1} [\{0\}]\|$
140	139 135	eqeq12d	$⊢ f = Q \to (\|f^{-1} [\{0\}]\| = \deg (f) \leftrightarrow \|Q^{-1} [\{0\}]\| = \deg (Q))$
141	136 140	anbi12d	$⊢ f = Q \to ((D = \deg (f) \land \|f^{-1} [\{0\}]\| = \deg (f)) \leftrightarrow (D = \deg (Q) \land \|Q^{-1} [\{0\}]\| = \deg (Q)))$
142	138	sumeq1d	$⊢ f = Q \to \sum_{x \in f^{-1} [\{0\}]} x = \sum_{x \in Q^{-1} [\{0\}]} x$
143		fveq2	$⊢ f = Q \to coeff (f) = coeff (Q)$
144	135	oveq1d	$⊢ f = Q \to \deg (f) - 1 = \deg (Q) - 1$
145	143 144	fveq12d	$⊢ f = Q \to coeff (f) (\deg (f) - 1) = coeff (Q) (\deg (Q) - 1)$
146	143 135	fveq12d	$⊢ f = Q \to coeff (f) (\deg (f)) = coeff (Q) (\deg (Q))$
147	145 146	oveq12d	$⊢ f = Q \to \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))} = \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))}$
148	147	negeqd	$⊢ f = Q \to - \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))} = - \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))}$
149	142 148	eqeq12d	$⊢ f = Q \to (\sum_{x \in f^{-1} [\{0\}]} x = - \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))} \leftrightarrow \sum_{x \in Q^{-1} [\{0\}]} x = - \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))})$
150	141 149	imbi12d	$⊢ f = Q \to (((D = \deg (f) \land \|f^{-1} [\{0\}]\| = \deg (f)) \to \sum_{x \in f^{-1} [\{0\}]} x = - \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))}) \leftrightarrow ((D = \deg (Q) \land \|Q^{-1} [\{0\}]\| = \deg (Q)) \to \sum_{x \in Q^{-1} [\{0\}]} x = - \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))}))$
151	8	adantr	$⊢ (φ \land z \in R) \to \forall f \in Poly (ℂ) ((D = \deg (f) \land \|f^{-1} [\{0\}]\| = \deg (f)) \to \sum_{x \in f^{-1} [\{0\}]} x = - \frac{coeff (f) (\deg (f) - 1)}{coeff (f) (\deg (f))})$
152	150 151 32	rspcdva	$⊢ (φ \land z \in R) \to ((D = \deg (Q) \land \|Q^{-1} [\{0\}]\| = \deg (Q)) \to \sum_{x \in Q^{-1} [\{0\}]} x = - \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))})$
153	31 134 152	mp2and	$⊢ (φ \land z \in R) \to \sum_{x \in Q^{-1} [\{0\}]} x = - \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))}$
154	31	fvoveq1d	$⊢ (φ \land z \in R) \to coeff (Q) (D - 1) = coeff (Q) (\deg (Q) - 1)$
155	61	fveq2d	$⊢ (φ \land z \in R) \to coeff (F) = coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)$
156	1 155	eqtrid	$⊢ (φ \land z \in R) \to A = coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)$
157	61	fveq2d	$⊢ (φ \land z \in R) \to \deg (F) = \deg ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)$
158	67	simp2d	$⊢ (φ \land z \in R) \to \deg (X^{p} -_{f} (ℂ \times \{z\})) = 1$
159		ax-1ne0	$⊢ 1 \neq 0$
160	159	a1i	$⊢ (φ \land z \in R) \to 1 \neq 0$
161	158 160	eqnetrd	$⊢ (φ \land z \in R) \to \deg (X^{p} -_{f} (ℂ \times \{z\})) \neq 0$
162		fveq2	$⊢ X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \to \deg (X^{p} -_{f} (ℂ \times \{z\})) = \deg (0_{𝑝})$
163	162 16	eqtrdi	$⊢ X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \to \deg (X^{p} -_{f} (ℂ \times \{z\})) = 0$
164	163	necon3i	$⊢ \deg (X^{p} -_{f} (ℂ \times \{z\})) \neq 0 \to X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝}$
165	161 164	syl	$⊢ (φ \land z \in R) \to X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝}$
166		eqid	$⊢ \deg (X^{p} -_{f} (ℂ \times \{z\})) = \deg (X^{p} -_{f} (ℂ \times \{z\}))$
167		eqid	$⊢ \deg (Q) = \deg (Q)$
168	166 167	dgrmul	$⊢ ((X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝}) \land (Q \in Poly (ℂ) \land Q \neq 0_{𝑝})) \to \deg ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) = \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)$
169	68 165 32 90 168	syl22anc	$⊢ (φ \land z \in R) \to \deg ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) = \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)$
170	157 169	eqtrd	$⊢ (φ \land z \in R) \to \deg (F) = \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)$
171	2 170	eqtrid	$⊢ (φ \land z \in R) \to N = \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)$
172	156 171	fveq12d	$⊢ (φ \land z \in R) \to A (N) = coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) (\deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q))$
173		eqid	$⊢ coeff (X^{p} -_{f} (ℂ \times \{z\})) = coeff (X^{p} -_{f} (ℂ \times \{z\}))$
174		eqid	$⊢ coeff (Q) = coeff (Q)$
175	173 174 166 167	coemulhi	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land Q \in Poly (ℂ)) \to coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) (\deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (\deg (X^{p} -_{f} (ℂ \times \{z\}))) coeff (Q) (\deg (Q))$
176	68 32 175	syl2anc	$⊢ (φ \land z \in R) \to coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) (\deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (\deg (X^{p} -_{f} (ℂ \times \{z\}))) coeff (Q) (\deg (Q))$
177	158	fveq2d	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (\deg (X^{p} -_{f} (ℂ \times \{z\}))) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (1)$
178		ssid	$⊢ ℂ \subseteq ℂ$
179		plyid	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to X^{p} \in Poly (ℂ)$
180	178 100 179	mp2an	$⊢ X^{p} \in Poly (ℂ)$
181		plyconst	$⊢ (ℂ \subseteq ℂ \land z \in ℂ) \to ℂ \times \{z\} \in Poly (ℂ)$
182	178 50 181	sylancr	$⊢ (φ \land z \in R) \to ℂ \times \{z\} \in Poly (ℂ)$
183		eqid	$⊢ coeff (X^{p}) = coeff (X^{p})$
184		eqid	$⊢ coeff (ℂ \times \{z\}) = coeff (ℂ \times \{z\})$
185	183 184	coesub	$⊢ (X^{p} \in Poly (ℂ) \land ℂ \times \{z\} \in Poly (ℂ)) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) = coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})$
186	180 182 185	sylancr	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) = coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})$
187	186	fveq1d	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) = (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (1)$
188		1nn0	$⊢ 1 \in ℕ_{0}$
189	183	coef3	$⊢ X^{p} \in Poly (ℂ) \to coeff (X^{p}) : ℕ_{0} ⟶ ℂ$
190		ffn	$⊢ coeff (X^{p}) : ℕ_{0} ⟶ ℂ \to coeff (X^{p}) Fn ℕ_{0}$
191	180 189 190	mp2b	$⊢ coeff (X^{p}) Fn ℕ_{0}$
192	191	a1i	$⊢ (φ \land z \in R) \to coeff (X^{p}) Fn ℕ_{0}$
193	184	coef3	$⊢ ℂ \times \{z\} \in Poly (ℂ) \to coeff (ℂ \times \{z\}) : ℕ_{0} ⟶ ℂ$
194		ffn	$⊢ coeff (ℂ \times \{z\}) : ℕ_{0} ⟶ ℂ \to coeff (ℂ \times \{z\}) Fn ℕ_{0}$
195	182 193 194	3syl	$⊢ (φ \land z \in R) \to coeff (ℂ \times \{z\}) Fn ℕ_{0}$
196		nn0ex	$⊢ ℕ_{0} \in V$
197	196	a1i	$⊢ (φ \land z \in R) \to ℕ_{0} \in V$
198		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
199		coeidp	$⊢ 1 \in ℕ_{0} \to coeff (X^{p}) (1) = if (1 = 1, 1, 0)$
200	199	adantl	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to coeff (X^{p}) (1) = if (1 = 1, 1, 0)$
201		eqid	$⊢ 1 = 1$
202	201	iftruei	$⊢ if (1 = 1, 1, 0) = 1$
203	200 202	eqtrdi	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to coeff (X^{p}) (1) = 1$
204		0lt1	$⊢ 0 < 1$
205		0re	$⊢ 0 \in ℝ$
206		1re	$⊢ 1 \in ℝ$
207	205 206	ltnlei	$⊢ 0 < 1 \leftrightarrow \neg 1 \leq 0$
208	204 207	mpbi	$⊢ \neg 1 \leq 0$
209	50	adantr	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to z \in ℂ$
210		0dgr	$⊢ z \in ℂ \to \deg (ℂ \times \{z\}) = 0$
211	209 210	syl	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to \deg (ℂ \times \{z\}) = 0$
212	211	breq2d	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to (1 \leq \deg (ℂ \times \{z\}) \leftrightarrow 1 \leq 0)$
213	208 212	mtbiri	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to \neg 1 \leq \deg (ℂ \times \{z\})$
214		eqid	$⊢ \deg (ℂ \times \{z\}) = \deg (ℂ \times \{z\})$
215	184 214	dgrub	$⊢ (ℂ \times \{z\} \in Poly (ℂ) \land 1 \in ℕ_{0} \land coeff (ℂ \times \{z\}) (1) \neq 0) \to 1 \leq \deg (ℂ \times \{z\})$
216	215	3expia	$⊢ (ℂ \times \{z\} \in Poly (ℂ) \land 1 \in ℕ_{0}) \to (coeff (ℂ \times \{z\}) (1) \neq 0 \to 1 \leq \deg (ℂ \times \{z\}))$
217	182 216	sylan	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to (coeff (ℂ \times \{z\}) (1) \neq 0 \to 1 \leq \deg (ℂ \times \{z\}))$
218	217	necon1bd	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to (\neg 1 \leq \deg (ℂ \times \{z\}) \to coeff (ℂ \times \{z\}) (1) = 0)$
219	213 218	mpd	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to coeff (ℂ \times \{z\}) (1) = 0$
220	192 195 197 197 198 203 219	ofval	$⊢ ((φ \land z \in R) \land 1 \in ℕ_{0}) \to (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (1) = 1 - 0$
221	188 220	mpan2	$⊢ (φ \land z \in R) \to (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (1) = 1 - 0$
222		1m0e1	$⊢ 1 - 0 = 1$
223	221 222	eqtrdi	$⊢ (φ \land z \in R) \to (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (1) = 1$
224	187 223	eqtrd	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) = 1$
225	177 224	eqtrd	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (\deg (X^{p} -_{f} (ℂ \times \{z\}))) = 1$
226	225	oveq1d	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (\deg (X^{p} -_{f} (ℂ \times \{z\}))) coeff (Q) (\deg (Q)) = 1 coeff (Q) (\deg (Q))$
227	174	coef3	$⊢ Q \in Poly (ℂ) \to coeff (Q) : ℕ_{0} ⟶ ℂ$
228	32 227	syl	$⊢ (φ \land z \in R) \to coeff (Q) : ℕ_{0} ⟶ ℂ$
229	228 34	ffvelrnd	$⊢ (φ \land z \in R) \to coeff (Q) (\deg (Q)) \in ℂ$
230	229	mulid2d	$⊢ (φ \land z \in R) \to 1 coeff (Q) (\deg (Q)) = coeff (Q) (\deg (Q))$
231	226 230	eqtrd	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (\deg (X^{p} -_{f} (ℂ \times \{z\}))) coeff (Q) (\deg (Q)) = coeff (Q) (\deg (Q))$
232	172 176 231	3eqtrd	$⊢ (φ \land z \in R) \to A (N) = coeff (Q) (\deg (Q))$
233	154 232	oveq12d	$⊢ (φ \land z \in R) \to \frac{coeff (Q) (D - 1)}{A (N)} = \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))}$
234	233	negeqd	$⊢ (φ \land z \in R) \to - \frac{coeff (Q) (D - 1)}{A (N)} = - \frac{coeff (Q) (\deg (Q) - 1)}{coeff (Q) (\deg (Q))}$
235	153 234	eqtr4d	$⊢ (φ \land z \in R) \to \sum_{x \in Q^{-1} [\{0\}]} x = - \frac{coeff (Q) (D - 1)}{A (N)}$
236	133 235	oveq12d	$⊢ (φ \land z \in R) \to \sum_{x \in \{z\}} x + \sum_{x \in Q^{-1} [\{0\}]} x = - (- z) + (- \frac{coeff (Q) (D - 1)}{A (N)})$
237	50	negcld	$⊢ (φ \land z \in R) \to - z \in ℂ$
238		nnm1nn0	$⊢ D \in ℕ \to D - 1 \in ℕ_{0}$
239	6 238	syl	$⊢ φ \to D - 1 \in ℕ_{0}$
240	239	adantr	$⊢ (φ \land z \in R) \to D - 1 \in ℕ_{0}$
241	228 240	ffvelrnd	$⊢ (φ \land z \in R) \to coeff (Q) (D - 1) \in ℂ$
242	232 229	eqeltrd	$⊢ (φ \land z \in R) \to A (N) \in ℂ$
243	2 1	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
244	43 243	syl	$⊢ (φ \land z \in R) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
245	244	necon3bid	$⊢ (φ \land z \in R) \to (F \neq 0_{𝑝} \leftrightarrow A (N) \neq 0)$
246	82 245	mpbid	$⊢ (φ \land z \in R) \to A (N) \neq 0$
247	241 242 246	divcld	$⊢ (φ \land z \in R) \to \frac{coeff (Q) (D - 1)}{A (N)} \in ℂ$
248	237 247	negdid	$⊢ (φ \land z \in R) \to - (- z + (\frac{coeff (Q) (D - 1)}{A (N)})) = - (- z) + (- \frac{coeff (Q) (D - 1)}{A (N)})$
249	237 242	mulcld	$⊢ (φ \land z \in R) \to (- z) A (N) \in ℂ$
250	249 241 242 246	divdird	$⊢ (φ \land z \in R) \to \frac{(- z) A (N) + coeff (Q) (D - 1)}{A (N)} = (\frac{(- z) A (N)}{A (N)}) + (\frac{coeff (Q) (D - 1)}{A (N)})$
251		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
252	11 251	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
253	252	adantr	$⊢ (φ \land z \in R) \to N - 1 \in ℕ_{0}$
254	173 174	coemul	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land Q \in Poly (ℂ) \land N - 1 \in ℕ_{0}) \to coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) (N - 1) = \sum_{k = 0}^{N - 1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k)$
255	68 32 253 254	syl3anc	$⊢ (φ \land z \in R) \to coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) (N - 1) = \sum_{k = 0}^{N - 1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k)$
256	156	fveq1d	$⊢ (φ \land z \in R) \to A (N - 1) = coeff ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) (N - 1)$
257		1e0p1	$⊢ 1 = 0 + 1$
258	257	oveq2i	$⊢ (0 \dots 1) = (0 \dots 0 + 1)$
259	258	sumeq1i	$⊢ \sum_{k = 0}^{1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = \sum_{k = 0}^{0 + 1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k)$
260		0nn0	$⊢ 0 \in ℕ_{0}$
261		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
262	260 261	eleqtri	$⊢ 0 \in ℤ_{\geq 0}$
263	262	a1i	$⊢ (φ \land z \in R) \to 0 \in ℤ_{\geq 0}$
264	258	eleq2i	$⊢ k \in (0 \dots 1) \leftrightarrow k \in (0 \dots 0 + 1)$
265	173	coef3	$⊢ X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) : ℕ_{0} ⟶ ℂ$
266	68 265	syl	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) : ℕ_{0} ⟶ ℂ$
267		elfznn0	$⊢ k \in (0 \dots 1) \to k \in ℕ_{0}$
268		ffvelrn	$⊢ (coeff (X^{p} -_{f} (ℂ \times \{z\})) : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) \in ℂ$
269	266 267 268	syl2an	$⊢ ((φ \land z \in R) \land k \in (0 \dots 1)) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) \in ℂ$
270	7	oveq1d	$⊢ φ \to D + 1 - 1 = N - 1$
271		pncan	$⊢ (D \in ℂ \land 1 \in ℂ) \to D + 1 - 1 = D$
272	101 100 271	sylancl	$⊢ φ \to D + 1 - 1 = D$
273	270 272	eqtr3d	$⊢ φ \to N - 1 = D$
274	273	adantr	$⊢ (φ \land z \in R) \to N - 1 = D$
275	6	adantr	$⊢ (φ \land z \in R) \to D \in ℕ$
276	274 275	eqeltrd	$⊢ (φ \land z \in R) \to N - 1 \in ℕ$
277		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
278	276 277	eleqtrdi	$⊢ (φ \land z \in R) \to N - 1 \in ℤ_{\geq 1}$
279		fzss2	$⊢ N - 1 \in ℤ_{\geq 1} \to (0 \dots 1) \subseteq (0 \dots N - 1)$
280	278 279	syl	$⊢ (φ \land z \in R) \to (0 \dots 1) \subseteq (0 \dots N - 1)$
281	280	sselda	$⊢ ((φ \land z \in R) \land k \in (0 \dots 1)) \to k \in (0 \dots N - 1)$
282		fznn0sub	$⊢ k \in (0 \dots N - 1) \to N - 1 - k \in ℕ_{0}$
283		ffvelrn	$⊢ (coeff (Q) : ℕ_{0} ⟶ ℂ \land N - 1 - k \in ℕ_{0}) \to coeff (Q) (N - 1 - k) \in ℂ$
284	228 282 283	syl2an	$⊢ ((φ \land z \in R) \land k \in (0 \dots N - 1)) \to coeff (Q) (N - 1 - k) \in ℂ$
285	281 284	syldan	$⊢ ((φ \land z \in R) \land k \in (0 \dots 1)) \to coeff (Q) (N - 1 - k) \in ℂ$
286	269 285	mulcld	$⊢ ((φ \land z \in R) \land k \in (0 \dots 1)) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) \in ℂ$
287	264 286	sylan2br	$⊢ ((φ \land z \in R) \land k \in (0 \dots 0 + 1)) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) \in ℂ$
288		id	$⊢ k = 0 + 1 \to k = 0 + 1$
289	288 257	eqtr4di	$⊢ k = 0 + 1 \to k = 1$
290	289	fveq2d	$⊢ k = 0 + 1 \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (1)$
291	289	oveq2d	$⊢ k = 0 + 1 \to N - 1 - k = N - 1 - 1$
292	291	fveq2d	$⊢ k = 0 + 1 \to coeff (Q) (N - 1 - k) = coeff (Q) (N - 1 - 1)$
293	290 292	oveq12d	$⊢ k = 0 + 1 \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) coeff (Q) (N - 1 - 1)$
294	263 287 293	fsump1	$⊢ (φ \land z \in R) \to \sum_{k = 0}^{0 + 1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = \sum_{k = 0}^{0} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) + coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) coeff (Q) (N - 1 - 1)$
295	259 294	eqtrid	$⊢ (φ \land z \in R) \to \sum_{k = 0}^{1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = \sum_{k = 0}^{0} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) + coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) coeff (Q) (N - 1 - 1)$
296		eldifn	$⊢ k \in ((0 \dots N - 1) ∖ (0 \dots 1)) \to \neg k \in (0 \dots 1)$
297	296	adantl	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to \neg k \in (0 \dots 1)$
298		eldifi	$⊢ k \in ((0 \dots N - 1) ∖ (0 \dots 1)) \to k \in (0 \dots N - 1)$
299		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
300	298 299	syl	$⊢ k \in ((0 \dots N - 1) ∖ (0 \dots 1)) \to k \in ℕ_{0}$
301	173 166	dgrub	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land k \in ℕ_{0} \land coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) \neq 0) \to k \leq \deg (X^{p} -_{f} (ℂ \times \{z\}))$
302	301	3expia	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land k \in ℕ_{0}) \to (coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) \neq 0 \to k \leq \deg (X^{p} -_{f} (ℂ \times \{z\})))$
303	68 300 302	syl2an	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to (coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) \neq 0 \to k \leq \deg (X^{p} -_{f} (ℂ \times \{z\})))$
304		elfzuz	$⊢ k \in (0 \dots N - 1) \to k \in ℤ_{\geq 0}$
305	298 304	syl	$⊢ k \in ((0 \dots N - 1) ∖ (0 \dots 1)) \to k \in ℤ_{\geq 0}$
306	305	adantl	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to k \in ℤ_{\geq 0}$
307		1z	$⊢ 1 \in ℤ$
308		elfz5	$⊢ (k \in ℤ_{\geq 0} \land 1 \in ℤ) \to (k \in (0 \dots 1) \leftrightarrow k \leq 1)$
309	306 307 308	sylancl	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to (k \in (0 \dots 1) \leftrightarrow k \leq 1)$
310	158	breq2d	$⊢ (φ \land z \in R) \to (k \leq \deg (X^{p} -_{f} (ℂ \times \{z\})) \leftrightarrow k \leq 1)$
311	310	adantr	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to (k \leq \deg (X^{p} -_{f} (ℂ \times \{z\})) \leftrightarrow k \leq 1)$
312	309 311	bitr4d	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to (k \in (0 \dots 1) \leftrightarrow k \leq \deg (X^{p} -_{f} (ℂ \times \{z\})))$
313	303 312	sylibrd	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to (coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) \neq 0 \to k \in (0 \dots 1))$
314	313	necon1bd	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to (\neg k \in (0 \dots 1) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) = 0)$
315	297 314	mpd	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) = 0$
316	315	oveq1d	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = 0 \cdot coeff (Q) (N - 1 - k)$
317	298 284	sylan2	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to coeff (Q) (N - 1 - k) \in ℂ$
318	317	mul02d	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to 0 \cdot coeff (Q) (N - 1 - k) = 0$
319	316 318	eqtrd	$⊢ ((φ \land z \in R) \land k \in ((0 \dots N - 1) ∖ (0 \dots 1))) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = 0$
320		fzfid	$⊢ (φ \land z \in R) \to (0 \dots N - 1) \in Fin$
321	280 286 319 320	fsumss	$⊢ (φ \land z \in R) \to \sum_{k = 0}^{1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = \sum_{k = 0}^{N - 1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k)$
322		0z	$⊢ 0 \in ℤ$
323	186	fveq1d	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) = (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (0)$
324		coeidp	$⊢ 0 \in ℕ_{0} \to coeff (X^{p}) (0) = if (0 = 1, 1, 0)$
325	159	nesymi	$⊢ \neg 0 = 1$
326	325	iffalsei	$⊢ if (0 = 1, 1, 0) = 0$
327	324 326	eqtrdi	$⊢ 0 \in ℕ_{0} \to coeff (X^{p}) (0) = 0$
328	327	adantl	$⊢ ((φ \land z \in R) \land 0 \in ℕ_{0}) \to coeff (X^{p}) (0) = 0$
329	184	coefv0	$⊢ ℂ \times \{z\} \in Poly (ℂ) \to (ℂ \times \{z\}) (0) = coeff (ℂ \times \{z\}) (0)$
330	182 329	syl	$⊢ (φ \land z \in R) \to (ℂ \times \{z\}) (0) = coeff (ℂ \times \{z\}) (0)$
331		0cn	$⊢ 0 \in ℂ$
332		vex	$⊢ z \in V$
333	332	fvconst2	$⊢ 0 \in ℂ \to (ℂ \times \{z\}) (0) = z$
334	331 333	ax-mp	$⊢ (ℂ \times \{z\}) (0) = z$
335	330 334	eqtr3di	$⊢ (φ \land z \in R) \to coeff (ℂ \times \{z\}) (0) = z$
336	335	adantr	$⊢ ((φ \land z \in R) \land 0 \in ℕ_{0}) \to coeff (ℂ \times \{z\}) (0) = z$
337	192 195 197 197 198 328 336	ofval	$⊢ ((φ \land z \in R) \land 0 \in ℕ_{0}) \to (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (0) = 0 - z$
338	260 337	mpan2	$⊢ (φ \land z \in R) \to (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (0) = 0 - z$
339		df-neg	$⊢ - z = 0 - z$
340	338 339	eqtr4di	$⊢ (φ \land z \in R) \to (coeff (X^{p}) -_{f} coeff (ℂ \times \{z\})) (0) = - z$
341	323 340	eqtrd	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) = - z$
342	274	oveq1d	$⊢ (φ \land z \in R) \to N - 1 - 0 = D - 0$
343	102	subid1d	$⊢ (φ \land z \in R) \to D - 0 = D$
344	342 343 31	3eqtrd	$⊢ (φ \land z \in R) \to N - 1 - 0 = \deg (Q)$
345	344	fveq2d	$⊢ (φ \land z \in R) \to coeff (Q) (N - 1 - 0) = coeff (Q) (\deg (Q))$
346	345 232	eqtr4d	$⊢ (φ \land z \in R) \to coeff (Q) (N - 1 - 0) = A (N)$
347	341 346	oveq12d	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) coeff (Q) (N - 1 - 0) = (- z) A (N)$
348	347 249	eqeltrd	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) coeff (Q) (N - 1 - 0) \in ℂ$
349		fveq2	$⊢ k = 0 \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (0)$
350		oveq2	$⊢ k = 0 \to N - 1 - k = N - 1 - 0$
351	350	fveq2d	$⊢ k = 0 \to coeff (Q) (N - 1 - k) = coeff (Q) (N - 1 - 0)$
352	349 351	oveq12d	$⊢ k = 0 \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) coeff (Q) (N - 1 - 0)$
353	352	fsum1	$⊢ (0 \in ℤ \land coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) coeff (Q) (N - 1 - 0) \in ℂ) \to \sum_{k = 0}^{0} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) coeff (Q) (N - 1 - 0)$
354	322 348 353	sylancr	$⊢ (φ \land z \in R) \to \sum_{k = 0}^{0} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = coeff (X^{p} -_{f} (ℂ \times \{z\})) (0) coeff (Q) (N - 1 - 0)$
355	354 347	eqtrd	$⊢ (φ \land z \in R) \to \sum_{k = 0}^{0} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) = (- z) A (N)$
356	274	fvoveq1d	$⊢ (φ \land z \in R) \to coeff (Q) (N - 1 - 1) = coeff (Q) (D - 1)$
357	224 356	oveq12d	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) coeff (Q) (N - 1 - 1) = 1 coeff (Q) (D - 1)$
358	241	mulid2d	$⊢ (φ \land z \in R) \to 1 coeff (Q) (D - 1) = coeff (Q) (D - 1)$
359	357 358	eqtrd	$⊢ (φ \land z \in R) \to coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) coeff (Q) (N - 1 - 1) = coeff (Q) (D - 1)$
360	355 359	oveq12d	$⊢ (φ \land z \in R) \to \sum_{k = 0}^{0} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k) + coeff (X^{p} -_{f} (ℂ \times \{z\})) (1) coeff (Q) (N - 1 - 1) = (- z) A (N) + coeff (Q) (D - 1)$
361	295 321 360	3eqtr3rd	$⊢ (φ \land z \in R) \to (- z) A (N) + coeff (Q) (D - 1) = \sum_{k = 0}^{N - 1} coeff (X^{p} -_{f} (ℂ \times \{z\})) (k) coeff (Q) (N - 1 - k)$
362	255 256 361	3eqtr4rd	$⊢ (φ \land z \in R) \to (- z) A (N) + coeff (Q) (D - 1) = A (N - 1)$
363	362	oveq1d	$⊢ (φ \land z \in R) \to \frac{(- z) A (N) + coeff (Q) (D - 1)}{A (N)} = \frac{A (N - 1)}{A (N)}$
364	237 242 246	divcan4d	$⊢ (φ \land z \in R) \to \frac{(- z) A (N)}{A (N)} = - z$
365	364	oveq1d	$⊢ (φ \land z \in R) \to (\frac{(- z) A (N)}{A (N)}) + (\frac{coeff (Q) (D - 1)}{A (N)}) = - z + (\frac{coeff (Q) (D - 1)}{A (N)})$
366	250 363 365	3eqtr3rd	$⊢ (φ \land z \in R) \to - z + (\frac{coeff (Q) (D - 1)}{A (N)}) = \frac{A (N - 1)}{A (N)}$
367	366	negeqd	$⊢ (φ \land z \in R) \to - (- z + (\frac{coeff (Q) (D - 1)}{A (N)})) = - \frac{A (N - 1)}{A (N)}$
368	248 367	eqtr3d	$⊢ (φ \land z \in R) \to - (- z) + (- \frac{coeff (Q) (D - 1)}{A (N)}) = - \frac{A (N - 1)}{A (N)}$
369	128 236 368	3eqtrd	$⊢ (φ \land z \in R) \to \sum_{x \in R} x = - \frac{A (N - 1)}{A (N)}$
370	28 369	exlimddv	$⊢ φ \to \sum_{x \in R} x = - \frac{A (N - 1)}{A (N)}$

Metamath Proof Explorer

Theorem vieta1lem2

Proof