This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> E. z e. CC ( F ` z ) = 0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
2 eqid 
 |-  ( deg ` F ) = ( deg ` F )
3 simpl 
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> F e. ( Poly ` S ) )
4 simpr 
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> ( deg ` F ) e. NN )
5 eqid 
 |-  if ( if ( 1 <_ s , s , 1 ) <_ ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( ( coeff ` F ) ` ( deg ` F ) ) ) / 2 ) ) , ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( ( coeff ` F ) ` ( deg ` F ) ) ) / 2 ) ) , if ( 1 <_ s , s , 1 ) ) = if ( if ( 1 <_ s , s , 1 ) <_ ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( ( coeff ` F ) ` ( deg ` F ) ) ) / 2 ) ) , ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( ( coeff ` F ) ` ( deg ` F ) ) ) / 2 ) ) , if ( 1 <_ s , s , 1 ) )
6 eqid 
 |-  ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( ( coeff ` F ) ` ( deg ` F ) ) ) / 2 ) ) = ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( ( coeff ` F ) ` ( deg ` F ) ) ) / 2 ) )
7 1 2 3 4 5 6 ftalem2 
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> E. r e. RR+ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) )
8 simpll 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( r e. RR+ /\ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) ) ) -> F e. ( Poly ` S ) )
9 simplr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( r e. RR+ /\ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) ) ) -> ( deg ` F ) e. NN )
10 eqid 
 |-  { s e. CC | ( abs ` s ) <_ r } = { s e. CC | ( abs ` s ) <_ r }
11 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 simprl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( r e. RR+ /\ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) ) ) -> r e. RR+ )
13 simprr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( r e. RR+ /\ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) ) ) -> A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) )
14 fveq2 
 |-  ( y = x -> ( abs ` y ) = ( abs ` x ) )
15 14 breq2d 
 |-  ( y = x -> ( r < ( abs ` y ) <-> r < ( abs ` x ) ) )
16 2fveq3 
 |-  ( y = x -> ( abs ` ( F ` y ) ) = ( abs ` ( F ` x ) ) )
17 16 breq2d 
 |-  ( y = x -> ( ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) <-> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
18 15 17 imbi12d 
 |-  ( y = x -> ( ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) <-> ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
19 18 cbvralvw 
 |-  ( A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) <-> A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
20 13 19 sylib 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( r e. RR+ /\ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) ) ) -> A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
21 1 2 8 9 10 11 12 20 ftalem3 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( r e. RR+ /\ A. y e. CC ( r < ( abs ` y ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` y ) ) ) ) ) -> E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
22 7 21 rexlimddv 
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
23 simpll 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( z e. CC /\ ( F ` z ) =/= 0 ) ) -> F e. ( Poly ` S ) )
24 simplr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( z e. CC /\ ( F ` z ) =/= 0 ) ) -> ( deg ` F ) e. NN )
25 simprl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( z e. CC /\ ( F ` z ) =/= 0 ) ) -> z e. CC )
26 simprr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( z e. CC /\ ( F ` z ) =/= 0 ) ) -> ( F ` z ) =/= 0 )
27 1 2 23 24 25 26 ftalem7 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ ( z e. CC /\ ( F ` z ) =/= 0 ) ) -> -. A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
28 27 expr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ z e. CC ) -> ( ( F ` z ) =/= 0 -> -. A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
29 28 necon4ad 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) /\ z e. CC ) -> ( A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> ( F ` z ) = 0 ) )
30 29 reximdva 
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> ( E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> E. z e. CC ( F ` z ) = 0 ) )
31 22 30 mpd 
 |-  ( ( F e. ( Poly ` S ) /\ ( deg ` F ) e. NN ) -> E. z e. CC ( F ` z ) = 0 )