dgreq0

Description: The leading coefficient of a polynomial is nonzero, unless the entire polynomial is zero. (Contributed by Mario Carneiro, 22-Jul-2014) (Proof shortened by Fan Zheng, 21-Jun-2016)

	Ref	Expression
Hypotheses	dgreq0.1	$⊢ N = \deg (F)$
	dgreq0.2	$⊢ A = coeff (F)$
Assertion	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$

Proof

Step	Hyp	Ref	Expression
1		dgreq0.1	$⊢ N = \deg (F)$
2		dgreq0.2	$⊢ A = coeff (F)$
3		fveq2	$⊢ F = 0_{𝑝} \to coeff (F) = coeff (0_{𝑝})$
4	2 3	eqtrid	$⊢ F = 0_{𝑝} \to A = coeff (0_{𝑝})$
5		coe0	$⊢ coeff (0_{𝑝}) = ℕ_{0} \times \{0\}$
6	4 5	eqtrdi	$⊢ F = 0_{𝑝} \to A = ℕ_{0} \times \{0\}$
7		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
8	1 7	eqtrid	$⊢ F = 0_{𝑝} \to N = \deg (0_{𝑝})$
9		dgr0	$⊢ \deg (0_{𝑝}) = 0$
10	8 9	eqtrdi	$⊢ F = 0_{𝑝} \to N = 0$
11	6 10	fveq12d	$⊢ F = 0_{𝑝} \to A (N) = (ℕ_{0} \times \{0\}) (0)$
12		0nn0	$⊢ 0 \in ℕ_{0}$
13		fvconst2g	$⊢ (0 \in ℕ_{0} \land 0 \in ℕ_{0}) \to (ℕ_{0} \times \{0\}) (0) = 0$
14	12 12 13	mp2an	$⊢ (ℕ_{0} \times \{0\}) (0) = 0$
15	11 14	eqtrdi	$⊢ F = 0_{𝑝} \to A (N) = 0$
16	2	coefv0	$⊢ F \in Poly (S) \to F (0) = A (0)$
17	16	adantr	$⊢ (F \in Poly (S) \land A (N) = 0) \to F (0) = A (0)$
18		simpr	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N \in ℕ$
19	18	nnred	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N \in ℝ$
20	19	ltm1d	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N - 1 < N$
21		nnre	$⊢ N \in ℕ \to N \in ℝ$
22	21	adantl	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N \in ℝ$
23		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
24	22 23	syl	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N - 1 \in ℝ$
25		simpll	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to F \in Poly (S)$
26		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
27	26	adantl	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N - 1 \in ℕ_{0}$
28	2 1	dgrub	$⊢ (F \in Poly (S) \land k \in ℕ_{0} \land A (k) \neq 0) \to k \leq N$
29	28	3expia	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq N)$
30	29	ad2ant2rl	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (A (k) \neq 0 \to k \leq N)$
31		simplr	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to A (N) = 0$
32		fveqeq2	$⊢ N = k \to (A (N) = 0 \leftrightarrow A (k) = 0)$
33	31 32	syl5ibcom	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (N = k \to A (k) = 0)$
34	33	necon3d	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (A (k) \neq 0 \to N \neq k)$
35	30 34	jcad	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (A (k) \neq 0 \to (k \leq N \land N \neq k))$
36		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
37	36	ad2antll	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to k \in ℝ$
38	21	ad2antrl	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to N \in ℝ$
39	37 38	ltlend	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (k < N \leftrightarrow (k \leq N \land N \neq k))$
40		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
41	40	ad2antll	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to k \in ℤ$
42		nnz	$⊢ N \in ℕ \to N \in ℤ$
43	42	ad2antrl	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to N \in ℤ$
44		zltlem1	$⊢ (k \in ℤ \land N \in ℤ) \to (k < N \leftrightarrow k \leq N - 1)$
45	41 43 44	syl2anc	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (k < N \leftrightarrow k \leq N - 1)$
46	39 45	bitr3d	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to ((k \leq N \land N \neq k) \leftrightarrow k \leq N - 1)$
47	35 46	sylibd	$⊢ ((F \in Poly (S) \land A (N) = 0) \land (N \in ℕ \land k \in ℕ_{0})) \to (A (k) \neq 0 \to k \leq N - 1)$
48	47	expr	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to (k \in ℕ_{0} \to (A (k) \neq 0 \to k \leq N - 1))$
49	48	ralrimiv	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N - 1)$
50	2	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
51	50	ad2antrr	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to A : ℕ_{0} ⟶ ℂ$
52		plyco0	$⊢ (N - 1 \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (N - 1 + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N - 1))$
53	27 51 52	syl2anc	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to (A [ℤ_{\geq (N - 1 + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N - 1))$
54	49 53	mpbird	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to A [ℤ_{\geq (N - 1 + 1)}] = \{0\}$
55	2 1	dgrlb	$⊢ (F \in Poly (S) \land N - 1 \in ℕ_{0} \land A [ℤ_{\geq (N - 1 + 1)}] = \{0\}) \to N \leq N - 1$
56	25 27 54 55	syl3anc	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to N \leq N - 1$
57	22 24 56	lensymd	$⊢ ((F \in Poly (S) \land A (N) = 0) \land N \in ℕ) \to \neg N - 1 < N$
58	20 57	pm2.65da	$⊢ (F \in Poly (S) \land A (N) = 0) \to \neg N \in ℕ$
59		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
60	1 59	eqeltrid	$⊢ F \in Poly (S) \to N \in ℕ_{0}$
61	60	adantr	$⊢ (F \in Poly (S) \land A (N) = 0) \to N \in ℕ_{0}$
62		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
63	61 62	sylib	$⊢ (F \in Poly (S) \land A (N) = 0) \to (N \in ℕ \lor N = 0)$
64	63	ord	$⊢ (F \in Poly (S) \land A (N) = 0) \to (\neg N \in ℕ \to N = 0)$
65	58 64	mpd	$⊢ (F \in Poly (S) \land A (N) = 0) \to N = 0$
66	65	fveq2d	$⊢ (F \in Poly (S) \land A (N) = 0) \to A (N) = A (0)$
67		simpr	$⊢ (F \in Poly (S) \land A (N) = 0) \to A (N) = 0$
68	17 66 67	3eqtr2d	$⊢ (F \in Poly (S) \land A (N) = 0) \to F (0) = 0$
69	68	sneqd	$⊢ (F \in Poly (S) \land A (N) = 0) \to \{F (0)\} = \{0\}$
70	69	xpeq2d	$⊢ (F \in Poly (S) \land A (N) = 0) \to ℂ \times \{F (0)\} = ℂ \times \{0\}$
71	1 65	eqtr3id	$⊢ (F \in Poly (S) \land A (N) = 0) \to \deg (F) = 0$
72		0dgrb	$⊢ F \in Poly (S) \to (\deg (F) = 0 \leftrightarrow F = ℂ \times \{F (0)\})$
73	72	adantr	$⊢ (F \in Poly (S) \land A (N) = 0) \to (\deg (F) = 0 \leftrightarrow F = ℂ \times \{F (0)\})$
74	71 73	mpbid	$⊢ (F \in Poly (S) \land A (N) = 0) \to F = ℂ \times \{F (0)\}$
75		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
76	75	a1i	$⊢ (F \in Poly (S) \land A (N) = 0) \to 0_{𝑝} = ℂ \times \{0\}$
77	70 74 76	3eqtr4d	$⊢ (F \in Poly (S) \land A (N) = 0) \to F = 0_{𝑝}$
78	77	ex	$⊢ F \in Poly (S) \to (A (N) = 0 \to F = 0_{𝑝})$
79	15 78	impbid2	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$

Metamath Proof Explorer

Theorem dgreq0

Proof