vieta1lem1

	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	vieta1lem1	$⊢ (φ \land z \in R) \to (Q \in Poly (ℂ) \land D = \deg (Q))$

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		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
11	4	adantr	$⊢ (φ \land z \in R) \to F \in Poly (S)$
12	10 11	sselid	$⊢ (φ \land z \in R) \to F \in Poly (ℂ)$
13		cnvimass	$⊢ F^{-1} [\{0\}] \subseteq dom F$
14	3 13	eqsstri	$⊢ R \subseteq dom F$
15		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
16	4 15	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
17	14 16	fssdm	$⊢ φ \to R \subseteq ℂ$
18	17	sselda	$⊢ (φ \land z \in R) \to z \in ℂ$
19		eqid	$⊢ X^{p} -_{f} (ℂ \times \{z\}) = X^{p} -_{f} (ℂ \times \{z\})$
20	19	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\})$
21	18 20	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\})$
22	21	simp1d	$⊢ (φ \land z \in R) \to X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ)$
23	21	simp2d	$⊢ (φ \land z \in R) \to \deg (X^{p} -_{f} (ℂ \times \{z\})) = 1$
24		ax-1ne0	$⊢ 1 \neq 0$
25	24	a1i	$⊢ (φ \land z \in R) \to 1 \neq 0$
26	23 25	eqnetrd	$⊢ (φ \land z \in R) \to \deg (X^{p} -_{f} (ℂ \times \{z\})) \neq 0$
27		fveq2	$⊢ X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \to \deg (X^{p} -_{f} (ℂ \times \{z\})) = \deg (0_{𝑝})$
28		dgr0	$⊢ \deg (0_{𝑝}) = 0$
29	27 28	eqtrdi	$⊢ X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \to \deg (X^{p} -_{f} (ℂ \times \{z\})) = 0$
30	29	necon3i	$⊢ \deg (X^{p} -_{f} (ℂ \times \{z\})) \neq 0 \to X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝}$
31	26 30	syl	$⊢ (φ \land z \in R) \to X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝}$
32		quotcl2	$⊢ (F \in Poly (ℂ) \land X^{p} -_{f} (ℂ \times \{z\}) \in Poly (ℂ) \land X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝}) \to F quot (X^{p} -_{f} (ℂ \times \{z\})) \in Poly (ℂ)$
33	12 22 31 32	syl3anc	$⊢ (φ \land z \in R) \to F quot (X^{p} -_{f} (ℂ \times \{z\})) \in Poly (ℂ)$
34	9 33	eqeltrid	$⊢ (φ \land z \in R) \to Q \in Poly (ℂ)$
35		1cnd	$⊢ (φ \land z \in R) \to 1 \in ℂ$
36	6	nncnd	$⊢ φ \to D \in ℂ$
37	36	adantr	$⊢ (φ \land z \in R) \to D \in ℂ$
38		dgrcl	$⊢ Q \in Poly (ℂ) \to \deg (Q) \in ℕ_{0}$
39	34 38	syl	$⊢ (φ \land z \in R) \to \deg (Q) \in ℕ_{0}$
40	39	nn0cnd	$⊢ (φ \land z \in R) \to \deg (Q) \in ℂ$
41		ax-1cn	$⊢ 1 \in ℂ$
42		addcom	$⊢ (1 \in ℂ \land D \in ℂ) \to 1 + D = D + 1$
43	41 37 42	sylancr	$⊢ (φ \land z \in R) \to 1 + D = D + 1$
44	7 2	eqtrdi	$⊢ φ \to D + 1 = \deg (F)$
45	44	adantr	$⊢ (φ \land z \in R) \to D + 1 = \deg (F)$
46	3	eleq2i	$⊢ z \in R \leftrightarrow z \in F^{-1} [\{0\}]$
47	16	ffnd	$⊢ φ \to F Fn ℂ$
48		fniniseg	$⊢ F Fn ℂ \to (z \in F^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land F (z) = 0))$
49	47 48	syl	$⊢ φ \to (z \in F^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land F (z) = 0))$
50	46 49	bitrid	$⊢ φ \to (z \in R \leftrightarrow (z \in ℂ \land F (z) = 0))$
51	50	simplbda	$⊢ (φ \land z \in R) \to F (z) = 0$
52	19	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\})))$
53	11 18 51 52	syl3anc	$⊢ (φ \land z \in R) \to F = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} (F quot (X^{p} -_{f} (ℂ \times \{z\})))$
54	9	oveq2i	$⊢ (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} (F quot (X^{p} -_{f} (ℂ \times \{z\})))$
55	53 54	eqtr4di	$⊢ (φ \land z \in R) \to F = (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q$
56	55	fveq2d	$⊢ (φ \land z \in R) \to \deg (F) = \deg ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q)$
57	6	peano2nnd	$⊢ φ \to D + 1 \in ℕ$
58	7 57	eqeltrrd	$⊢ φ \to N \in ℕ$
59	58	nnne0d	$⊢ φ \to N \neq 0$
60	2 59	eqnetrrid	$⊢ φ \to \deg (F) \neq 0$
61		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
62	61 28	eqtrdi	$⊢ F = 0_{𝑝} \to \deg (F) = 0$
63	62	necon3i	$⊢ \deg (F) \neq 0 \to F \neq 0_{𝑝}$
64	60 63	syl	$⊢ φ \to F \neq 0_{𝑝}$
65	64	adantr	$⊢ (φ \land z \in R) \to F \neq 0_{𝑝}$
66	55 65	eqnetrrd	$⊢ (φ \land z \in R) \to (X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q \neq 0_{𝑝}$
67		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_{𝑝}))$
68	22 34 67	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_{𝑝}))$
69	68	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_{𝑝}))$
70	66 69	mpbid	$⊢ (φ \land z \in R) \to \neg (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝})$
71		neanior	$⊢ (X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝} \land Q \neq 0_{𝑝}) \leftrightarrow \neg (X^{p} -_{f} (ℂ \times \{z\}) = 0_{𝑝} \lor Q = 0_{𝑝})$
72	70 71	sylibr	$⊢ (φ \land z \in R) \to (X^{p} -_{f} (ℂ \times \{z\}) \neq 0_{𝑝} \land Q \neq 0_{𝑝})$
73	72	simprd	$⊢ (φ \land z \in R) \to Q \neq 0_{𝑝}$
74		eqid	$⊢ \deg (X^{p} -_{f} (ℂ \times \{z\})) = \deg (X^{p} -_{f} (ℂ \times \{z\}))$
75		eqid	$⊢ \deg (Q) = \deg (Q)$
76	74 75	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)$
77	22 31 34 73 76	syl22anc	$⊢ (φ \land z \in R) \to \deg ((X^{p} -_{f} (ℂ \times \{z\})) \times_{f} Q) = \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)$
78	45 56 77	3eqtrd	$⊢ (φ \land z \in R) \to D + 1 = \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q)$
79	23	oveq1d	$⊢ (φ \land z \in R) \to \deg (X^{p} -_{f} (ℂ \times \{z\})) + \deg (Q) = 1 + \deg (Q)$
80	43 78 79	3eqtrd	$⊢ (φ \land z \in R) \to 1 + D = 1 + \deg (Q)$
81	35 37 40 80	addcanad	$⊢ (φ \land z \in R) \to D = \deg (Q)$
82	34 81	jca	$⊢ (φ \land z \in R) \to (Q \in Poly (ℂ) \land D = \deg (Q))$

Metamath Proof Explorer

Theorem vieta1lem1

Proof