fta

Description: The Fundamental Theorem of Algebra. Any polynomial with positive degree (i.e. non-constant) has a root. This is Metamath 100 proof #2. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	fta	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to \exists z \in ℂ F (z) = 0$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ coeff (F) = coeff (F)$
2		eqid	$⊢ \deg (F) = \deg (F)$
3		simpl	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to F \in Poly (S)$
4		simpr	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to \deg (F) \in ℕ$
5		eqid	$⊢ if (if (1 \leq s, s, 1) \leq \frac{\|F (0)\|}{\frac{\|coeff (F) (\deg (F))\|}{2}}, \frac{\|F (0)\|}{\frac{\|coeff (F) (\deg (F))\|}{2}}, if (1 \leq s, s, 1)) = if (if (1 \leq s, s, 1) \leq \frac{\|F (0)\|}{\frac{\|coeff (F) (\deg (F))\|}{2}}, \frac{\|F (0)\|}{\frac{\|coeff (F) (\deg (F))\|}{2}}, if (1 \leq s, s, 1))$
6		eqid	$⊢ \frac{\|F (0)\|}{\frac{\|coeff (F) (\deg (F))\|}{2}} = \frac{\|F (0)\|}{\frac{\|coeff (F) (\deg (F))\|}{2}}$
7	1 2 3 4 5 6	ftalem2	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to \exists r \in ℝ^{+} \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|)$
8		simpll	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (r \in ℝ^{+} \land \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|))) \to F \in Poly (S)$
9		simplr	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (r \in ℝ^{+} \land \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|))) \to \deg (F) \in ℕ$
10		eqid	$⊢ \{s \in ℂ \| \|s\| \leq r\} = \{s \in ℂ \| \|s\| \leq r\}$
11		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
12		simprl	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (r \in ℝ^{+} \land \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|))) \to r \in ℝ^{+}$
13		simprr	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (r \in ℝ^{+} \land \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|))) \to \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|)$
14		fveq2	$⊢ y = x \to \|y\| = \|x\|$
15	14	breq2d	$⊢ y = x \to (r < \|y\| \leftrightarrow r < \|x\|)$
16		2fveq3	$⊢ y = x \to \|F (y)\| = \|F (x)\|$
17	16	breq2d	$⊢ y = x \to (\|F (0)\| < \|F (y)\| \leftrightarrow \|F (0)\| < \|F (x)\|)$
18	15 17	imbi12d	$⊢ y = x \to ((r < \|y\| \to \|F (0)\| < \|F (y)\|) \leftrightarrow (r < \|x\| \to \|F (0)\| < \|F (x)\|))$
19	18	cbvralvw	$⊢ \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|) \leftrightarrow \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|)$
20	13 19	sylib	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (r \in ℝ^{+} \land \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|))) \to \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|)$
21	1 2 8 9 10 11 12 20	ftalem3	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (r \in ℝ^{+} \land \forall y \in ℂ (r < \|y\| \to \|F (0)\| < \|F (y)\|))) \to \exists z \in ℂ \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$
22	7 21	rexlimddv	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to \exists z \in ℂ \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$
23		simpll	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (z \in ℂ \land F (z) \neq 0)) \to F \in Poly (S)$
24		simplr	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (z \in ℂ \land F (z) \neq 0)) \to \deg (F) \in ℕ$
25		simprl	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (z \in ℂ \land F (z) \neq 0)) \to z \in ℂ$
26		simprr	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (z \in ℂ \land F (z) \neq 0)) \to F (z) \neq 0$
27	1 2 23 24 25 26	ftalem7	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land (z \in ℂ \land F (z) \neq 0)) \to \neg \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$
28	27	expr	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land z \in ℂ) \to (F (z) \neq 0 \to \neg \forall x \in ℂ \|F (z)\| \leq \|F (x)\|)$
29	28	necon4ad	$⊢ ((F \in Poly (S) \land \deg (F) \in ℕ) \land z \in ℂ) \to (\forall x \in ℂ \|F (z)\| \leq \|F (x)\| \to F (z) = 0)$
30	29	reximdva	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to (\exists z \in ℂ \forall x \in ℂ \|F (z)\| \leq \|F (x)\| \to \exists z \in ℂ F (z) = 0)$
31	22 30	mpd	$⊢ (F \in Poly (S) \land \deg (F) \in ℕ) \to \exists z \in ℂ F (z) = 0$

Metamath Proof Explorer

Theorem fta

Proof