let n be Nat; :: thesis: not 65 divides (2 |^ n) - 3
assume 65 divides (2 |^ n) - 3 ; :: thesis: contradiction
then A1: 2 |^ n,3 are_congruent_mod 65 ;
A2: 2 |^ 7,63 are_congruent_mod 65 by Lm7;
65 * 3 = ((2 |^ 8) - 3) - 58 by Lm8;
then A3: 2 |^ 8,61 are_congruent_mod 65 ;
65 * 7 = ((2 |^ 9) - 3) - 54 by Lm9;
then A4: 2 |^ 9,57 are_congruent_mod 65 ;
65 * 15 = ((2 |^ 10) - 3) - 46 by Lm10;
then A5: 2 |^ 10,49 are_congruent_mod 65 ;
65 * 31 = ((2 |^ 11) - 3) - 30 by Lm11;
then A6: 2 |^ 11,33 are_congruent_mod 65 ;
A7: 2 |^ n,2 |^ (n mod 12) are_congruent_mod 65 by Th30;
not not n mod (11 + 1) = 0 & ... & not n mod (11 + 1) = 11 by NUMBER03:11;

per cases then ( n mod 12 = 0 or n mod 12 = 1 or n mod 12 = 2 or n mod 12 = 3 or n mod 12 = 4 or n mod 12 = 5 or n mod 12 = 6 or n mod 12 = 7 or n mod 12 = 8 or n mod 12 = 9 or n mod 12 = 10 or n mod 12 = 11 ) ;

suppose n mod 12 = 0 ; :: thesis: contradiction

then 2 |^ n,1 are_congruent_mod 65 by A7, NEWTON:4;
hence contradiction by A1, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 1 ; :: thesis: contradiction

hence contradiction by A1, A7, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 2 ; :: thesis: contradiction

hence contradiction by A1, A7, Lm2, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 3 ; :: thesis: contradiction

hence contradiction by A1, A7, Lm3, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 4 ; :: thesis: contradiction

hence contradiction by A1, A7, Lm4, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 5 ; :: thesis: contradiction

hence contradiction by A1, A7, Lm5, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 6 ; :: thesis: contradiction

hence contradiction by A1, A7, Lm6, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 7 ; :: thesis: contradiction

then 2 |^ n,63 are_congruent_mod 65 by A2, A7, INT_1:15;
hence contradiction by A1, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 8 ; :: thesis: contradiction

then 2 |^ n,61 are_congruent_mod 65 by A3, A7, INT_1:15;
hence contradiction by A1, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 9 ; :: thesis: contradiction

then 2 |^ n,57 are_congruent_mod 65 by A4, A7, INT_1:15;
hence contradiction by A1, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 10 ; :: thesis: contradiction

then 2 |^ n,49 are_congruent_mod 65 by A5, A7, INT_1:15;
hence contradiction by A1, NAT_6:14; :: thesis: verum

end;

suppose n mod 12 = 11 ; :: thesis: contradiction

then 2 |^ n,33 are_congruent_mod 65 by A6, A7, INT_1:15;
hence contradiction by A1, NAT_6:14; :: thesis: verum

end;

end;