Theorem 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	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → ∃ 𝑧 ∈ ℂ ( 𝐹 ‘ 𝑧 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
2		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
3		simpl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		simpr	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → ( deg ‘ 𝐹 ) ∈ ℕ )
5		eqid	⊢ if ( if ( 1 ≤ 𝑠 , 𝑠 , 1 ) ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( ( coeff ‘ 𝐹 ) ‘ ( deg ‘ 𝐹 ) ) ) / 2 ) ) , ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( ( coeff ‘ 𝐹 ) ‘ ( deg ‘ 𝐹 ) ) ) / 2 ) ) , if ( 1 ≤ 𝑠 , 𝑠 , 1 ) ) = if ( if ( 1 ≤ 𝑠 , 𝑠 , 1 ) ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( ( coeff ‘ 𝐹 ) ‘ ( deg ‘ 𝐹 ) ) ) / 2 ) ) , ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( ( coeff ‘ 𝐹 ) ‘ ( deg ‘ 𝐹 ) ) ) / 2 ) ) , if ( 1 ≤ 𝑠 , 𝑠 , 1 ) )
6		eqid	⊢ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( ( coeff ‘ 𝐹 ) ‘ ( deg ‘ 𝐹 ) ) ) / 2 ) ) = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( ( coeff ‘ 𝐹 ) ‘ ( deg ‘ 𝐹 ) ) ) / 2 ) )
7	1 2 3 4 5 6	ftalem2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → ∃ 𝑟 ∈ ℝ+ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
8		simpll	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
9		simplr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( deg ‘ 𝐹 ) ∈ ℕ )
10		eqid	⊢ { 𝑠 ∈ ℂ ∣ ( abs ‘ 𝑠 ) ≤ 𝑟 } = { 𝑠 ∈ ℂ ∣ ( abs ‘ 𝑠 ) ≤ 𝑟 }
11		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12		simprl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ) → 𝑟 ∈ ℝ+ )
13		simprr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
14		fveq2	⊢ ( 𝑦 = 𝑥 → ( abs ‘ 𝑦 ) = ( abs ‘ 𝑥 ) )
15	14	breq2d	⊢ ( 𝑦 = 𝑥 → ( 𝑟 < ( abs ‘ 𝑦 ) ↔ 𝑟 < ( abs ‘ 𝑥 ) ) )
16		2fveq3	⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
17	16	breq2d	⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
18	15 17	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
19	18	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
20	13 19	sylib	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
21	1 2 8 9 10 11 12 20	ftalem3	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
22	7 21	rexlimddv	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
23		simpll	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ≠ 0 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
24		simplr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ≠ 0 ) ) → ( deg ‘ 𝐹 ) ∈ ℕ )
25		simprl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ≠ 0 ) ) → 𝑧 ∈ ℂ )
26		simprr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) ≠ 0 )
27	1 2 23 24 25 26	ftalem7	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ≠ 0 ) ) → ¬ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
28	27	expr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑧 ) ≠ 0 → ¬ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
29	28	necon4ad	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑧 ) = 0 ) )
30	29	reximdva	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → ( ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℂ ( 𝐹 ‘ 𝑧 ) = 0 ) )
31	22 30	mpd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) ∈ ℕ ) → ∃ 𝑧 ∈ ℂ ( 𝐹 ‘ 𝑧 ) = 0 )