This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )