let a, b be Nat; :: thesis: ( a > 0 & b > 0 implies ex N being infinite Subset of NAT st
for n, m being Nat
for p being Prime st n in N & m in N holds
( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m ) )
assume A1: ( a > 0 & b > 0 ) ; :: thesis: ex N being infinite Subset of NAT st
for n, m being Nat
for p being Prime st n in N & m in N holds
( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m )
set d = a gcd (a + b);
consider a1, c being Nat such that
A2: ( a = (a gcd (a + b)) * a1 & a + b = (a gcd (a + b)) * c & a1,c are_coprime ) by A1, NUMBER03:18;
reconsider a1 = a1 as non zero Nat by A1, A2;
A3: a1 >= 1 by NAT_1:14;
A4: c > 1

proof

c <> 0 by A1, A2;
then A5: c >= 1 by NAT_1:14;
assume c <= 1 ; :: thesis: contradiction
then A6: c = 1 by A5, XXREAL_0:1;
a + 0 < a + b by A1, XREAL_1:8;
hence contradiction by A6, A2, A3, XREAL_1:66; :: thesis: verum

end;

then c >= 1 + 1 by NAT_1:13;
then ( c |^ (Euler a1) > Euler a1 & Euler a1 >= 1 ) by NAT_1:14, NEWTON:86;
then A7: c |^ (Euler a1) > 1 by XXREAL_0:2;
A8: for n being Nat holds a1 divides ((c |^ (Euler a1)) |^ (n + 1)) - 1

proof

let n be Nat; :: thesis: a1 divides ((c |^ (Euler a1)) |^ (n + 1)) - 1
a1 >= 1 by NAT_1:14;

per cases then ( a1 = 1 or a1 > 1 ) by XXREAL_0:1;

suppose a1 = 1 ; :: thesis: a1 divides ((c |^ (Euler a1)) |^ (n + 1)) - 1

hence a1 divides ((c |^ (Euler a1)) |^ (n + 1)) - 1 by INT_2:12; :: thesis: verum

end;

suppose A9: a1 > 1 ; :: thesis: a1 divides ((c |^ (Euler a1)) |^ (n + 1)) - 1

c <> 0 by A2, A1;
then (c |^ (Euler a1)) mod a1 = 1 by A2, A9, EULER_2:18;
then ( ((c |^ (Euler a1)) |^ (n + 1)) mod a1 = 1 & 1 = 1 mod a1 ) by NEWTON05:15;
hence a1 divides ((c |^ (Euler a1)) |^ (n + 1)) - 1 by INT_4:23; :: thesis: verum

end;

end;

end;

deffunc H₁( Nat) -> set = (c * ((((c |^ (Euler a1)) |^ ($1 + 1)) - 1) / a1)) + 1;
consider f being Function such that
A10: ( dom f = NAT & ( for x being Element of NAT holds f . x = H₁(x) ) ) from FUNCT_1:sch 4();
A11: rng f c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being object such that
A12: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A12, A10;
c <> 0 by A1, A2;
then consider tn being Nat such that
A13: a1 * tn = ((c |^ (Euler a1)) |^ (x + 1)) - 1 by A8, NAT_D:def 3;
(((c |^ (Euler a1)) |^ (x + 1)) - 1) / a1 = tn * (a1 / a1) by A13, XCMPLX_1:74
.= tn * 1 by XCMPLX_1:60 ;
then y = (c * tn) + 1 by A10, A12;
hence y in NAT ; :: thesis: verum

end;

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A14: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A14, A10;
( H₁(x1) = f . x1 & H₁(x2) = f . x2 ) by A10;
then (c * ((((c |^ (Euler a1)) |^ (x1 + 1)) - 1) / a1)) + 1 = (c * ((((c |^ (Euler a1)) |^ (x2 + 1)) - 1) / a1)) + 1 by A14;
then (((c |^ (Euler a1)) |^ (x1 + 1)) - 1) / a1 = (((c |^ (Euler a1)) |^ (x2 + 1)) - 1) / a1 by A4, XCMPLX_1:5;
then a1 * (((c |^ (Euler a1)) |^ (x1 + 1)) - 1) = a1 * (((c |^ (Euler a1)) |^ (x2 + 1)) - 1) by XCMPLX_1:95;
then ((c |^ (Euler a1)) |^ (x1 + 1)) - 1 = ((c |^ (Euler a1)) |^ (x2 + 1)) - 1 by XCMPLX_1:5;
then x1 + 1 = x2 + 1 by A7, PEPIN:30;
hence x1 = x2 ; :: thesis: verum

