let x be real number ; :: thesis: ( not x is irrational implies ex n being Element of NAT st
( n >= 2 & (n ! ) * x is integer ) )
assume not x is irrational ; :: thesis: ex n being Element of NAT st
( n >= 2 & (n ! ) * x is integer )
then consider i being Integer, n being Element of NAT such that
A1: ( n <> 0 & x = i / n ) by RAT_1:24;

per cases ( n < 1 + 1 or n >= 2 ) ;

suppose n < 1 + 1 ; :: thesis: ex n being Element of NAT st
( n >= 2 & (n ! ) * x is integer )

then A2: n <= 1 by NAT_1:13;
n > 0 by A1;
then n >= 0 + 1 by NAT_1:13;
then n = 1 by A2, XXREAL_0:1;
then reconsider x1 = x as Integer by A1;
take n = 2; :: thesis: ( n >= 2 & (n ! ) * x is integer )
(n ! ) * x1 is integer ;
hence ( n >= 2 & (n ! ) * x is integer ) ; :: thesis: verum

end;

suppose A3: n >= 2 ; :: thesis: ex n being Element of NAT st
( n >= 2 & (n ! ) * x is integer )

take n ; :: thesis: ( n >= 2 & (n ! ) * x is integer )
thus n >= 2 by A3; :: thesis: (n ! ) * x is integer
reconsider m = n - 1 as Element of NAT by A3, INT_1:18, XXREAL_0:2;
(n ! ) * x = ((m + 1) * (m ! )) * x by NEWTON:21
.= (n * x) * (m ! )
.= i * (m ! ) by A1, XCMPLX_1:88 ;
hence (n ! ) * x is integer ; :: thesis: verum

end;

end;