ply1degltel

Description: Characterize elementhood in the set S of polynomials of degree less than N . (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	ply1degltlss.p	$⊢ P = {Poly}_{1} (R)$
	ply1degltlss.d	$⊢ D = \deg_{1} (R)$
	ply1degltlss.1	$⊢ S = D^{-1} [[−∞, N)]$
	ply1degltlss.3	$⊢ φ \to N \in ℕ_{0}$
	ply1degltlss.2	$⊢ φ \to R \in Ring$
	ply1degltel.1	$⊢ B = {Base}_{P}$
Assertion	ply1degltel	$⊢ φ \to (F \in S \leftrightarrow (F \in B \land D (F) \leq N - 1))$

Proof

Step	Hyp	Ref	Expression
1		ply1degltlss.p	$⊢ P = {Poly}_{1} (R)$
2		ply1degltlss.d	$⊢ D = \deg_{1} (R)$
3		ply1degltlss.1	$⊢ S = D^{-1} [[−∞, N)]$
4		ply1degltlss.3	$⊢ φ \to N \in ℕ_{0}$
5		ply1degltlss.2	$⊢ φ \to R \in Ring$
6		ply1degltel.1	$⊢ B = {Base}_{P}$
7		simpr	$⊢ (φ \land F = 0_{P}) \to F = 0_{P}$
8	2 1 6	deg1xrf	$⊢ D : B ⟶ ℝ^{*}$
9	8	a1i	$⊢ φ \to D : B ⟶ ℝ^{*}$
10	9	ffnd	$⊢ φ \to D Fn B$
11	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
12		eqid	$⊢ 0_{P} = 0_{P}$
13	6 12	ring0cl	$⊢ P \in Ring \to 0_{P} \in B$
14	5 11 13	3syl	$⊢ φ \to 0_{P} \in B$
15	2 1 12	deg1z	$⊢ R \in Ring \to D (0_{P}) = −∞$
16	5 15	syl	$⊢ φ \to D (0_{P}) = −∞$
17		mnfxr	$⊢ −∞ \in ℝ^{*}$
18	17	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
19	4	nn0red	$⊢ φ \to N \in ℝ$
20	19	rexrd	$⊢ φ \to N \in ℝ^{*}$
21	18	xrleidd	$⊢ φ \to −∞ \leq −∞$
22	19	mnfltd	$⊢ φ \to −∞ < N$
23	18 20 18 21 22	elicod	$⊢ φ \to −∞ \in [−∞, N)$
24	16 23	eqeltrd	$⊢ φ \to D (0_{P}) \in [−∞, N)$
25	10 14 24	elpreimad	$⊢ φ \to 0_{P} \in D^{-1} [[−∞, N)]$
26	25 3	eleqtrrdi	$⊢ φ \to 0_{P} \in S$
27	26	adantr	$⊢ (φ \land F = 0_{P}) \to 0_{P} \in S$
28	7 27	eqeltrd	$⊢ (φ \land F = 0_{P}) \to F \in S$
29		cnvimass	$⊢ D^{-1} [[−∞, N)] \subseteq dom D$
30	3 29	eqsstri	$⊢ S \subseteq dom D$
31	8	fdmi	$⊢ dom D = B$
32	30 31	sseqtri	$⊢ S \subseteq B$
33	32 28	sselid	$⊢ (φ \land F = 0_{P}) \to F \in B$
34	7	fveq2d	$⊢ (φ \land F = 0_{P}) \to D (F) = D (0_{P})$
35	16	adantr	$⊢ (φ \land F = 0_{P}) \to D (0_{P}) = −∞$
36	34 35	eqtrd	$⊢ (φ \land F = 0_{P}) \to D (F) = −∞$
37		1red	$⊢ φ \to 1 \in ℝ$
38	19 37	resubcld	$⊢ φ \to N - 1 \in ℝ$
39	38	rexrd	$⊢ φ \to N - 1 \in ℝ^{*}$
40	39	adantr	$⊢ (φ \land F = 0_{P}) \to N - 1 \in ℝ^{*}$
41	40	mnfled	$⊢ (φ \land F = 0_{P}) \to −∞ \leq N - 1$
42	36 41	eqbrtrd	$⊢ (φ \land F = 0_{P}) \to D (F) \leq N - 1$
43		pm5.1	$⊢ (F \in S \land (F \in B \land D (F) \leq N - 1)) \to (F \in S \leftrightarrow (F \in B \land D (F) \leq N - 1))$
44	28 33 42 43	syl12anc	$⊢ (φ \land F = 0_{P}) \to (F \in S \leftrightarrow (F \in B \land D (F) \leq N - 1))$
45	3	eleq2i	$⊢ F \in S \leftrightarrow F \in D^{-1} [[−∞, N)]$
46	10	adantr	$⊢ (φ \land F \neq 0_{P}) \to D Fn B$
47		elpreima	$⊢ D Fn B \to (F \in D^{-1} [[−∞, N)] \leftrightarrow (F \in B \land D (F) \in [−∞, N)))$
48	46 47	syl	$⊢ (φ \land F \neq 0_{P}) \to (F \in D^{-1} [[−∞, N)] \leftrightarrow (F \in B \land D (F) \in [−∞, N)))$
49	45 48	bitrid	$⊢ (φ \land F \neq 0_{P}) \to (F \in S \leftrightarrow (F \in B \land D (F) \in [−∞, N)))$
50	17	a1i	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to −∞ \in ℝ^{*}$
51	20	ad2antrr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to N \in ℝ^{*}$
52		elico1	$⊢ (−∞ \in ℝ^{} \land N \in ℝ^{}) \to (D (F) \in [−∞, N) \leftrightarrow (D (F) \in ℝ^{*} \land −∞ \leq D (F) \land D (F) < N))$
53	50 51 52	syl2anc	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) \in [−∞, N) \leftrightarrow (D (F) \in ℝ^{*} \land −∞ \leq D (F) \land D (F) < N))$
54		df-3an	$⊢ (D (F) \in ℝ^{} \land −∞ \leq D (F) \land D (F) < N) \leftrightarrow ((D (F) \in ℝ^{} \land −∞ \leq D (F)) \land D (F) < N)$
55	53 54	bitrdi	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) \in [−∞, N) \leftrightarrow ((D (F) \in ℝ^{*} \land −∞ \leq D (F)) \land D (F) < N))$
56	5	ad2antrr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to R \in Ring$
57		simpr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to F \in B$
58		simplr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to F \neq 0_{P}$
59	2 1 12 6	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq 0_{P}) \to D (F) \in ℕ_{0}$
60	56 57 58 59	syl3anc	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℕ_{0}$
61	60	nn0red	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℝ$
62	61	rexrd	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℝ^{*}$
63	62	mnfled	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to −∞ \leq D (F)$
64	62 63	jca	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) \in ℝ^{*} \land −∞ \leq D (F))$
65	64	biantrurd	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) < N \leftrightarrow ((D (F) \in ℝ^{*} \land −∞ \leq D (F)) \land D (F) < N))$
66	60	nn0zd	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℤ$
67	4	nn0zd	$⊢ φ \to N \in ℤ$
68	67	ad2antrr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to N \in ℤ$
69		zltlem1	$⊢ (D (F) \in ℤ \land N \in ℤ) \to (D (F) < N \leftrightarrow D (F) \leq N - 1)$
70	66 68 69	syl2anc	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) < N \leftrightarrow D (F) \leq N - 1)$
71	55 65 70	3bitr2d	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) \in [−∞, N) \leftrightarrow D (F) \leq N - 1)$
72	71	pm5.32da	$⊢ (φ \land F \neq 0_{P}) \to ((F \in B \land D (F) \in [−∞, N)) \leftrightarrow (F \in B \land D (F) \leq N - 1))$
73	49 72	bitrd	$⊢ (φ \land F \neq 0_{P}) \to (F \in S \leftrightarrow (F \in B \land D (F) \leq N - 1))$
74	44 73	pm2.61dane	$⊢ φ \to (F \in S \leftrightarrow (F \in B \land D (F) \leq N - 1))$

Metamath Proof Explorer

Theorem ply1degltel

Proof