let a be Nat; :: thesis: ( ( for i being Nat holds not a + 1 = 2 |^ i ) implies { n where n is Nat : n divides (a |^ n) + 1 } is infinite )
assume A1: for i being Nat holds not a + 1 = 2 |^ i ; :: thesis: { n where n is Nat : n divides (a |^ n) + 1 } is infinite
set A = { n where n is Nat : n divides (a |^ n) + 1 } ;
consider p being Element of NAT such that
A2: p is prime and
A3: p divides a + 1 and
A4: p <> 2 by A1, GROUPP_1:1, INT_2:28;
p is odd by A2, A4;
then reconsider p = p as odd Prime by A2;
deffunc H₁( Nat) -> set = p |^ $1;
consider f being ManySortedSet of NAT such that
A5: for d being Element of NAT holds f . d = H₁(d) from PBOOLE:sch 5();
A6: dom f = NAT by PARTFUN1:def 2;
A7: rng f c= { n where n is Nat : n divides (a |^ n) + 1 }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { n where n is Nat : n divides (a |^ n) + 1 } )
assume y in rng f ; :: thesis: y in { n where n is Nat : n divides (a |^ n) + 1 }
then consider k being object such that
A8: k in dom f and
A9: f . k = y by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A8, PARTFUN1:def 2;
H₁(k) divides (a |^ H₁(k)) + 1 by A3, Th23;
then H₁(k) in { n where n is Nat : n divides (a |^ n) + 1 } ;
hence y in { n where n is Nat : n divides (a |^ n) + 1 } by A5, A9; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A10: ( x1 in dom f & x2 in dom f ) and
A11: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A10, PARTFUN1:def 2;
A12: p > 1 by INT_2:def 4;
( f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A5;
hence x1 = x2 by A11, A12, PEPIN:30; :: thesis: verum

end;

hence { n where n is Nat : n divides (a |^ n) + 1 } is infinite by A6, A7, CARD_1:59; :: thesis: verum