let n be Nat; :: thesis: (n !) * () is integer
defpred S1[ Nat] means ( \$1 <= n implies (n !) * ( . \$1) is integer );
now :: thesis: for k being Nat st ( k <= n implies (n !) * () is integer ) & k + 1 <= n holds
(n !) * ( . (k + 1)) is integer
let k be Nat; :: thesis: ( ( k <= n implies (n !) * () is integer ) & k + 1 <= n implies (n !) * ( . (k + 1)) is integer )
assume A1: ( k <= n implies (n !) * () is integer ) ; :: thesis: ( k + 1 <= n implies (n !) * ( . (k + 1)) is integer )
assume A2: k + 1 <= n ; :: thesis: (n !) * ( . (k + 1)) is integer
k + 0 <= k + 1 by XREAL_1:6;
then reconsider i = (n !) * () as Integer by ;
(n !) * (eseq . (k + 1)) = (n !) / ((k + 1) !) by Th32;
then reconsider j = (n !) * (eseq . (k + 1)) as Integer by ;
A3: i + j is Integer ;
(n !) * ( . (k + 1)) = (n !) * (() + (eseq . (k + 1))) by SERIES_1:def 1
.= ((n !) * ()) + ((n !) * (eseq . (k + 1))) ;
hence (n !) * ( . (k + 1)) is integer by A3; :: thesis: verum
end;
then A4: for k being Nat st S1[k] holds
S1[k + 1] ;
now :: thesis: ( 0 <= n implies (n !) * () is integer )
assume 0 <= n ; :: thesis: (n !) * () is integer
(n !) * () = (n !) * () by SERIES_1:def 1
.= (n !) / () by Th32 ;
hence (n !) * () is integer by Th36; :: thesis: verum
end;
then A5: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A5, A4);
hence (n !) * () is integer ; :: thesis: verum