let n be Element of NAT ; ( n > 1 & n <> 4 & not n is prime implies ex k being non zero Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) )
assume that
A1:
n > 1
and
A2:
n <> 4
; ( n is prime or ex k being non zero Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) )
assume A3:
not n is prime
; ex k being non zero Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )
per cases
( n <= 1 or ex k being Nat st
( k divides n & not k = 1 & not k = n ) )
by A3, INT_2:def 4;
suppose
ex
k being
Nat st
(
k divides n & not
k = 1 & not
k = n )
;
ex k being non zero Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )then consider k being
Nat such that A4:
k divides n
and A5:
(
k <> 1 &
k <> n )
;
consider m being
Nat such that A6:
n = k * m
by A4, NAT_D:def 3;
A7:
(
m divides n &
m is non
zero Element of
NAT )
by A1, A6, NAT_D:def 3, ORDINAL1:def 12;
A8:
k is non
zero Element of
NAT
by A1, A4, INT_2:3, ORDINAL1:def 12;
A9:
(
k <> 2 or
m <> 2 )
by A2, A6;
(
m <> 1 &
m <> n )
by A1, A5, A6, XCMPLX_1:7;
hence
ex
k being non
zero Element of
NAT st
(
k <> 1 &
k <> 2 &
k <> n &
k divides n )
by A4, A5, A8, A7, A9;
verum end;