Theorem 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	⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) → ( ( 𝑃 ‘ 𝐴 ) = 0 ↔ 𝑃 = 0𝑝 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl3	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) )
2		simpl2	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → 𝑃 ∈ ( Poly ‘ ℚ ) )
3		dgrcl	⊢ ( 𝑃 ∈ ( Poly ‘ ℚ ) → ( deg ‘ 𝑃 ) ∈ ℕ0 )
4	2 3	syl	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( deg ‘ 𝑃 ) ∈ ℕ0 )
5	4	nn0red	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( deg ‘ 𝑃 ) ∈ ℝ )
6		simpl1	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → 𝐴 ∈ 𝔸 )
7		dgraacl	⊢ ( 𝐴 ∈ 𝔸 → ( degAA ‘ 𝐴 ) ∈ ℕ )
8	6 7	syl	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( degAA ‘ 𝐴 ) ∈ ℕ )
9	8	nnred	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( degAA ‘ 𝐴 ) ∈ ℝ )
10	5 9	ltnled	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ↔ ¬ ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) ) )
11	1 10	mpbid	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ¬ ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) )
12		simpl2	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ ( 𝑃 ≠ 0𝑝 ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝑃 ∈ ( Poly ‘ ℚ ) )
13		simprl	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ ( 𝑃 ≠ 0𝑝 ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝑃 ≠ 0𝑝 )
14		simpl1	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ ( 𝑃 ≠ 0𝑝 ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ 𝔸 )
15		aacn	⊢ ( 𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ )
16	14 15	syl	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ ( 𝑃 ≠ 0𝑝 ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ ℂ )
17		simprr	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ ( 𝑃 ≠ 0𝑝 ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( 𝑃 ‘ 𝐴 ) = 0 )
18		dgraaub	⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) )
19	12 13 16 17 18	syl22anc	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ ( 𝑃 ≠ 0𝑝 ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) )
20	19	expr	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ( ( 𝑃 ‘ 𝐴 ) = 0 → ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) ) )
21	11 20	mtod	⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) ∧ 𝑃 ≠ 0𝑝 ) → ¬ ( 𝑃 ‘ 𝐴 ) = 0 )
22	21	ex	⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) → ( 𝑃 ≠ 0𝑝 → ¬ ( 𝑃 ‘ 𝐴 ) = 0 ) )
23	22	necon4ad	⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) → ( ( 𝑃 ‘ 𝐴 ) = 0 → 𝑃 = 0𝑝 ) )
24		0pval	⊢ ( 𝐴 ∈ ℂ → ( 0𝑝 ‘ 𝐴 ) = 0 )
25	15 24	syl	⊢ ( 𝐴 ∈ 𝔸 → ( 0𝑝 ‘ 𝐴 ) = 0 )
26		fveq1	⊢ ( 𝑃 = 0𝑝 → ( 𝑃 ‘ 𝐴 ) = ( 0𝑝 ‘ 𝐴 ) )
27	26	eqeq1d	⊢ ( 𝑃 = 0𝑝 → ( ( 𝑃 ‘ 𝐴 ) = 0 ↔ ( 0𝑝 ‘ 𝐴 ) = 0 ) )
28	25 27	syl5ibrcom	⊢ ( 𝐴 ∈ 𝔸 → ( 𝑃 = 0𝑝 → ( 𝑃 ‘ 𝐴 ) = 0 ) )
29	28	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) → ( 𝑃 = 0𝑝 → ( 𝑃 ‘ 𝐴 ) = 0 ) )
30	23 29	impbid	⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝑃 ∈ ( Poly ‘ ℚ ) ∧ ( deg ‘ 𝑃 ) < ( degAA ‘ 𝐴 ) ) → ( ( 𝑃 ‘ 𝐴 ) = 0 ↔ 𝑃 = 0𝑝 ) )