Theorem 0dgr

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

	Ref	Expression
Assertion	0dgr	⊢ ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℂ ⊆ ℂ
2		plyconst	⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
4		0nn0	⊢ 0 ∈ ℕ0
5	4	a1i	⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℕ0 )
6		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 0 ) ) → 𝐴 ∈ ℂ )
7		0z	⊢ 0 ∈ ℤ
8		exp0	⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 0 ) = 1 )
9	8	oveq2d	⊢ ( 𝑧 ∈ ℂ → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = ( 𝐴 · 1 ) )
10		mulid1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
11	9 10	sylan9eqr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = 𝐴 )
12		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ )
13	11 12	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) ∈ ℂ )
14		oveq2	⊢ ( 𝑘 = 0 → ( 𝑧 ↑ 𝑘 ) = ( 𝑧 ↑ 0 ) )
15	14	oveq2d	⊢ ( 𝑘 = 0 → ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
16	15	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
17	7 13 16	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
18	17 11	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = 𝐴 )
19	18	mpteq2dva	⊢ ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ 𝐴 ) )
20		fconstmpt	⊢ ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ 𝐴 )
21	19 20	syl6reqr	⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
22	3 5 6 21	dgrle	⊢ ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) ≤ 0 )
23		dgrcl	⊢ ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ℂ × { 𝐴 } ) ) ∈ ℕ0 )
24		nn0le0eq0	⊢ ( ( deg ‘ ( ℂ × { 𝐴 } ) ) ∈ ℕ0 → ( ( deg ‘ ( ℂ × { 𝐴 } ) ) ≤ 0 ↔ ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 ) )
25	3 23 24	3syl	⊢ ( 𝐴 ∈ ℂ → ( ( deg ‘ ( ℂ × { 𝐴 } ) ) ≤ 0 ↔ ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 ) )
26	22 25	mpbid	⊢ ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )