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 A1, NAT_1:13;
n <= 1 by A3, NAT_1:13;
then n = 1 by A4, XXREAL_0:1;
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 A5, INT_1:5, XXREAL_0:2;
(n !) * x = ((m + 1) * (m !)) * x by NEWTON:15
.= (n * x) * (m !)
.= i * (m !) by A1, A2, XCMPLX_1:87 ;
hence (n !) * x is integer ; :: thesis: verum
end;
end;