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;

( 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 )
;

end;

suppose A3:
n < 1 + 1
; :: thesis: ex n being Nat st

( n >= 2 & (n !) * x is integer )

( 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;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

suppose A5:
n >= 2
; :: thesis: ex n being Nat st

( n >= 2 & (n !) * x is integer )

( 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;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