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 ‘ 𝑃 ) ∈ ℕ )