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

Metamath Proof Explorer

Theorem dgrnznn

Description: A nonzero polynomial with a root has positive degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion dgrnznn 
|- ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( deg ` P ) e. NN )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> P = ( CC X. { ( P ` 0 ) } ) )
2 1 fveq1d 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> ( P ` A ) = ( ( CC X. { ( P ` 0 ) } ) ` A ) )
3 simplr 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> ( P ` A ) = 0 )
4 fvex 
 |-  ( P ` 0 ) e. _V
5 4 fvconst2 
 |-  ( A e. CC -> ( ( CC X. { ( P ` 0 ) } ) ` A ) = ( P ` 0 ) )
6 5 ad2antrr 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> ( ( CC X. { ( P ` 0 ) } ) ` A ) = ( P ` 0 ) )
7 2 3 6 3eqtr3rd 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> ( P ` 0 ) = 0 )
8 7 sneqd 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> { ( P ` 0 ) } = { 0 } )
9 8 xpeq2d 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> ( CC X. { ( P ` 0 ) } ) = ( CC X. { 0 } ) )
10 1 9 eqtrd 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> P = ( CC X. { 0 } ) )
11 df-0p 
 |-  0p = ( CC X. { 0 } )
12 10 11 eqtr4di 
 |-  ( ( ( A e. CC /\ ( P ` A ) = 0 ) /\ P = ( CC X. { ( P ` 0 ) } ) ) -> P = 0p )
13 12 ex 
 |-  ( ( A e. CC /\ ( P ` A ) = 0 ) -> ( P = ( CC X. { ( P ` 0 ) } ) -> P = 0p ) )
14 13 necon3ad 
 |-  ( ( A e. CC /\ ( P ` A ) = 0 ) -> ( P =/= 0p -> -. P = ( CC X. { ( P ` 0 ) } ) ) )
15 14 impcom 
 |-  ( ( P =/= 0p /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> -. P = ( CC X. { ( P ` 0 ) } ) )
16 15 adantll 
 |-  ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> -. P = ( CC X. { ( P ` 0 ) } ) )
17 0dgrb 
 |-  ( P e. ( Poly ` S ) -> ( ( deg ` P ) = 0 <-> P = ( CC X. { ( P ` 0 ) } ) ) )
18 17 ad2antrr 
 |-  ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( ( deg ` P ) = 0 <-> P = ( CC X. { ( P ` 0 ) } ) ) )
19 16 18 mtbird 
 |-  ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> -. ( deg ` P ) = 0 )
20 dgrcl 
 |-  ( P e. ( Poly ` S ) -> ( deg ` P ) e. NN0 )
21 20 ad2antrr 
 |-  ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( deg ` P ) e. NN0 )
22 elnn0 
 |-  ( ( deg ` P ) e. NN0 <-> ( ( deg ` P ) e. NN \/ ( deg ` P ) = 0 ) )
23 21 22 sylib 
 |-  ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( ( deg ` P ) e. NN \/ ( deg ` P ) = 0 ) )
24 orel2 
 |-  ( -. ( deg ` P ) = 0 -> ( ( ( deg ` P ) e. NN \/ ( deg ` P ) = 0 ) -> ( deg ` P ) e. NN ) )
25 19 23 24 sylc 
 |-  ( ( ( P e. ( Poly ` S ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( deg ` P ) e. NN )