Metamath Proof Explorer

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 )