dgrnznn

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

		Ref	Expression
	Assertion	dgrnznn	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to \deg (P) \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to P = ℂ \times \{P (0)\}$
2	1	fveq1d	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to P (A) = (ℂ \times \{P (0)\}) (A)$
3		simplr	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to P (A) = 0$
4		fvex	$⊢ P (0) \in V$
5	4	fvconst2	$⊢ A \in ℂ \to (ℂ \times \{P (0)\}) (A) = P (0)$
6	5	ad2antrr	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to (ℂ \times \{P (0)\}) (A) = P (0)$
7	2 3 6	3eqtr3rd	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to P (0) = 0$
8	7	sneqd	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to \{P (0)\} = \{0\}$
9	8	xpeq2d	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to ℂ \times \{P (0)\} = ℂ \times \{0\}$
10	1 9	eqtrd	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to P = ℂ \times \{0\}$
11		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
12	10 11	eqtr4di	$⊢ ((A \in ℂ \land P (A) = 0) \land P = ℂ \times \{P (0)\}) \to P = 0_{𝑝}$
13	12	ex	$⊢ (A \in ℂ \land P (A) = 0) \to (P = ℂ \times \{P (0)\} \to P = 0_{𝑝})$
14	13	necon3ad	$⊢ (A \in ℂ \land P (A) = 0) \to (P \neq 0_{𝑝} \to \neg P = ℂ \times \{P (0)\})$
15	14	impcom	$⊢ (P \neq 0_{𝑝} \land (A \in ℂ \land P (A) = 0)) \to \neg P = ℂ \times \{P (0)\}$
16	15	adantll	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to \neg P = ℂ \times \{P (0)\}$
17		0dgrb	$⊢ P \in Poly (S) \to (\deg (P) = 0 \leftrightarrow P = ℂ \times \{P (0)\})$
18	17	ad2antrr	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to (\deg (P) = 0 \leftrightarrow P = ℂ \times \{P (0)\})$
19	16 18	mtbird	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to \neg \deg (P) = 0$
20		dgrcl	$⊢ P \in Poly (S) \to \deg (P) \in ℕ_{0}$
21	20	ad2antrr	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to \deg (P) \in ℕ_{0}$
22		elnn0	$⊢ \deg (P) \in ℕ_{0} \leftrightarrow (\deg (P) \in ℕ \lor \deg (P) = 0)$
23	21 22	sylib	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to (\deg (P) \in ℕ \lor \deg (P) = 0)$
24		orel2	$⊢ \neg \deg (P) = 0 \to ((\deg (P) \in ℕ \lor \deg (P) = 0) \to \deg (P) \in ℕ)$
25	19 23 24	sylc	$⊢ ((P \in Poly (S) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to \deg (P) \in ℕ$

Metamath Proof Explorer

Theorem dgrnznn

Proof