defpred S1[ Nat] means for X being finite Subset of RAT st card X = $1 holds
ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) );
P1: S1[ 0 ]
proof
let X be finite Subset of RAT; :: thesis: ( card X = 0 implies ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) )
assume AS: card X = 0 ; :: thesis: ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
reconsider a = 1 as Element of INT by NUMBERS:17;
take a ; :: thesis: ( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
thus a <> 0 ; :: thesis: for r being Element of RAT st r in X holds
a * r in INT
thus for r being Element of RAT st r in X holds
a * r in INT by AS; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AS1: S1[n] ; :: thesis: S1[n + 1]
let X be finite Subset of RAT; :: thesis: ( card X = n + 1 implies ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) )
assume AS2: card X = n + 1 ; :: thesis: ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
then X <> {} ;
then consider x being object such that
A1: x in X by XBOOLE_0:def 1;
B6: {x} is Subset of X by A1, SUBSET_1:41;
set Y = X \ {x};
reconsider Y = X \ {x} as finite Subset of RAT ;
D1: X = Y \/ {x} by B6, XBOOLE_1:45;
card Y = (card X) - (card {x}) by B6, CARD_2:44
.= (n + 1) - 1 by AS2, CARD_1:30
.= n ;
then consider a0 being Element of INT such that
A4: a0 <> 0 and
A5: for r being Element of RAT st r in Y holds
a0 * r in INT by AS1;
reconsider x = x as Element of RAT by A1;
consider x0, ib0 being Integer such that
A6: ( ib0 <> 0 & x = x0 / ib0 ) by RAT_1:1;
reconsider ia0 = a0 as Integer ;
set ia = ia0 * ib0;
reconsider a = ia0 * ib0 as Element of INT by INT_1:def 2;
for r being Element of RAT st r in X holds
a * r in INT
proof
let r be Element of RAT ; :: thesis: ( r in X implies a * r in INT )
assume r in X ; :: thesis: a * r in INT
per cases then ( r in Y or r in {x} ) by D1, XBOOLE_0:def 3;
suppose r in Y ; :: thesis: a * r in INT
then reconsider iar = ia0 * r as Integer by A5, INT_1:def 2;
a * r = ib0 * iar ;
hence a * r in INT by INT_1:def 2; :: thesis: verum
end;
suppose A72: r in {x} ; :: thesis: a * r in INT
a * r = ia0 * (ib0 * r)
.= ia0 * (ib0 * (x0 / ib0)) by A6, A72, TARSKI:def 1
.= ia0 * x0 by A6, XCMPLX_1:87 ;
hence a * r in INT by INT_1:def 2; :: thesis: verum
end;
end;
end;
hence ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) by A4, A6; :: thesis: verum
end;
P3: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
 let X be finite Subset of RAT; :: thesis: ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
card X is Nat ;
hence ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) by P3; :: thesis: verum