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		fconstmpt	⊢ ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ 𝐴 )
8		0z	⊢ 0 ∈ ℤ
9		exp0	⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 0 ) = 1 )
10	9	oveq2d	⊢ ( 𝑧 ∈ ℂ → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = ( 𝐴 · 1 ) )
11		mulrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
12	10 11	sylan9eqr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = 𝐴 )
13		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ )
14	12 13	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) ∈ ℂ )
15		oveq2	⊢ ( 𝑘 = 0 → ( 𝑧 ↑ 𝑘 ) = ( 𝑧 ↑ 0 ) )
16	15	oveq2d	⊢ ( 𝑘 = 0 → ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
17	16	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
18	8 14 17	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
19	18 12	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) = 𝐴 )
20	19	mpteq2dva	⊢ ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ 𝐴 ) )
21	7 20	eqtr4id	⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 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 )