rnplynfin

Description: The range of a nonconstant polynomial is not a finite set. (Contributed by SN, 30-Aug-2026)

	Ref	Expression
Hypotheses	rnplynfin.f	$⊢ φ \to F \in Poly (S)$
	rnplynfin.1	$⊢ φ \to \deg (F) \neq 0$
Assertion	rnplynfin	$⊢ φ \to \neg ran F \in Fin$

Proof

Step	Hyp	Ref	Expression
1		rnplynfin.f	$⊢ φ \to F \in Poly (S)$
2		rnplynfin.1	$⊢ φ \to \deg (F) \neq 0$
3		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
4	1 3	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
5	4	frnd	$⊢ φ \to ran F \subseteq ℂ$
6		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
7	6 1	sselid	$⊢ φ \to F \in Poly (ℂ)$
8	7	adantr	$⊢ (φ \land x \in ℂ) \to F \in Poly (ℂ)$
9		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
10		plyconst	$⊢ (ℂ \subseteq ℂ \land x \in ℂ) \to ℂ \times \{x\} \in Poly (ℂ)$
11	9 10	sylan	$⊢ (φ \land x \in ℂ) \to ℂ \times \{x\} \in Poly (ℂ)$
12		plysubcl	$⊢ (F \in Poly (ℂ) \land ℂ \times \{x\} \in Poly (ℂ)) \to F -_{f} (ℂ \times \{x\}) \in Poly (ℂ)$
13	8 11 12	syl2anc	$⊢ (φ \land x \in ℂ) \to F -_{f} (ℂ \times \{x\}) \in Poly (ℂ)$
14	2	neneqd	$⊢ φ \to \neg \deg (F) = 0$
15	14	adantr	$⊢ (φ \land x \in ℂ) \to \neg \deg (F) = 0$
16		0dgr	$⊢ x \in ℂ \to \deg (ℂ \times \{x\}) = 0$
17	16	adantl	$⊢ (φ \land x \in ℂ) \to \deg (ℂ \times \{x\}) = 0$
18		fveqeq2	$⊢ F = ℂ \times \{x\} \to (\deg (F) = 0 \leftrightarrow \deg (ℂ \times \{x\}) = 0)$
19	17 18	syl5ibrcom	$⊢ (φ \land x \in ℂ) \to (F = ℂ \times \{x\} \to \deg (F) = 0)$
20	15 19	mtod	$⊢ (φ \land x \in ℂ) \to \neg F = ℂ \times \{x\}$
21		vex	$⊢ x \in V$
22	21	fconst2	$⊢ F : ℂ ⟶ \{x\} \leftrightarrow F = ℂ \times \{x\}$
23	20 22	sylnibr	$⊢ (φ \land x \in ℂ) \to \neg F : ℂ ⟶ \{x\}$
24	4	ffnd	$⊢ φ \to F Fn ℂ$
25	24	adantr	$⊢ (φ \land x \in ℂ) \to F Fn ℂ$
26	25	adantr	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℂ F (y) = x) \to F Fn ℂ$
27		simpr	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℂ F (y) = x) \to \forall y \in ℂ F (y) = x$
28		fconstfv	$⊢ F : ℂ ⟶ \{x\} \leftrightarrow (F Fn ℂ \land \forall y \in ℂ F (y) = x)$
29	26 27 28	sylanbrc	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℂ F (y) = x) \to F : ℂ ⟶ \{x\}$
30	23 29	mtand	$⊢ (φ \land x \in ℂ) \to \neg \forall y \in ℂ F (y) = x$
31		rexnal	$⊢ \exists y \in ℂ \neg F (y) = x \leftrightarrow \neg \forall y \in ℂ F (y) = x$
32	30 31	sylibr	$⊢ (φ \land x \in ℂ) \to \exists y \in ℂ \neg F (y) = x$
33		cnex	$⊢ ℂ \in V$
34	33	a1i	$⊢ (φ \land x \in ℂ) \to ℂ \in V$
35		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
36		eqidd	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to F (y) = F (y)$
37	34 35 25 36	ofc2	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to (F -_{f} (ℂ \times \{x\})) (y) = F (y) - x$
38	37	neeq1d	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to ((F -_{f} (ℂ \times \{x\})) (y) \neq 0 \leftrightarrow F (y) - x \neq 0)$
39	4	ffvelcdmda	$⊢ (φ \land y \in ℂ) \to F (y) \in ℂ$
40	39	adantlr	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to F (y) \in ℂ$
41		simplr	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to x \in ℂ$
42	40 41	subeq0ad	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to (F (y) - x = 0 \leftrightarrow F (y) = x)$
43	42	necon3bid	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to (F (y) - x \neq 0 \leftrightarrow F (y) \neq x)$
44		df-ne	$⊢ F (y) \neq x \leftrightarrow \neg F (y) = x$
45	44	a1i	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to (F (y) \neq x \leftrightarrow \neg F (y) = x)$
46	38 43 45	3bitrd	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to ((F -_{f} (ℂ \times \{x\})) (y) \neq 0 \leftrightarrow \neg F (y) = x)$
47	46	rexbidva	$⊢ (φ \land x \in ℂ) \to (\exists y \in ℂ (F -_{f} (ℂ \times \{x\})) (y) \neq 0 \leftrightarrow \exists y \in ℂ \neg F (y) = x)$
48	32 47	mpbird	$⊢ (φ \land x \in ℂ) \to \exists y \in ℂ (F -_{f} (ℂ \times \{x\})) (y) \neq 0$
49		ne0p	$⊢ (y \in ℂ \land (F -_{f} (ℂ \times \{x\})) (y) \neq 0) \to F -_{f} (ℂ \times \{x\}) \neq 0_{𝑝}$
50	49	rexlimiva	$⊢ \exists y \in ℂ (F -_{f} (ℂ \times \{x\})) (y) \neq 0 \to F -_{f} (ℂ \times \{x\}) \neq 0_{𝑝}$
51	48 50	syl	$⊢ (φ \land x \in ℂ) \to F -_{f} (ℂ \times \{x\}) \neq 0_{𝑝}$
52		eqid	$⊢ {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] = {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}]$
53	52	fta1	$⊢ (F -_{f} (ℂ \times \{x\}) \in Poly (ℂ) \land F -_{f} (ℂ \times \{x\}) \neq 0_{𝑝}) \to ({(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \in Fin \land \|{(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}]\| \leq \deg (F -_{f} (ℂ \times \{x\})))$
54	13 51 53	syl2anc	$⊢ (φ \land x \in ℂ) \to ({(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \in Fin \land \|{(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}]\| \leq \deg (F -_{f} (ℂ \times \{x\})))$
55	54	simpld	$⊢ (φ \land x \in ℂ) \to {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \in Fin$
56	55	ralrimiva	$⊢ φ \to \forall x \in ℂ {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \in Fin$
57		fnconstg	$⊢ x \in ℂ \to (ℂ \times \{x\}) Fn ℂ$
58	57	adantl	$⊢ (φ \land x \in ℂ) \to (ℂ \times \{x\}) Fn ℂ$
59		inidm	$⊢ ℂ \cap ℂ = ℂ$
60	21	fvconst2	$⊢ y \in ℂ \to (ℂ \times \{x\}) (y) = x$
61	60	adantl	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to (ℂ \times \{x\}) (y) = x$
62	25 58 34 34 59 36 61	ofval	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to (F -_{f} (ℂ \times \{x\})) (y) = F (y) - x$
63	62	eqeq1d	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to ((F -_{f} (ℂ \times \{x\})) (y) = 0 \leftrightarrow F (y) - x = 0)$
64	63 42	bitrd	$⊢ ((φ \land x \in ℂ) \land y \in ℂ) \to ((F -_{f} (ℂ \times \{x\})) (y) = 0 \leftrightarrow F (y) = x)$
65	64	pm5.32da	$⊢ (φ \land x \in ℂ) \to ((y \in ℂ \land (F -_{f} (ℂ \times \{x\})) (y) = 0) \leftrightarrow (y \in ℂ \land F (y) = x))$
66	25 58 34 34 59	offn	$⊢ (φ \land x \in ℂ) \to (F -_{f} (ℂ \times \{x\})) Fn ℂ$
67		fniniseg	$⊢ (F -_{f} (ℂ \times \{x\})) Fn ℂ \to (y \in {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \leftrightarrow (y \in ℂ \land (F -_{f} (ℂ \times \{x\})) (y) = 0))$
68	66 67	syl	$⊢ (φ \land x \in ℂ) \to (y \in {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \leftrightarrow (y \in ℂ \land (F -_{f} (ℂ \times \{x\})) (y) = 0))$
69		fniniseg	$⊢ F Fn ℂ \to (y \in F^{-1} [\{x\}] \leftrightarrow (y \in ℂ \land F (y) = x))$
70	25 69	syl	$⊢ (φ \land x \in ℂ) \to (y \in F^{-1} [\{x\}] \leftrightarrow (y \in ℂ \land F (y) = x))$
71	65 68 70	3bitr4d	$⊢ (φ \land x \in ℂ) \to (y \in {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \leftrightarrow y \in F^{-1} [\{x\}])$
72	71	eqrdv	$⊢ (φ \land x \in ℂ) \to {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] = F^{-1} [\{x\}]$
73	72	eleq1d	$⊢ (φ \land x \in ℂ) \to ({(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \in Fin \leftrightarrow F^{-1} [\{x\}] \in Fin)$
74	73	ralbidva	$⊢ φ \to (\forall x \in ℂ {(F -_{f} (ℂ \times \{x\}))}^{-1} [\{0\}] \in Fin \leftrightarrow \forall x \in ℂ F^{-1} [\{x\}] \in Fin)$
75	56 74	mpbid	$⊢ φ \to \forall x \in ℂ F^{-1} [\{x\}] \in Fin$
76		ssralv	$⊢ ran F \subseteq ℂ \to (\forall x \in ℂ F^{-1} [\{x\}] \in Fin \to \forall x \in ran F F^{-1} [\{x\}] \in Fin)$
77	5 75 76	sylc	$⊢ φ \to \forall x \in ran F F^{-1} [\{x\}] \in Fin$
78	4	fdmd	$⊢ φ \to dom F = ℂ$
79		nnnfi	$⊢ \neg ℕ \in Fin$
80		nnsscn	$⊢ ℕ \subseteq ℂ$
81		ssfi	$⊢ (ℂ \in Fin \land ℕ \subseteq ℂ) \to ℕ \in Fin$
82	80 81	mpan2	$⊢ ℂ \in Fin \to ℕ \in Fin$
83	79 82	mto	$⊢ \neg ℂ \in Fin$
84	83	a1i	$⊢ φ \to \neg ℂ \in Fin$
85	78 84	eqneltrd	$⊢ φ \to \neg dom F \in Fin$
86	85	adantr	$⊢ (φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \to \neg dom F \in Fin$
87	4	ffund	$⊢ φ \to Fun F$
88		iunpreima	$⊢ Fun F \to F^{-1} [⋃_{x \in ran F} \{x\}] = ⋃_{x \in ran F} F^{-1} [\{x\}]$
89	87 88	syl	$⊢ φ \to F^{-1} [⋃_{x \in ran F} \{x\}] = ⋃_{x \in ran F} F^{-1} [\{x\}]$
90		iunid	$⊢ ⋃_{x \in ran F} \{x\} = ran F$
91	90	imaeq2i	$⊢ F^{-1} [⋃_{x \in ran F} \{x\}] = F^{-1} [ran F]$
92		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
93	91 92	eqtri	$⊢ F^{-1} [⋃_{x \in ran F} \{x\}] = dom F$
94	89 93	eqtr3di	$⊢ φ \to ⋃_{x \in ran F} F^{-1} [\{x\}] = dom F$
95	94	ad2antrr	$⊢ ((φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \land ran F \in Fin) \to ⋃_{x \in ran F} F^{-1} [\{x\}] = dom F$
96		simpr	$⊢ ((φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \land ran F \in Fin) \to ran F \in Fin$
97		simplr	$⊢ ((φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \land ran F \in Fin) \to \forall x \in ran F F^{-1} [\{x\}] \in Fin$
98		iunfi	$⊢ (ran F \in Fin \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \to ⋃_{x \in ran F} F^{-1} [\{x\}] \in Fin$
99	96 97 98	syl2anc	$⊢ ((φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \land ran F \in Fin) \to ⋃_{x \in ran F} F^{-1} [\{x\}] \in Fin$
100	95 99	eqeltrrd	$⊢ ((φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \land ran F \in Fin) \to dom F \in Fin$
101	86 100	mtand	$⊢ (φ \land \forall x \in ran F F^{-1} [\{x\}] \in Fin) \to \neg ran F \in Fin$
102	77 101	mpdan	$⊢ φ \to \neg ran F \in Fin$

Metamath Proof Explorer

Theorem rnplynfin

Proof