Theorem 0dgr

Description: A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Assertion	0dgr	|- ( A e. CC -> ( deg ` ( CC X. { A } ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- CC C_ CC
2		plyconst	|- ( ( CC C_ CC /\ A e. CC ) -> ( CC X. { A } ) e. ( Poly ` CC ) )
3	1 2	mpan	|- ( A e. CC -> ( CC X. { A } ) e. ( Poly ` CC ) )
4		0nn0	|- 0 e. NN0
5	4	a1i	|- ( A e. CC -> 0 e. NN0 )
6		simpl	|- ( ( A e. CC /\ k e. ( 0 ... 0 ) ) -> A e. CC )
7		fconstmpt	|- ( CC X. { A } ) = ( z e. CC |-> A )
8		0z	|- 0 e. ZZ
9		exp0	|- ( z e. CC -> ( z ^ 0 ) = 1 )
10	9	oveq2d	|- ( z e. CC -> ( A x. ( z ^ 0 ) ) = ( A x. 1 ) )
11		mulid1	|- ( A e. CC -> ( A x. 1 ) = A )
12	10 11	sylan9eqr	|- ( ( A e. CC /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = A )
13		simpl	|- ( ( A e. CC /\ z e. CC ) -> A e. CC )
14	12 13	eqeltrd	|- ( ( A e. CC /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) e. CC )
15		oveq2	|- ( k = 0 -> ( z ^ k ) = ( z ^ 0 ) )
16	15	oveq2d	|- ( k = 0 -> ( A x. ( z ^ k ) ) = ( A x. ( z ^ 0 ) ) )
17	16	fsum1	|- ( ( 0 e. ZZ /\ ( A x. ( z ^ 0 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) = ( A x. ( z ^ 0 ) ) )
18	8 14 17	sylancr	|- ( ( A e. CC /\ z e. CC ) -> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) = ( A x. ( z ^ 0 ) ) )
19	18 12	eqtrd	|- ( ( A e. CC /\ z e. CC ) -> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) = A )
20	19	mpteq2dva	|- ( A e. CC -> ( z e. CC |-> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) ) = ( z e. CC |-> A ) )
21	7 20	eqtr4id	|- ( A e. CC -> ( CC X. { A } ) = ( z e. CC |-> sum_ k e. ( 0 ... 0 ) ( A x. ( z ^ k ) ) ) )
22	3 5 6 21	dgrle	|- ( A e. CC -> ( deg ` ( CC X. { A } ) ) <_ 0 )
23		dgrcl	|- ( ( CC X. { A } ) e. ( Poly ` CC ) -> ( deg ` ( CC X. { A } ) ) e. NN0 )
24		nn0le0eq0	|- ( ( deg ` ( CC X. { A } ) ) e. NN0 -> ( ( deg ` ( CC X. { A } ) ) <_ 0 <-> ( deg ` ( CC X. { A } ) ) = 0 ) )
25	3 23 24	3syl	|- ( A e. CC -> ( ( deg ` ( CC X. { A } ) ) <_ 0 <-> ( deg ` ( CC X. { A } ) ) = 0 ) )
26	22 25	mpbid	|- ( A e. CC -> ( deg ` ( CC X. { A } ) ) = 0 )