Metamath Proof Explorer

Theorem rnplynfin

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

Ref Expression
Hypotheses rnplynfin.f 
|- ( ph -> F e. ( Poly ` S ) )
rnplynfin.1 
|- ( ph -> ( deg ` F ) =/= 0 )
Assertion rnplynfin 
|- ( ph -> -. ran F e. Fin )

Proof

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