defpred S1[ Nat] means for M being Matrix of \$1,F_Real st M is Matrix of \$1,F_Rat holds
Det M in F_Rat ;
P0: S1[ 0 ]
proof
let M be Matrix of 0 ,F_Real; :: thesis: ( M is Matrix of 0 ,F_Rat implies Det M in F_Rat )
assume M is Matrix of 0 ,F_Rat ; :: thesis:
Det M = 1. F_Real by MATRIXR2:41
.= 1 ;
hence Det M in F_Rat ; :: 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,F_Rat implies Det M in F_Rat )
assume AS1: M is Matrix of n + 1,F_Rat ; :: thesis:
reconsider j = 1 as Nat ;
X0: ( 1 <= 1 & 1 <= n + 1 ) by NAT_1:14;
then j in Seg (n + 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 F_Rat
proof
let i be Nat; :: thesis: ( i in dom (LaplaceExpC (M,j)) implies (LaplaceExpC (M,j)) . i in F_Rat )
assume X30: i in dom (LaplaceExpC (M,j)) ; :: thesis: (LaplaceExpC (M,j)) . i in F_Rat
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 ;
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 F_Rat by ;
(n + 1) -' 1 = n by NAT_D:34;
then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;
Det DD in F_Rat
proof
per cases ( 0 < n or not 0 < n ) ;
end;
end;
then A1: Minor (M,i,j) in F_Rat by NAT_D:34;
(power F_Real) . ((- ()),(i + j)) in F_Rat by LmSign1D;
hence (LaplaceExpC (M,j)) . i in F_Rat by ; :: thesis: verum
end;
hence Det M in F_Rat by ; :: 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,F_Rat holds
Det M in F_Rat ; :: thesis: verum