dgrlb

Description: If all the coefficients above M are zero, then the degree of F is at most M . (Contributed by Mario Carneiro, 22-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$⊢ A = coeff (F)$
2		dgrub.2	$⊢ N = \deg (F)$
3		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
4	2 3	eqeltrid	$⊢ F \in Poly (S) \to N \in ℕ_{0}$
5	4	3ad2ant1	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to N \in ℕ_{0}$
6	5	nn0red	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to N \in ℝ$
7		simp2	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to M \in ℕ_{0}$
8	7	nn0red	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to M \in ℝ$
9	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)$
10	9	simpld	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ S \cup \{0\}$
11	10	3ad2ant1	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to A : ℕ_{0} ⟶ S \cup \{0\}$
12		ffn	$⊢ A : ℕ_{0} ⟶ S \cup \{0\} \to A Fn ℕ_{0}$
13		elpreima	$⊢ A Fn ℕ_{0} \to (y \in A^{-1} [ℂ ∖ \{0\}] \leftrightarrow (y \in ℕ_{0} \land A (y) \in (ℂ ∖ \{0\})))$
14	11 12 13	3syl	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to (y \in A^{-1} [ℂ ∖ \{0\}] \leftrightarrow (y \in ℕ_{0} \land A (y) \in (ℂ ∖ \{0\})))$
15	14	biimpa	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to (y \in ℕ_{0} \land A (y) \in (ℂ ∖ \{0\}))$
16	15	simpld	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to y \in ℕ_{0}$
17	16	nn0red	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to y \in ℝ$
18	8	adantr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to M \in ℝ$
19		eldifsni	$⊢ A (y) \in (ℂ ∖ \{0\}) \to A (y) \neq 0$
20	15 19	simpl2im	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to A (y) \neq 0$
21		simp3	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
22	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
23	22	3ad2ant1	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to A : ℕ_{0} ⟶ ℂ$
24		plyco0	$⊢ (M \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall y \in ℕ_{0} (A (y) \neq 0 \to y \leq M))$
25	7 23 24	syl2anc	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to (A [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall y \in ℕ_{0} (A (y) \neq 0 \to y \leq M))$
26	21 25	mpbid	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to \forall y \in ℕ_{0} (A (y) \neq 0 \to y \leq M)$
27	26	r19.21bi	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in ℕ_{0}) \to (A (y) \neq 0 \to y \leq M)$
28	16 27	syldan	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to (A (y) \neq 0 \to y \leq M)$
29	20 28	mpd	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to y \leq M$
30	17 18 29	lensymd	$⊢ ((F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \land y \in A^{-1} [ℂ ∖ \{0\}]) \to \neg M < y$
31	30	ralrimiva	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to \forall y \in A^{-1} [ℂ ∖ \{0\}] \neg M < y$
32		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
33		ltso	$⊢ < Or ℝ$
34		soss	$⊢ ℕ_{0} \subseteq ℝ \to (< Or ℝ \to < Or ℕ_{0})$
35	32 33 34	mp2	$⊢ < Or ℕ_{0}$
36	35	a1i	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to < Or ℕ_{0}$
37		0zd	$⊢ F \in Poly (S) \to 0 \in ℤ$
38		cnvimass	$⊢ A^{-1} [ℂ ∖ \{0\}] \subseteq dom A$
39	38 10	fssdm	$⊢ F \in Poly (S) \to A^{-1} [ℂ ∖ \{0\}] \subseteq ℕ_{0}$
40	9	simprd	$⊢ F \in Poly (S) \to \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n$
41		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
42	41	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))$
43	37 39 40 42	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))$
44	43	3ad2ant1	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \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))$
45	36 44	supnub	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to ((M \in ℕ_{0} \land \forall y \in A^{-1} [ℂ ∖ \{0\}] \neg M < y) \to \neg M < sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <))$
46	7 31 45	mp2and	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to \neg M < sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
47	1	dgrval	$⊢ F \in Poly (S) \to \deg (F) = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
48	2 47	syl5eq	$⊢ F \in Poly (S) \to N = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
49	48	3ad2ant1	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to N = sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <)$
50	49	breq2d	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to (M < N \leftrightarrow M < sup (A^{-1} [ℂ ∖ \{0\}] ℕ_{0} <))$
51	46 50	mtbird	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to \neg M < N$
52	6 8 51	nltled	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to N \leq M$

Metamath Proof Explorer

Theorem dgrlb

Proof