6 = 2 * 3 ;
then 2 divides 6 by NAT_D:def 3;
hence not 6 is prime by INT_2:def 4; :: thesis:
8 = 2 * 4 ;
then 2 divides 8 by NAT_D:def 3;
hence not 8 is prime by INT_2:def 4; :: thesis:
9 = 3 * 3 ;
then 3 divides 9 by NAT_D:def 3;
hence not 9 is prime by INT_2:def 4; :: thesis:
10 = 2 * 5 ;
then 2 divides 10 by NAT_D:def 3;
hence not 10 is prime by INT_2:def 4; :: thesis:
12 = 2 * 6 ;
then 2 divides 12 by NAT_D:def 3;
hence not 12 is prime by INT_2:def 4; :: thesis:
14 = 2 * 7 ;
then 2 divides 14 by NAT_D:def 3;
hence not 14 is prime by INT_2:def 4; :: thesis:
15 = 3 * 5 ;
then 3 divides 15 by NAT_D:def 3;
hence not 15 is prime by INT_2:def 4; :: thesis:
16 = 4 * 4 ;
then 4 divides 16 by NAT_D:def 3;
hence not 16 is prime by INT_2:def 4; :: thesis:
18 = 2 * 9 ;
then 2 divides 18 by NAT_D:def 3;
hence not 18 is prime by INT_2:def 4; :: thesis:
20 = 4 * 5 ;
then 4 divides 20 by NAT_D:def 3;
hence not 20 is prime by INT_2:def 4; :: thesis:
21 = 3 * 7 ;
then 3 divides 21 by NAT_D:def 3;
hence not 21 is prime by INT_2:def 4; :: thesis:
22 = 2 * 11 ;
then 2 divides 22 by NAT_D:def 3;
hence not 22 is prime by INT_2:def 4; :: thesis:
24 = 4 * 6 ;
then 4 divides 24 by NAT_D:def 3;
hence not 24 is prime by INT_2:def 4; :: thesis:
25 = 5 * 5 ;
then 5 divides 25 by NAT_D:def 3;
hence not 25 is prime by INT_2:def 4; :: thesis:
26 = 2 * 13 ;
then 2 divides 26 by NAT_D:def 3;
hence not 26 is prime by INT_2:def 4; :: thesis:
27 = 3 * 9 ;
then 3 divides 27 by NAT_D:def 3;
hence not 27 is prime by INT_2:def 4; :: thesis:
28 = 4 * 7 ;
then 4 divides 28 by NAT_D:def 3;
hence not 28 is prime by INT_2:def 4; :: thesis: