dgraa0p

Description: A rational polynomial of degree less than an algebraic number cannot be zero at that number unless it is the zero polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014)

		Ref	Expression
	Assertion	dgraa0p	$⊢ (A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \to (P (A) = 0 \leftrightarrow P = 0_{𝑝})$

Proof

Step	Hyp	Ref	Expression
1		simpl3	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \deg (P) < \deg_{𝔸} (A)$
2		simpl2	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to P \in Poly (ℚ)$
3		dgrcl	$⊢ P \in Poly (ℚ) \to \deg (P) \in ℕ_{0}$
4	2 3	syl	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \deg (P) \in ℕ_{0}$
5	4	nn0red	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \deg (P) \in ℝ$
6		simpl1	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to A \in 𝔸$
7		dgraacl	$⊢ A \in 𝔸 \to \deg_{𝔸} (A) \in ℕ$
8	6 7	syl	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \deg_{𝔸} (A) \in ℕ$
9	8	nnred	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \deg_{𝔸} (A) \in ℝ$
10	5 9	ltnled	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to (\deg (P) < \deg_{𝔸} (A) \leftrightarrow \neg \deg_{𝔸} (A) \leq \deg (P))$
11	1 10	mpbid	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \neg \deg_{𝔸} (A) \leq \deg (P)$
12		simpl2	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land (P \neq 0_{𝑝} \land P (A) = 0)) \to P \in Poly (ℚ)$
13		simprl	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land (P \neq 0_{𝑝} \land P (A) = 0)) \to P \neq 0_{𝑝}$
14		simpl1	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land (P \neq 0_{𝑝} \land P (A) = 0)) \to A \in 𝔸$
15		aacn	$⊢ A \in 𝔸 \to A \in ℂ$
16	14 15	syl	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land (P \neq 0_{𝑝} \land P (A) = 0)) \to A \in ℂ$
17		simprr	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land (P \neq 0_{𝑝} \land P (A) = 0)) \to P (A) = 0$
18		dgraaub	$⊢ ((P \in Poly (ℚ) \land P \neq 0_{𝑝}) \land (A \in ℂ \land P (A) = 0)) \to \deg_{𝔸} (A) \leq \deg (P)$
19	12 13 16 17 18	syl22anc	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land (P \neq 0_{𝑝} \land P (A) = 0)) \to \deg_{𝔸} (A) \leq \deg (P)$
20	19	expr	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to (P (A) = 0 \to \deg_{𝔸} (A) \leq \deg (P))$
21	11 20	mtod	$⊢ ((A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \land P \neq 0_{𝑝}) \to \neg P (A) = 0$
22	21	ex	$⊢ (A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \to (P \neq 0_{𝑝} \to \neg P (A) = 0)$
23	22	necon4ad	$⊢ (A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \to (P (A) = 0 \to P = 0_{𝑝})$
24		0pval	$⊢ A \in ℂ \to 0_{𝑝} (A) = 0$
25	15 24	syl	$⊢ A \in 𝔸 \to 0_{𝑝} (A) = 0$
26		fveq1	$⊢ P = 0_{𝑝} \to P (A) = 0_{𝑝} (A)$
27	26	eqeq1d	$⊢ P = 0_{𝑝} \to (P (A) = 0 \leftrightarrow 0_{𝑝} (A) = 0)$
28	25 27	syl5ibrcom	$⊢ A \in 𝔸 \to (P = 0_{𝑝} \to P (A) = 0)$
29	28	3ad2ant1	$⊢ (A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \to (P = 0_{𝑝} \to P (A) = 0)$
30	23 29	impbid	$⊢ (A \in 𝔸 \land P \in Poly (ℚ) \land \deg (P) < \deg_{𝔸} (A)) \to (P (A) = 0 \leftrightarrow P = 0_{𝑝})$

Metamath Proof Explorer

Theorem dgraa0p

Proof