defpred S1[ Nat] means for M being Matrix of $1,F_Real st M is Matrix of $1,INT holds
Det M in INT ;
P0: S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume P10: S1[n] ; :: thesis: S1[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 ) ;
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 S1[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