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 ]
P1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume P10:
S1[
n]
;
S1[n + 1]
let M be
Matrix of
n + 1,
F_Real;
( M is Matrix of n + 1,INT implies Det M in INT )
assume AS1:
M is
Matrix of
n + 1,
INT
;
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;
( i in dom (LaplaceExpC (M,j)) implies (LaplaceExpC (M,j)) . i in INT )
assume X30:
i in dom (LaplaceExpC (M,j))
;
(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
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;
verum
end;
hence
Det M in INT
by X1, LmSign1C;
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
; verum