Step |
Hyp |
Ref |
Expression |
1 |
|
dgreq.1 |
|- ( ph -> F e. ( Poly ` S ) ) |
2 |
|
dgreq.2 |
|- ( ph -> N e. NN0 ) |
3 |
|
dgreq.3 |
|- ( ph -> A : NN0 --> CC ) |
4 |
|
dgreq.4 |
|- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) |
5 |
|
dgreq.5 |
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) |
6 |
|
dgreq.6 |
|- ( ph -> ( A ` N ) =/= 0 ) |
7 |
|
elfznn0 |
|- ( k e. ( 0 ... N ) -> k e. NN0 ) |
8 |
|
ffvelrn |
|- ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC ) |
9 |
3 7 8
|
syl2an |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC ) |
10 |
1 2 9 5
|
dgrle |
|- ( ph -> ( deg ` F ) <_ N ) |
11 |
1 2 3 4 5
|
coeeq |
|- ( ph -> ( coeff ` F ) = A ) |
12 |
11
|
fveq1d |
|- ( ph -> ( ( coeff ` F ) ` N ) = ( A ` N ) ) |
13 |
12 6
|
eqnetrd |
|- ( ph -> ( ( coeff ` F ) ` N ) =/= 0 ) |
14 |
|
eqid |
|- ( coeff ` F ) = ( coeff ` F ) |
15 |
|
eqid |
|- ( deg ` F ) = ( deg ` F ) |
16 |
14 15
|
dgrub |
|- ( ( F e. ( Poly ` S ) /\ N e. NN0 /\ ( ( coeff ` F ) ` N ) =/= 0 ) -> N <_ ( deg ` F ) ) |
17 |
1 2 13 16
|
syl3anc |
|- ( ph -> N <_ ( deg ` F ) ) |
18 |
|
dgrcl |
|- ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 ) |
19 |
1 18
|
syl |
|- ( ph -> ( deg ` F ) e. NN0 ) |
20 |
19
|
nn0red |
|- ( ph -> ( deg ` F ) e. RR ) |
21 |
2
|
nn0red |
|- ( ph -> N e. RR ) |
22 |
20 21
|
letri3d |
|- ( ph -> ( ( deg ` F ) = N <-> ( ( deg ` F ) <_ N /\ N <_ ( deg ` F ) ) ) ) |
23 |
10 17 22
|
mpbir2and |
|- ( ph -> ( deg ` F ) = N ) |