defpred S₁[ Nat] means for M being Matrix of $1,F_Real st M is Matrix of $1,INT holds
Det M in INT ;
P0: S₁[ 0 ]

proof

let M be Matrix of 0 ,F_Real; :: thesis: ( M is Matrix of 0 ,INT implies Det M in INT )
assume M is Matrix of 0 ,INT ; :: thesis: Det M in INT
Det M = 1. F_Real by MATRIXR2:41
.= 1 ;
hence Det M in INT by INT_1:def 2; :: thesis: verum

end;

P1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume P10: S₁[n] ; :: thesis: S₁[n + 1]
let M be Matrix of n + 1,F_Real; :: thesis: ( M is Matrix of n + 1,INT implies Det M in INT )
assume AS1: M is Matrix of n + 1,INT ; :: thesis: Det M in INT
reconsider j = 1 as Nat ;
X0: ( 1 <= 1 & 1 <= n + 1 ) by NAT_1:14;
then j in Seg (n + 1) by FINSEQ_1:1;
then X1: Det M = Sum (LaplaceExpC (M,j)) by LAPLACE:27;
set L = LaplaceExpC (M,j);
X2: ( len (LaplaceExpC (M,j)) = n + 1 & ( for i being Nat st i in dom (LaplaceExpC (M,j)) holds
(LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) by LAPLACE:def 8;
for i being Nat st i in dom (LaplaceExpC (M,j)) holds
(LaplaceExpC (M,j)) . i in INT

proof

let i be Nat; :: thesis: ( i in dom (LaplaceExpC (M,j)) implies (LaplaceExpC (M,j)) . i in INT )
assume X30: i in dom (LaplaceExpC (M,j)) ; :: thesis: (LaplaceExpC (M,j)) . i in INT
then X31: (LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) by LAPLACE:def 8;
( i in Seg (n + 1) & j in Seg (n + 1) ) by X0, X2, X30, FINSEQ_1:def 3, FINSEQ_1:1;
then [i,j] in [:(Seg (n + 1)),(Seg (n + 1)):] by ZFMISC_1:87;
then X41: [i,j] in Indices M by MATRIX_0:24;
then X32: M * (i,j) is Element of INT by AS1, LmSign1B;
(n + 1) -' 1 = n by NAT_D:34;
then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;
Det DD in INT

proof

per cases ( 0 < n or not 0 < n ) ;

suppose 0 < n ; :: thesis: Det DD in INT

then DD is Matrix of n,INT by LmSign1E, AS1, X41;
hence Det DD in INT by P10; :: thesis: verum

end;

suppose not 0 < n ; :: thesis: Det DD in INT

then n = 0 ;
then Det DD = 1. F_Real by MATRIXR2:41
.= 1 ;
hence Det DD in INT by INT_1:def 2; :: thesis: verum

end;

end;

end;

then Minor (M,i,j) in INT by NAT_D:34;
then Cofactor (M,i,j) in INT by LmSign1D;
hence (LaplaceExpC (M,j)) . i in INT by X32, X31, INT_1:def 2; :: thesis: verum

end;

hence Det M in INT by X1, LmSign1C; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P0, P1);
hence for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,INT holds
Det M in INT ; :: thesis: verum