let f be Polynomial of INT.Ring; ( degree f > 0 implies { p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is infinite )
assume A1:
degree f > 0
; { p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is infinite
(len f) - 1 > 0
by A1, HURWITZ:def 2;
then
((len f) - 1) + 1 > 0 + 1
by XREAL_1:6;
then A2:
len f >= 1 + 1
by NAT_1:13;
per cases
( f . 0 = 0. INT.Ring or f . 0 <> 0. INT.Ring )
;
suppose A3:
f . 0 = 0. INT.Ring
;
{ p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is infinite
SetPrimes c= { p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p }
proof
let y be
object ;
TARSKI:def 3 ( not y in SetPrimes or y in { p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } )
assume
y in SetPrimes
;
y in { p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p }
then reconsider y =
y as
Prime by NEWTON:def 6;
eval (
f,
(f . 0))
= 0
by A3, POLYNOM5:31;
then
ex
x being
Element of
INT.Ring st
eval (
f,
x),
0 are_congruent_mod y
by INT_1:11;
hence
y in { p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p }
;
verum
end; hence
{ p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is
infinite
;
verum end; suppose
f . 0 <> 0. INT.Ring
;
{ p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is infinite then consider f1 being
Polynomial of
INT.Ring such that A4:
(
len f = len f1 &
f1 . 0 = 1. INT.Ring )
and
for
i being
Element of
NAT st
0 < i holds
f1 . i = (f . i) * ((power INT.Ring) . ((f . 0),(i -' 1)))
and A5:
for
x being
Element of
INT.Ring holds
eval (
f,
((f . 0) * x))
= (f . 0) * (eval (f1,x))
by Th69;
set n = the
Element of
NAT ;
ex
m being
Element of
NAT st
for
n being
Nat st
n >= m holds
|.(eval (f1,(In ((n !),INT.Ring)))).| > 1
proof
reconsider g1 =
f1 as
Polynomial of
F_Complex by ALGNUM_1:4, LIOUVIL2:7;
len f1 = len g1
by ALGNUM_1:4, LIOUVIL2:8;
then consider e being
Real such that A6:
for
z being
Element of
F_Complex st
e < |.z.| holds
|.(eval (g1,z)).| > 1
by A4, A2, Th71;
set E =
|.[/e\].| + 1;
consider n being
Element of
NAT such that A7:
(
n ! <= |.[/e\].| + 1 &
|.[/e\].| + 1
< (n + 1) ! & ( for
m being
Element of
NAT st
m ! <= |.[/e\].| + 1 &
|.[/e\].| + 1
< (m + 1) ! holds
m = n ) )
by NAT_1:14, ASYMPT_1:57;
take N =
n + 1;
for n being Nat st n >= N holds
|.(eval (f1,(In ((n !),INT.Ring)))).| > 1
let i be
Nat;
( i >= N implies |.(eval (f1,(In ((i !),INT.Ring)))).| > 1 )
assume A8:
i >= N
;
|.(eval (f1,(In ((i !),INT.Ring)))).| > 1
i ! >= N !
by A8, ASYMPT_1:56;
then A9:
i ! > |.[/e\].| + 1
by A7, XXREAL_0:2;
(
e <= [/e\] &
[/e\] <= |.[/e\].| )
by INT_1:def 7, COMPLEX1:76;
then
(
e <= |.[/e\].| &
|.[/e\].| < |.[/e\].| + 1 )
by NAT_1:13, XXREAL_0:2;
then A10:
e < |.[/e\].| + 1
by XXREAL_0:2;
i ! in COMPLEX
by XCMPLX_0:def 2;
then A11:
i ! in the
carrier of
F_Complex
by COMPLFLD:def 1;
then
i ! = In (
(i !),
F_Complex)
by SUBSET_1:def 8;
then
e < |.(In ((i !),F_Complex)).|
by A10, A9, XXREAL_0:2;
then
|.(eval (g1,(In ((i !),F_Complex)))).| > 1
by A6;
hence
|.(eval (f1,(In ((i !),INT.Ring)))).| > 1
by ALGNUM_1:4, Th40, A11, SUBSET_1:def 8;
verum
end; then consider m being
Element of
NAT such that A12:
for
n being
Nat st
n >= m holds
|.(eval (f1,(In ((n !),INT.Ring)))).| > 1
;
defpred S1[
Nat]
means ex
x being
Element of
INT.Ring st
eval (
f,
x),
0 are_congruent_mod $1;
set X =
{ p where p is Prime : ( S1[p] & p >= m ) } ;
A13:
for
n being
Nat st
n >= m holds
ex
p being
Prime st
(
p > n &
S1[
p] )
proof
let n be
Nat;
( n >= m implies ex p being Prime st
( p > n & S1[p] ) )
assume A14:
n >= m
;
ex p being Prime st
( p > n & S1[p] )
set N =
In (
(n !),
INT.Ring);
consider k being
Element of
INT.Ring such that A15:
eval (
f1,
(In ((n !),INT.Ring)))
= (k * (In ((n !),INT.Ring))) + (f1 . 0)
by Th70;
|.((k * (In ((n !),INT.Ring))) + 1).| > 1
by A4, A15, A14, A12;
then consider p being
Prime such that A16:
p divides |.((k * (In ((n !),INT.Ring))) + 1).|
by MOEBIUS1:5;
A17:
p divides (k * (In ((n !),INT.Ring))) + 1
by A16, NUMBER14:4;
A18:
p > n
eval (
f,
((f . 0) * (In ((n !),INT.Ring)))) =
(f . 0) * (eval (f1,(In ((n !),INT.Ring))))
by A5
.=
(f . 0) * ((k * (In ((n !),INT.Ring))) + 1)
by A4, A15
;
then
eval (
f,
((f . 0) * (In ((n !),INT.Ring)))),
0 are_congruent_mod p
by A17, INT_2:2;
hence
ex
p being
Prime st
(
p > n &
S1[
p] )
by A18;
verum
end;
for
y being
object st
y in { p where p is Prime : ( S1[p] & p >= m ) } holds
y is
natural
then reconsider X =
{ p where p is Prime : ( S1[p] & p >= m ) } as
natural-membered set by MEMBERED:def 6;
A19:
not
X is
empty
A21:
for
a being
Nat st
a in X holds
ex
b being
Nat st
(
b > a &
b in X )
X c= { p where p is Prime : S1[p] }
hence
{ p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is
infinite
by A21, A19, NUMBER04:1;
verum end;