Description: A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | 0dgrb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | eqid | |
|
3 | 1 2 | coeid | |
4 | 3 | adantr | |
5 | simplr | |
|
6 | 5 | oveq2d | |
7 | 6 | sumeq1d | |
8 | 0z | |
|
9 | exp0 | |
|
10 | 9 | adantl | |
11 | 10 | oveq2d | |
12 | 1 | coef3 | |
13 | 0nn0 | |
|
14 | ffvelrn | |
|
15 | 12 13 14 | sylancl | |
16 | 15 | ad2antrr | |
17 | 16 | mulid1d | |
18 | 11 17 | eqtrd | |
19 | 18 16 | eqeltrd | |
20 | fveq2 | |
|
21 | oveq2 | |
|
22 | 20 21 | oveq12d | |
23 | 22 | fsum1 | |
24 | 8 19 23 | sylancr | |
25 | 24 18 | eqtrd | |
26 | 7 25 | eqtrd | |
27 | 26 | mpteq2dva | |
28 | 4 27 | eqtrd | |
29 | fconstmpt | |
|
30 | 28 29 | eqtr4di | |
31 | 30 | fveq1d | |
32 | 0cn | |
|
33 | fvex | |
|
34 | 33 | fvconst2 | |
35 | 32 34 | ax-mp | |
36 | 31 35 | eqtrdi | |
37 | 36 | sneqd | |
38 | 37 | xpeq2d | |
39 | 30 38 | eqtr4d | |
40 | 39 | ex | |
41 | plyf | |
|
42 | ffvelrn | |
|
43 | 41 32 42 | sylancl | |
44 | 0dgr | |
|
45 | 43 44 | syl | |
46 | fveqeq2 | |
|
47 | 45 46 | syl5ibrcom | |
48 | 40 47 | impbid | |