let k be positive Nat; :: thesis: ( ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) iff k in {2,5,8} )
thus ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) implies k in {2,5,8} ) :: thesis: ( k in {2,5,8} implies ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) )

proof

assume that
A1: k <= 10 and
A2: for n being positive Nat holds H₁(k,n) is composite ; :: thesis: k in {2,5,8}
not not k = 0 & ... & not k = 10 by A1;

per cases then ( k = 0 or k = 1 or k = 2 or k = 5 or k = 8 or k = 3 or k = 4 or k = 6 or k = 7 or k = 9 or k = 10 ) ;

suppose k = 0 ; :: thesis: k in {2,5,8}

hence k in {2,5,8} ; :: thesis: verum

end;

suppose A3: k = 1 ; :: thesis: k in {2,5,8}

H₁(1,1) = (2 |^ (2 |^ 1)) + 1 ;
hence k in {2,5,8} by A2, A3, Th24; :: thesis: verum

end;

suppose ( k = 2 or k = 5 or k = 8 ) ; :: thesis: k in {2,5,8}

hence k in {2,5,8} by ENUMSET1:def 1; :: thesis: verum

end;

suppose A4: k = 3 ; :: thesis: k in {2,5,8}

H₁(3,1) = (3 * (2 |^ (2 |^ 1))) + 1 ;
hence k in {2,5,8} by A2, A4, Th26; :: thesis: verum

end;

suppose A5: k = 4 ; :: thesis: k in {2,5,8}

H₁(4,1) = (4 * (2 |^ (2 |^ 1))) + 1 ;
hence k in {2,5,8} by A2, A5, Th27; :: thesis: verum

end;

suppose A6: k = 6 ; :: thesis: k in {2,5,8}

H₁(6,2) = 97 by Lm2, Lm4;
hence k in {2,5,8} by A2, A6, XPRIMES1:97; :: thesis: verum

end;

suppose A7: k = 7 ; :: thesis: k in {2,5,8}

H₁(7,1) = (7 * (2 |^ (2 |^ 1))) + 1 ;
hence k in {2,5,8} by A2, A7, Th30; :: thesis: verum

end;

suppose A8: k = 9 ; :: thesis: k in {2,5,8}

H₁(9,1) = (9 * (2 |^ (2 |^ 1))) + 1 ;
hence k in {2,5,8} by A2, A8, Th32; :: thesis: verum

end;

suppose A9: k = 10 ; :: thesis: k in {2,5,8}

H₁(10,1) = (10 * (2 |^ (2 |^ 1))) + 1 ;
hence k in {2,5,8} by A2, A9, Th33; :: thesis: verum

end;

end;

end;

assume k in {2,5,8} ; :: thesis: ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) )

per cases then ( k = 2 or k = 5 or k = 8 ) by ENUMSET1:def 1;

suppose k = 2 ; :: thesis: ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) )

hence ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) by Th35; :: thesis: verum

end;

suppose k = 5 ; :: thesis: ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) )

hence ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) by Th36; :: thesis: verum

end;

suppose k = 8 ; :: thesis: ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) )

hence ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) by Th37; :: thesis: verum

end;

end;