dgrub

Description: If the M -th coefficient of F is nonzero, then the degree of F is at least M . (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	dgrub.1	$⊢ A = coeff (F)$
	dgrub.2	$⊢ N = \deg (F)$
Assertion	dgrub	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to M \leq N$

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$⊢ A = coeff (F)$
2		dgrub.2	$⊢ N = \deg (F)$
3		simp2	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to M \in ℕ_{0}$
4	3	nn0red	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to M \in ℝ$
5		simp1	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to F \in Poly (S)$
6		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
7	2 6	eqeltrid	$⊢ F \in Poly (S) \to N \in ℕ_{0}$
8	5 7	syl	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to N \in ℕ_{0}$
9	8	nn0red	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to N \in ℝ$
10	1	dgrval	$⊢ F \in Poly (S) \to \deg (F) = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
11	2 10	eqtrid	$⊢ F \in Poly (S) \to N = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
12	5 11	syl	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to N = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
13	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
14	5 13	syl	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to A : ℕ_{0} ⟶ ℂ$
15	14 3	ffvelcdmd	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to A (M) \in ℂ$
16		simp3	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to A (M) \neq 0$
17		eldifsn	$⊢ A (M) \in (ℂ ∖ \{0\}) \leftrightarrow (A (M) \in ℂ \land A (M) \neq 0)$
18	15 16 17	sylanbrc	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to A (M) \in (ℂ ∖ \{0\})$
19	1	coef	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ S \cup \{0\}$
20		ffn	$⊢ A : ℕ_{0} ⟶ S \cup \{0\} \to A Fn ℕ_{0}$
21		elpreima	$⊢ A Fn ℕ_{0} \to (M \in A^{-1} [ℂ ∖ \{0\}] \leftrightarrow (M \in ℕ_{0} \land A (M) \in (ℂ ∖ \{0\})))$
22	5 19 20 21	4syl	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to (M \in A^{-1} [ℂ ∖ \{0\}] \leftrightarrow (M \in ℕ_{0} \land A (M) \in (ℂ ∖ \{0\})))$
23	3 18 22	mpbir2and	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to M \in A^{-1} [ℂ ∖ \{0\}]$
24		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
25		ltso	$⊢ < Or ℝ$
26		soss	$⊢ ℕ_{0} \subseteq ℝ \to (< Or ℝ \to < Or ℕ_{0})$
27	24 25 26	mp2	$⊢ < Or ℕ_{0}$
28	27	a1i	$⊢ F \in Poly (S) \to < Or ℕ_{0}$
29		0zd	$⊢ F \in Poly (S) \to 0 \in ℤ$
30		cnvimass	$⊢ A^{-1} [ℂ ∖ \{0\}] \subseteq dom A$
31	30 19	fssdm	$⊢ F \in Poly (S) \to A^{-1} [ℂ ∖ \{0\}] \subseteq ℕ_{0}$
32	1	dgrlem	$⊢ F \in Poly (S) \to (A : ℕ_{0} ⟶ S \cup \{0\} \land \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
33	32	simprd	$⊢ F \in Poly (S) \to \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n$
34		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
35	34	uzsupss	$⊢ (0 \in ℤ \land A^{-1} [ℂ ∖ \{0\}] \subseteq ℕ_{0} \land \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n) \to \exists n \in ℕ_{0} (\forall x \in A^{-1} [ℂ ∖ \{0\}] \neg n < x \land \forall x \in ℕ_{0} (x < n \to \exists y \in A^{-1} [ℂ ∖ \{0\}] x < y))$
36	29 31 33 35	syl3anc	$⊢ F \in Poly (S) \to \exists n \in ℕ_{0} (\forall x \in A^{-1} [ℂ ∖ \{0\}] \neg n < x \land \forall x \in ℕ_{0} (x < n \to \exists y \in A^{-1} [ℂ ∖ \{0\}] x < y))$
37	28 36	supub	$⊢ F \in Poly (S) \to (M \in A^{-1} [ℂ ∖ \{0\}] \to \neg sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <) < M)$
38	5 23 37	sylc	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to \neg sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <) < M$
39	12 38	eqnbrtrd	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to \neg N < M$
40	4 9 39	nltled	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to M \leq N$

Metamath Proof Explorer

Theorem dgrub

Proof