let n be natural number ; ( not n divides 24 or n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 )
assume n:
n divides 24
; ( n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 )
then
n <= 24
by INT_2:27;
then el:
not not n = 0 & ... & not n = 24
;
n0:
not 0 divides 24
by INT_2:3;
( 5 * 4 < 24 & 24 < 5 * (4 + 1) )
;
then n5:
not 5 divides 24
by NEWTON03:40;
( 7 * 3 < 24 & 24 < 7 * (3 + 1) )
;
then n7:
not 7 divides 24
by NEWTON03:40;
( 9 * 2 < 24 & 24 < 9 * (2 + 1) )
;
then n9:
not 9 divides 24
by NEWTON03:40;
( 10 * 2 < 24 & 24 < 10 * (2 + 1) )
;
then n10:
not 10 divides 24
by NEWTON03:40;
( 11 * 2 < 24 & 24 < 11 * (2 + 1) )
;
then n11:
not 11 divides 24
by NEWTON03:40;
( 13 * 1 < 24 & 24 < 13 * (1 + 1) )
;
then n13:
not 13 divides 24
by NEWTON03:40;
( 14 * 1 < 24 & 24 < 14 * (1 + 1) )
;
then n14:
not 14 divides 24
by NEWTON03:40;
( 15 * 1 < 24 & 24 < 15 * (1 + 1) )
;
then n15:
not 15 divides 24
by NEWTON03:40;
( 16 * 1 < 24 & 24 < 16 * (1 + 1) )
;
then n16:
not 16 divides 24
by NEWTON03:40;
( 17 * 1 < 24 & 24 < 17 * (1 + 1) )
;
then n17:
not 17 divides 24
by NEWTON03:40;
( 18 * 1 < 24 & 24 < 18 * (1 + 1) )
;
then n18:
not 18 divides 24
by NEWTON03:40;
( 19 * 1 < 24 & 24 < 19 * (1 + 1) )
;
then n19:
not 19 divides 24
by NEWTON03:40;
( 20 * 1 < 24 & 24 < 20 * (1 + 1) )
;
then n20:
not 20 divides 24
by NEWTON03:40;
( 21 * 1 < 24 & 24 < 21 * (1 + 1) )
;
then n21:
not 21 divides 24
by NEWTON03:40;
( 22 * 1 < 24 & 24 < 22 * (1 + 1) )
;
then n22:
not 22 divides 24
by NEWTON03:40;
( 23 * 1 < 24 & 24 < 23 * (1 + 1) )
;
then
not 23 divides 24
by NEWTON03:40;
hence
( n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 )
by n, el, n0, n5, n7, n9, n10, n11, n13, n14, n15, n16, n17, n18, n19, n20, n21, n22; verum