let x be Real; :: thesis: ( x is rational implies ex n being Nat st
( n >= 2 & (n !) * x is integer ) )

assume x is rational ; :: thesis: ex n being Nat st
( n >= 2 & (n !) * x is integer )

then consider i being Integer, n being Nat such that
A1: n <> 0 and
A2: x = i / n by RAT_1:8;
per cases ( n < 1 + 1 or n >= 2 ) ;
suppose A3: n < 1 + 1 ; :: thesis: ex n being Nat st
( n >= 2 & (n !) * x is integer )

A4: n >= 0 + 1 by ;
n <= 1 by ;
then n = 1 by ;
then reconsider x1 = x as Integer by A2;
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 A5: n >= 2 ; :: thesis: ex n being Nat st
( n >= 2 & (n !) * x is integer )

take n ; :: thesis: ( n >= 2 & (n !) * x is integer )
thus n >= 2 by A5; :: thesis: (n !) * x is integer
reconsider m = n - 1 as Element of NAT by ;
(n !) * x = ((m + 1) * (m !)) * x by NEWTON:15
.= (n * x) * (m !)
.= i * (m !) by ;
hence (n !) * x is integer ; :: thesis: verum
end;
end;