let t be Integer; :: thesis: ( not t divides 24 or t = - 1 or t = 1 or t = - 2 or t = 2 or t = - 3 or t = 3 or t = - 4 or t = 4 or t = - 6 or t = 6 or t = - 8 or t = 8 or t = - 12 or t = 12 or t = - 24 or t = 24 )
reconsider n = |.t.| as Nat ;
assume t divides 24 ; :: thesis: ( t = - 1 or t = 1 or t = - 2 or t = 2 or t = - 3 or t = 3 or t = - 4 or t = 4 or t = - 6 or t = 6 or t = - 8 or t = 8 or t = - 12 or t = 12 or t = - 24 or t = 24 )
then n divides |.24.| by INT_2:16;
then n divides 24 ;
then ( n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 ) by lem24nat;
hence ( t = - 1 or t = 1 or t = - 2 or t = 2 or t = - 3 or t = 3 or t = - 4 or t = 4 or t = - 6 or t = 6 or t = - 8 or t = 8 or t = - 12 or t = 12 or t = - 24 or t = 24 ) by lemmod; :: thesis: verum