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 ) |