end;

then reconsider N = rng f as infinite Subset of NAT by FUNCT_1:def 4, A11, A10, CARD_1:59;
take N ; :: thesis: for n, m being Nat
for p being Prime st n in N & m in N holds
( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m )
A15: for n being Nat
for p being Prime st n in N holds
( p divides (ArProg (b,a)) . n iff ( p divides a gcd (a + b) or p divides c ) )

proof

let n be Nat; :: thesis: for p being Prime st n in N holds
( p divides (ArProg (b,a)) . n iff ( p divides a gcd (a + b) or p divides c ) )
let p be Prime; :: thesis: ( n in N implies ( p divides (ArProg (b,a)) . n iff ( p divides a gcd (a + b) or p divides c ) ) )
assume A16: n in N ; :: thesis: ( p divides (ArProg (b,a)) . n iff ( p divides a gcd (a + b) or p divides c ) )
consider x being object such that
A17: ( x in dom f & f . x = n ) by A16, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A17, A10;
c <> 0 by A1, A2;
then consider tn being Nat such that
A18: a1 * tn = ((c |^ (Euler a1)) |^ (x + 1)) - 1 by A8, NAT_D:def 3;
(((c |^ (Euler a1)) |^ (x + 1)) - 1) / a1 = tn * (a1 / a1) by A18, XCMPLX_1:74
.= tn * 1 by XCMPLX_1:60 ;
then n = (c * tn) + 1 by A10, A17;
then A19: (ArProg (b,a)) . n = b + (a * ((c * tn) + 1)) by NUMBER06:7
.= ((a * c) * tn) + (c * (a gcd (a + b))) by A2
.= (((a gcd (a + b)) * c) * (a1 * tn)) + (c * (a gcd (a + b))) by A2
.= (((a gcd (a + b)) * c) * (((c |^ (Euler a1)) |^ (x + 1)) - 1)) + (c * (a gcd (a + b))) by A18
.= ((a gcd (a + b)) * c) * ((c |^ (Euler a1)) |^ (x + 1))
.= ((a gcd (a + b)) * c) * (c |^ ((x + 1) * (Euler a1))) by NEWTON:9
.= (a gcd (a + b)) * (c * (c |^ ((x + 1) * (Euler a1))))
.= (a gcd (a + b)) * (c |^ (1 + ((x + 1) * (Euler a1)))) by NEWTON:6 ;

hereby :: thesis: ( ( p divides a gcd (a + b) or p divides c ) implies p divides (ArProg (b,a)) . n )

assume p divides (ArProg (b,a)) . n ; :: thesis: ( p divides a gcd (a + b) or p divides c )
then ( p divides a gcd (a + b) or p divides c |^ (1 + ((x + 1) * (Euler a1))) ) by A19, INT_5:7;
hence ( p divides a gcd (a + b) or p divides c ) by NAT_3:5; :: thesis: verum

end;

assume ( p divides a gcd (a + b) or p divides c ) ; :: thesis: p divides (ArProg (b,a)) . n
then ( p divides a gcd (a + b) or p divides c |^ (1 + ((x + 1) * (Euler a1))) ) by NEWTON02:14;
hence p divides (ArProg (b,a)) . n by A19, NAT_D:9; :: thesis: verum

end;

let n, m be Nat; :: thesis: for p being Prime st n in N & m in N holds
( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m )
let p be Prime; :: thesis: ( n in N & m in N implies ( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m ) )
assume A20: ( n in N & m in N ) ; :: thesis: ( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m )
( p divides (ArProg (b,a)) . n iff ( p divides a gcd (a + b) or p divides c ) ) by A20, A15;
hence ( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m ) by A20, A15; :: thesis: verum