let a be Nat; :: thesis: ( a > 1 implies { n where n is Nat : n divides (a |^ n) + 1 } is infinite )
assume A1: a > 1 ; :: thesis: { n where n is Nat : n divides (a |^ n) + 1 } is infinite
set A = { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } ;
set X = { n where n is Nat : n divides (a |^ n) + 1 } ;
A2: { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } is natural-membered

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis: ( not x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } or not x is natural )
assume x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } ; :: thesis: x is natural
then ex s being Nat st
( x = s & s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) ;
hence x is natural ; :: thesis: verum

end;

A3: { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } c= { n where n is Nat : n divides (a |^ n) + 1 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } or x in { n where n is Nat : n divides (a |^ n) + 1 } )
assume x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } ; :: thesis: x in { n where n is Nat : n divides (a |^ n) + 1 }
then ex s being Nat st
( x = s & s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) ;
hence x in { n where n is Nat : n divides (a |^ n) + 1 } ; :: thesis: verum

end;

per cases ( a is odd or a is even ) ;

suppose A4: a is odd ; :: thesis: { n where n is Nat : n divides (a |^ n) + 1 } is infinite

2 = 2 * ((2 * 0) + 1) ;
then A5: 2 is double_odd ;
(a |^ 2) + 1 is double_odd by A4;
then 2 divides (a |^ 2) + 1 ;
then A6: 2 in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } by A4, A5;
for x being Nat st x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } holds
ex b being Nat st
( b > x & b in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } )

proof

let x be Nat; :: thesis: ( x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } implies ex b being Nat st
( b > x & b in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } ) )
assume x in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } ; :: thesis: ex b being Nat st
( b > x & b in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } )
then consider s being Nat such that
A7: x = s and
A8: ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) ;
take s1 = (a |^ s) + 1; :: thesis: ( s1 > x & s1 in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } )
( s1 > s & s1 is double_odd & (a |^ s1) + 1 is double_odd & s1 divides (a |^ s1) + 1 ) by A1, A4, A8, Th24;
hence ( s1 > x & s1 in { s where s is Nat : ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 ) } ) by A7; :: thesis: verum

end;

hence { n where n is Nat : n divides (a |^ n) + 1 } is infinite by A2, A3, A6, Th1; :: thesis: verum

end;

suppose A9: a is even ; :: thesis: { n where n is Nat : n divides (a |^ n) + 1 } is infinite

now :: thesis: for i being Nat holds not a + 1 = 2 |^ i

given i being Nat such that A10: a + 1 = 2 |^ i ; :: thesis: contradiction

now :: thesis: not i < 1

assume i < 1 ; :: thesis: contradiction
then a + 1 = 1 by A10, Lm1, NAT_1:14;
hence contradiction by A1, NAT_1:14; :: thesis: verum

end;

hence contradiction by A9, A10; :: thesis: verum

end;

hence { n where n is Nat : n divides (a |^ n) + 1 } is infinite by Lm1117; :: thesis: verum

end;

end;