ply1degleel

Description: Characterize elementhood in the set S of polynomials of degree less than N . (Contributed by Thierry Arnoux, 2-Apr-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	ply1degleel	$⊢ φ \to (F \in S \leftrightarrow (F \in B \land D (F) < N))$

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	19	adantr	$⊢ (φ \land F = 0_{P}) \to N \in ℝ$
38	37	mnfltd	$⊢ (φ \land F = 0_{P}) \to −∞ < N$
39	36 38	eqbrtrd	$⊢ (φ \land F = 0_{P}) \to D (F) < N$
40		pm5.1	$⊢ (F \in S \land (F \in B \land D (F) < N)) \to (F \in S \leftrightarrow (F \in B \land D (F) < N))$
41	28 33 39 40	syl12anc	$⊢ (φ \land F = 0_{P}) \to (F \in S \leftrightarrow (F \in B \land D (F) < N))$
42	3	eleq2i	$⊢ F \in S \leftrightarrow F \in D^{-1} [[−∞, N)]$
43	10	adantr	$⊢ (φ \land F \neq 0_{P}) \to D Fn B$
44		elpreima	$⊢ D Fn B \to (F \in D^{-1} [[−∞, N)] \leftrightarrow (F \in B \land D (F) \in [−∞, N)))$
45	43 44	syl	$⊢ (φ \land F \neq 0_{P}) \to (F \in D^{-1} [[−∞, N)] \leftrightarrow (F \in B \land D (F) \in [−∞, N)))$
46	42 45	bitrid	$⊢ (φ \land F \neq 0_{P}) \to (F \in S \leftrightarrow (F \in B \land D (F) \in [−∞, N)))$
47	5	ad2antrr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to R \in Ring$
48		simpr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to F \in B$
49		simplr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to F \neq 0_{P}$
50	2 1 12 6	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq 0_{P}) \to D (F) \in ℕ_{0}$
51	47 48 49 50	syl3anc	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℕ_{0}$
52	51	nn0red	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℝ$
53	52	rexrd	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to D (F) \in ℝ^{*}$
54	53	mnfled	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to −∞ \leq D (F)$
55	53 54	jca	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) \in ℝ^{*} \land −∞ \leq D (F))$
56	20	ad2antrr	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to N \in ℝ^{*}$
57		elico1	$⊢ (−∞ \in ℝ^{} \land N \in ℝ^{}) \to (D (F) \in [−∞, N) \leftrightarrow (D (F) \in ℝ^{*} \land −∞ \leq D (F) \land D (F) < N))$
58	17 56 57	sylancr	$⊢ ((φ \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))$
59		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)$
60	58 59	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))$
61	55 60	mpbirand	$⊢ ((φ \land F \neq 0_{P}) \land F \in B) \to (D (F) \in [−∞, N) \leftrightarrow D (F) < N)$
62	61	pm5.32da	$⊢ (φ \land F \neq 0_{P}) \to ((F \in B \land D (F) \in [−∞, N)) \leftrightarrow (F \in B \land D (F) < N))$
63	46 62	bitrd	$⊢ (φ \land F \neq 0_{P}) \to (F \in S \leftrightarrow (F \in B \land D (F) < N))$
64	41 63	pm2.61dane	$⊢ φ \to (F \in S \leftrightarrow (F \in B \land D (F) < N))$

Metamath Proof Explorer

Theorem ply1degleel

Proof