let n be Nat; :: thesis:
assume A1: n divides 27 ; :: thesis:
then n <= 27 by INT_2:27;
then A2: not not n = 0 & ... & not n = 27 ;

now :: thesis:

((2 * 13) + 1) mod 2 = 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 2 divides 27 ; :: thesis:
((4 * 6) + 3) mod 4 = 3 mod 4 by NAT_D:21
.= 3 by NAT_D:24 ;
hence not 4 divides 27 by INT_1:62; :: thesis:
((5 * 5) + 2) mod 5 = 2 mod 5 by NAT_D:21
.= 2 by NAT_D:24 ;
hence not 5 divides 27 by INT_1:62; :: thesis:
((6 * 4) + 3) mod 6 = 3 mod 6 by NAT_D:21
.= 3 by NAT_D:24 ;
hence not 6 divides 27 by INT_1:62; :: thesis:
((7 * 3) + 6) mod 7 = 6 mod 7 by NAT_D:21
.= 6 by NAT_D:24 ;
hence not 7 divides 27 by INT_1:62; :: thesis:
((8 * 3) + 3) mod 8 = 3 mod 8 by NAT_D:21
.= 3 by NAT_D:24 ;
hence not 8 divides 27 by INT_1:62; :: thesis:
((10 * 2) + 7) mod 10 = 7 mod 10 by NAT_D:21
.= 7 by NAT_D:24 ;
hence not 10 divides 27 by INT_1:62; :: thesis:
((11 * 2) + 5) mod 11 = 5 mod 11 by NAT_D:21
.= 5 by NAT_D:24 ;
hence not 11 divides 27 by INT_1:62; :: thesis:
((12 * 2) + 3) mod 12 = 3 mod 12 by NAT_D:21
.= 3 by NAT_D:24 ;
hence not 12 divides 27 by INT_1:62; :: thesis:
((13 * 2) + 1) mod 13 = 1 mod 13 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 13 divides 27 by INT_1:62; :: thesis:
((14 * 1) + 13) mod 14 = 13 mod 14 by NAT_D:21
.= 13 by NAT_D:24 ;
hence not 14 divides 27 by INT_1:62; :: thesis:
((15 * 1) + 12) mod 15 = 12 mod 15 by NAT_D:21
.= 12 by NAT_D:24 ;
hence not 15 divides 27 by INT_1:62; :: thesis:
((16 * 1) + 11) mod 16 = 11 mod 16 by NAT_D:21
.= 11 by NAT_D:24 ;
hence not 16 divides 27 by INT_1:62; :: thesis:
((17 * 1) + 10) mod 17 = 10 mod 17 by NAT_D:21
.= 10 by NAT_D:24 ;
hence not 17 divides 27 by INT_1:62; :: thesis:
((18 * 1) + 9) mod 18 = 9 mod 18 by NAT_D:21
.= 9 by NAT_D:24 ;
hence not 18 divides 27 by INT_1:62; :: thesis:
((19 * 1) + 8) mod 19 = 8 mod 19 by NAT_D:21
.= 8 by NAT_D:24 ;
hence not 19 divides 27 by INT_1:62; :: thesis:
((20 * 1) + 7) mod 20 = 7 mod 20 by NAT_D:21
.= 7 by NAT_D:24 ;
hence not 20 divides 27 by INT_1:62; :: thesis:
((21 * 1) + 6) mod 21 = 6 mod 21 by NAT_D:21
.= 6 by NAT_D:24 ;
hence not 21 divides 27 by INT_1:62; :: thesis:
((22 * 1) + 5) mod 22 = 5 mod 22 by NAT_D:21
.= 5 by NAT_D:24 ;
hence not 22 divides 27 by INT_1:62; :: thesis:
((23 * 1) + 4) mod 23 = 4 mod 23 by NAT_D:21
.= 4 by NAT_D:24 ;
hence not 23 divides 27 by INT_1:62; :: thesis:
((24 * 1) + 3) mod 24 = 3 mod 24 by NAT_D:21
.= 3 by NAT_D:24 ;
hence not 24 divides 27 by INT_1:62; :: thesis:
((25 * 1) + 2) mod 25 = 2 mod 25 by NAT_D:21
.= 2 by NAT_D:24 ;
hence not 25 divides 27 by INT_1:62; :: thesis:
((26 * 1) + 1) mod 26 = 1 mod 26 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 26 divides 27 by INT_1:62; :: thesis:

end;

hence ( n = 1 or n = 3 or n = 9 or n = 27 ) by A1, A2; :: thesis: