Metamath Proof Explorer

Theorem dgrnznn

Description: A nonzero polynomial with a root has positive degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion dgrnznn ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) )
2 1 fveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( 𝑃 ‘ 𝐴 ) = ( ( ℂ × { ( 𝑃 ‘ 0 ) } ) ‘ 𝐴 ) )
3 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( 𝑃 ‘ 𝐴 ) = 0 )
4 fvex ⊢ ( 𝑃 ‘ 0 ) ∈ V
5 4 fvconst2 ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { ( 𝑃 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑃 ‘ 0 ) )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( ( ℂ × { ( 𝑃 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑃 ‘ 0 ) )
7 2 3 6 3eqtr3rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( 𝑃 ‘ 0 ) = 0 )
8 7 sneqd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → { ( 𝑃 ‘ 0 ) } = { 0 } )
9 8 xpeq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( ℂ × { ( 𝑃 ‘ 0 ) } ) = ( ℂ × { 0 } ) )
10 1 9 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → 𝑃 = ( ℂ × { 0 } ) )
11 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
12 10 11 eqtr4di ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → 𝑃 = 0𝑝 )
13 12 ex ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) → ( 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) → 𝑃 = 0𝑝 ) )
14 13 necon3ad ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) → ( 𝑃 ≠ 0𝑝 → ¬ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) )
15 14 impcom ⊢ ( ( 𝑃 ≠ 0𝑝 ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ¬ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) )
16 15 adantll ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ¬ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) )
17 0dgrb ⊢ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) → ( ( deg ‘ 𝑃 ) = 0 ↔ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) )
18 17 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( ( deg ‘ 𝑃 ) = 0 ↔ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) )
19 16 18 mtbird ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ¬ ( deg ‘ 𝑃 ) = 0 )
20 dgrcl ⊢ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝑃 ) ∈ ℕ0 )
21 20 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ ℕ0 )
22 elnn0 ⊢ ( ( deg ‘ 𝑃 ) ∈ ℕ0 ↔ ( ( deg ‘ 𝑃 ) ∈ ℕ ∨ ( deg ‘ 𝑃 ) = 0 ) )
23 21 22 sylib ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( ( deg ‘ 𝑃 ) ∈ ℕ ∨ ( deg ‘ 𝑃 ) = 0 ) )
24 orel2 ⊢ ( ¬ ( deg ‘ 𝑃 ) = 0 → ( ( ( deg ‘ 𝑃 ) ∈ ℕ ∨ ( deg ‘ 𝑃 ) = 0 ) → ( deg ‘ 𝑃 ) ∈ ℕ ) )
25 19 23 24 sylc ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ ℕ )