let m, n, r be Nat; :: thesis: ( n > 1 & ( for i being Nat st i < n holds
( (ArProg (m,r)) . i is odd & (ArProg (m,r)) . i is prime ) ) implies for p being Prime st p < n holds
p divides r )
assume A0: n > 1 ; :: thesis: ( ex i being Nat st
( i < n & not ( (ArProg (m,r)) . i is odd & (ArProg (m,r)) . i is prime ) ) or for p being Prime st p < n holds
p divides r )
assume A1: for i being Nat st i < n holds
( (ArProg (m,r)) . i is odd & (ArProg (m,r)) . i is prime ) ; :: thesis: for p being Prime st p < n holds
p divides r
let p be Prime; :: thesis: ( p < n implies p divides r )
assume ZZ: p < n ; :: thesis: p divides r
per cases ( r = 0 or r <> 0 ) ;
suppose r = 0 ; :: thesis: p divides r
hence p divides r by NAT_D:6; :: thesis: verum
end;
suppose Z2: r <> 0 ; :: thesis: p divides r
Zz: n <= m
proof
assume F1: n > m ; :: thesis: contradiction
S1: 1 + r <> 1 by Z2;
(ArProg (m,r)) . 0 = m + (0 * r) by NUMBER06:7;
then ( m is odd & m is prime ) by A1, A0;
then S2: 1 * (1 + r) < m * (1 + r) by XREAL_1:68;
1 + r divides m * (1 + r) ;
then WZ: not m + (m * r) is prime by S2, S1;
(ArProg (m,r)) . m = m + (m * r) by NUMBER06:7;
hence contradiction by WZ, A1, F1; :: thesis: verum
end;
deffunc H1( Nat) -> Element of NAT = ((ArProg (m,r)) . $1) mod p;
BD: p < m by ZZ, Zz, XXREAL_0:2;
JJ: for i being Nat st 0 <= i & i < n holds
H1(i) <> 0
proof
let i be Nat; :: thesis: ( 0 <= i & i < n implies H1(i) <> 0 )
assume WW: ( 0 <= i & i < n ) ; :: thesis: H1(i) <> 0
reconsider aa = (ArProg (m,r)) . i as Nat ;
XY: (ArProg (m,r)) . i = m + (i * r) by NUMBER06:7;
assume H1(i) = 0 ; :: thesis: contradiction
then p divides aa by PEPIN:6;
then W1: p divides m + (r * i) by NUMBER06:7;
m + (r * i) is Prime by A1, WW, XY;
then Ox: ( p = m + (r * i) or p = 1 ) by INT_2:def 4, W1;
p + 0 < m + (r * i) by BD, XREAL_1:8;
hence contradiction by Ox, INT_2:def 4; :: thesis: verum
end;
reconsider w = p - 1 as Nat ;
reconsider Sw = Seg w as non empty finite set ;
deffunc H2( Nat) -> Element of Sw = In ((((ArProg (m,r)) . $1) mod p),Sw);
ex f being Function of ({0} \/ (Seg w)),Sw st
for x being Element of {0} \/ (Seg w) holds f . x = H2(x) from FUNCT_2:sch 4();
then consider f being Function of ({0} \/ (Seg w)),Sw such that
CC: for x being Element of {0} \/ (Seg w) holds f . x = H2(x) ;
set B = Seg w;
set A = {0} \/ (Seg w);
not 0 in Seg w by FINSEQ_1:1;
then P2: card ({0} \/ (Seg w)) = (card (Seg w)) + 1 by CARD_2:41
.= w + 1 ;
reconsider cB = card (Seg w), cA = card ({0} \/ (Seg w)) as Nat ;
cB < cA by P2, NAT_1:13;
then card (Segm cB) in card (Segm cA) by NAT_1:41;
then consider xx1, xx2 being object such that
C3: ( xx1 in {0} \/ (Seg w) & xx2 in {0} \/ (Seg w) & xx1 <> xx2 & f . xx1 = f . xx2 ) by FINSEQ_4:65;
reconsider xx1 = xx1, xx2 = xx2 as Nat by C3;
ex n1, n2 being Nat st
( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
proof
per cases ( xx1 > xx2 or xx1 < xx2 ) by XXREAL_0:1, C3;
suppose W1: xx1 > xx2 ; :: thesis: ex n1, n2 being Nat st
( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
take n1 = xx2; :: thesis: ex n2 being Nat st
( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
take n2 = xx1; :: thesis: ( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
thus ( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 ) by C3, W1; :: thesis: verum
end;
suppose W1: xx1 < xx2 ; :: thesis: ex n1, n2 being Nat st
( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
take n1 = xx1; :: thesis: ex n2 being Nat st
( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
take n2 = xx2; :: thesis: ( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 )
thus ( n1 in {0} \/ (Seg w) & n2 in {0} \/ (Seg w) & n1 < n2 & f . n1 = f . n2 ) by C3, W1; :: thesis: verum
end;
end;
end;
then consider x2, x1 being Nat such that
C3: ( x2 in {0} \/ (Seg w) & x1 in {0} \/ (Seg w) & x2 < x1 & f . x2 = f . x1 ) ;
(ArProg (m,r)) . x1 = m + (x1 * r) by NUMBER06:7;
then H2: ((ArProg (m,r)) . x1) - ((ArProg (m,r)) . x2) = (m + (x1 * r)) - (m + (x2 * r)) by NUMBER06:7;
k1: ( x1 in {0} or x1 in Seg w ) by C3, XBOOLE_0:def 3;
then K1: ( x1 = 0 or ( 1 <= x1 & x1 <= p - 1 ) ) by FINSEQ_1:1;
K2: x1 <= p - 1 by k1, FINSEQ_1:1;
( x2 in {0} or x2 in Seg w ) by C3, XBOOLE_0:def 3;
then WW: x2 <= p - 1 by FINSEQ_1:1;
J3: p - 1 < (p - 1) + 1 by NAT_1:13;
x1 - x2 <= x1 - 0 by XREAL_1:13;
then x1 - x2 <= w by K2, XXREAL_0:2;
then T1: x1 - x2 < p by J3, XXREAL_0:2;
x1 < p by K1, J3, XXREAL_0:2;
then x1 < n by ZZ, XXREAL_0:2;
then O1: ((ArProg (m,r)) . x1) mod p <> 0 by JJ;
((ArProg (m,r)) . x1) mod p < w + 1 by NAT_D:1;
then O2: ((ArProg (m,r)) . x1) mod p <= w by NAT_1:13;
Ja: 0 + 1 <= ((ArProg (m,r)) . x1) mod p by O1, NAT_1:13;
x2 < p by WW, J3, XXREAL_0:2;
then ( 0 <= x2 & x2 < n ) by ZZ, XXREAL_0:2;
then O1: ((ArProg (m,r)) . x2) mod p <> 0 by JJ;
((ArProg (m,r)) . x2) mod p < w + 1 by NAT_D:1;
then O3: ((ArProg (m,r)) . x2) mod p <= w by NAT_1:13;
Jb: 0 + 1 <= ((ArProg (m,r)) . x2) mod p by O1, NAT_1:13;
f . x1 = In ((((ArProg (m,r)) . x1) mod p),Sw) by C3, CC;
then C4: f . x1 = ((ArProg (m,r)) . x1) mod p by Ja, SUBSET_1:def 8, O2, FINSEQ_1:1;
f . x2 = In ((((ArProg (m,r)) . x2) mod p),Sw) by C3, CC;
then f . x2 = ((ArProg (m,r)) . x2) mod p by Jb, SUBSET_1:def 8, O3, FINSEQ_1:1;
then SS: p divides (x1 - x2) * r by H2, C3, C4, INT_4:23;
x1 - x2 > x2 - x2 by C3, XREAL_1:9;
then not p divides x1 - x2 by T1, NAT_D:7;
hence p divides r by SS, NAT_6:7; :: thesis: verum
end;
end;