Metamath Proof Explorer


Theorem dgreq

Description: If the highest term in a polynomial expression is nonzero, then the polynomial's degree is completely determined. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgreq.1 φ F Poly S
dgreq.2 φ N 0
dgreq.3 φ A : 0
dgreq.4 φ A N + 1 = 0
dgreq.5 φ F = z k = 0 N A k z k
dgreq.6 φ A N 0
Assertion dgreq φ deg F = N

Proof

Step Hyp Ref Expression
1 dgreq.1 φ F Poly S
2 dgreq.2 φ N 0
3 dgreq.3 φ A : 0
4 dgreq.4 φ A N + 1 = 0
5 dgreq.5 φ F = z k = 0 N A k z k
6 dgreq.6 φ A N 0
7 elfznn0 k 0 N k 0
8 ffvelrn A : 0 k 0 A k
9 3 7 8 syl2an φ k 0 N A k
10 1 2 9 5 dgrle φ deg F N
11 1 2 3 4 5 coeeq φ coeff F = A
12 11 fveq1d φ coeff F N = A N
13 12 6 eqnetrd φ coeff F N 0
14 eqid coeff F = coeff F
15 eqid deg F = deg F
16 14 15 dgrub F Poly S N 0 coeff F N 0 N deg F
17 1 2 13 16 syl3anc φ N deg F
18 dgrcl F Poly S deg F 0
19 1 18 syl φ deg F 0
20 19 nn0red φ deg F
21 2 nn0red φ N
22 20 21 letri3d φ deg F = N deg F N N deg F
23 10 17 22 mpbir2and φ deg F = N