dgrlt

Description: Two ways to say that the degree of F is strictly less than N . (Contributed by Mario Carneiro, 25-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dgreq0.1	$⊢ N = \deg (F)$
2		dgreq0.2	$⊢ A = coeff (F)$
3		simpr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to F = 0_{𝑝}$
4	3	fveq2d	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to \deg (F) = \deg (0_{𝑝})$
5		dgr0	$⊢ \deg (0_{𝑝}) = 0$
6	5	eqcomi	$⊢ 0 = \deg (0_{𝑝})$
7	4 1 6	3eqtr4g	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to N = 0$
8		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
9	8	ad2antlr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to 0 \leq M$
10	7 9	eqbrtrd	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to N \leq M$
11	3	fveq2d	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to coeff (F) = coeff (0_{𝑝})$
12		coe0	$⊢ coeff (0_{𝑝}) = ℕ_{0} \times \{0\}$
13	12	eqcomi	$⊢ ℕ_{0} \times \{0\} = coeff (0_{𝑝})$
14	11 2 13	3eqtr4g	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to A = ℕ_{0} \times \{0\}$
15	14	fveq1d	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to A (M) = (ℕ_{0} \times \{0\}) (M)$
16		c0ex	$⊢ 0 \in V$
17	16	fvconst2	$⊢ M \in ℕ_{0} \to (ℕ_{0} \times \{0\}) (M) = 0$
18	17	ad2antlr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to (ℕ_{0} \times \{0\}) (M) = 0$
19	15 18	eqtrd	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to A (M) = 0$
20	10 19	jca	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land F = 0_{𝑝}) \to (N \leq M \land A (M) = 0)$
21		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
22	1 21	eqeltrid	$⊢ F \in Poly (S) \to N \in ℕ_{0}$
23	22	nn0red	$⊢ F \in Poly (S) \to N \in ℝ$
24		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
25		ltle	$⊢ (N \in ℝ \land M \in ℝ) \to (N < M \to N \leq M)$
26	23 24 25	syl2an	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to (N < M \to N \leq M)$
27	26	imp	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land N < M) \to N \leq M$
28	2 1	dgrub	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A (M) \neq 0) \to M \leq N$
29	28	3expia	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to (A (M) \neq 0 \to M \leq N)$
30		lenlt	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow \neg N < M)$
31	24 23 30	syl2anr	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to (M \leq N \leftrightarrow \neg N < M)$
32	29 31	sylibd	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to (A (M) \neq 0 \to \neg N < M)$
33	32	necon4ad	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to (N < M \to A (M) = 0)$
34	33	imp	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land N < M) \to A (M) = 0$
35	27 34	jca	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land N < M) \to (N \leq M \land A (M) = 0)$
36	20 35	jaodan	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (F = 0_{𝑝} \lor N < M)) \to (N \leq M \land A (M) = 0)$
37		leloe	$⊢ (N \in ℝ \land M \in ℝ) \to (N \leq M \leftrightarrow (N < M \lor N = M))$
38	23 24 37	syl2an	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to (N \leq M \leftrightarrow (N < M \lor N = M))$
39	38	biimpa	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land N \leq M) \to (N < M \lor N = M)$
40	39	adantrr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (N < M \lor N = M)$
41		fveq2	$⊢ N = M \to A (N) = A (M)$
42	1 2	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
43	42	ad2antrr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
44		simprr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to A (M) = 0$
45	44	eqeq2d	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (A (N) = A (M) \leftrightarrow A (N) = 0)$
46	43 45	bitr4d	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (F = 0_{𝑝} \leftrightarrow A (N) = A (M))$
47	41 46	syl5ibr	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (N = M \to F = 0_{𝑝})$
48	47	orim2d	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to ((N < M \lor N = M) \to (N < M \lor F = 0_{𝑝}))$
49	40 48	mpd	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (N < M \lor F = 0_{𝑝})$
50	49	orcomd	$⊢ ((F \in Poly (S) \land M \in ℕ_{0}) \land (N \leq M \land A (M) = 0)) \to (F = 0_{𝑝} \lor N < M)$
51	36 50	impbida	$⊢ (F \in Poly (S) \land M \in ℕ_{0}) \to ((F = 0_{𝑝} \lor N < M) \leftrightarrow (N \leq M \land A (M) = 0))$

Metamath Proof Explorer

Theorem dgrlt

Proof