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 )