0dgr

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

		Ref	Expression
	Assertion	0dgr	$⊢ A \in ℂ \to \deg (ℂ \times \{A\}) = 0$

Proof

Step	Hyp	Ref	Expression
1		ssid	$⊢ ℂ \subseteq ℂ$
2		plyconst	$⊢ (ℂ \subseteq ℂ \land A \in ℂ) \to ℂ \times \{A\} \in Poly (ℂ)$
3	1 2	mpan	$⊢ A \in ℂ \to ℂ \times \{A\} \in Poly (ℂ)$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5	4	a1i	$⊢ A \in ℂ \to 0 \in ℕ_{0}$
6		simpl	$⊢ (A \in ℂ \land k \in (0 \dots 0)) \to A \in ℂ$
7		fconstmpt	$⊢ ℂ \times \{A\} = (z \in ℂ ⟼ A)$
8		0z	$⊢ 0 \in ℤ$
9		exp0	$⊢ z \in ℂ \to z^{0} = 1$
10	9	oveq2d	$⊢ z \in ℂ \to A z^{0} = A \cdot 1$
11		mulrid	$⊢ A \in ℂ \to A \cdot 1 = A$
12	10 11	sylan9eqr	$⊢ (A \in ℂ \land z \in ℂ) \to A z^{0} = A$
13		simpl	$⊢ (A \in ℂ \land z \in ℂ) \to A \in ℂ$
14	12 13	eqeltrd	$⊢ (A \in ℂ \land z \in ℂ) \to A z^{0} \in ℂ$
15		oveq2	$⊢ k = 0 \to z^{k} = z^{0}$
16	15	oveq2d	$⊢ k = 0 \to A z^{k} = A z^{0}$
17	16	fsum1	$⊢ (0 \in ℤ \land A z^{0} \in ℂ) \to \sum_{k = 0}^{0} A z^{k} = A z^{0}$
18	8 14 17	sylancr	$⊢ (A \in ℂ \land z \in ℂ) \to \sum_{k = 0}^{0} A z^{k} = A z^{0}$
19	18 12	eqtrd	$⊢ (A \in ℂ \land z \in ℂ) \to \sum_{k = 0}^{0} A z^{k} = A$
20	19	mpteq2dva	$⊢ A \in ℂ \to (z \in ℂ ⟼ \sum_{k = 0}^{0} A z^{k}) = (z \in ℂ ⟼ A)$
21	7 20	eqtr4id	$⊢ A \in ℂ \to ℂ \times \{A\} = (z \in ℂ ⟼ \sum_{k = 0}^{0} A z^{k})$
22	3 5 6 21	dgrle	$⊢ A \in ℂ \to \deg (ℂ \times \{A\}) \leq 0$
23		dgrcl	$⊢ ℂ \times \{A\} \in Poly (ℂ) \to \deg (ℂ \times \{A\}) \in ℕ_{0}$
24		nn0le0eq0	$⊢ \deg (ℂ \times \{A\}) \in ℕ_{0} \to (\deg (ℂ \times \{A\}) \leq 0 \leftrightarrow \deg (ℂ \times \{A\}) = 0)$
25	3 23 24	3syl	$⊢ A \in ℂ \to (\deg (ℂ \times \{A\}) \leq 0 \leftrightarrow \deg (ℂ \times \{A\}) = 0)$
26	22 25	mpbid	$⊢ A \in ℂ \to \deg (ℂ \times \{A\}) = 0$

Metamath Proof Explorer

Theorem 0dgr

Proof