let n, m be Nat; :: thesis: ( 2 * m <= n implies ex CardF being XFinSequence of NAT st
( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardF & dom CardF = m & ( for j being Nat st j < m holds
CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) ) )
assume A1: 2 * m <= n ; :: thesis: ex CardF being XFinSequence of NAT st
( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardF & dom CardF = m & ( for j being Nat st j < m holds
CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) )
set Z = Domin_0 (n,m);
defpred S1[ set , set ] means for j being Nat st j = $1 holds
$2 = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ;
set W = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } ;
A2: for k being Nat st k in Segm m holds
ex x being Element of bool (Domin_0 (n,m)) st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Segm m implies ex x being Element of bool (Domin_0 (n,m)) st S1[k,x] )
assume k in Segm m ; :: thesis: ex x being Element of bool (Domin_0 (n,m)) st S1[k,x]
set NN = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ;
{ pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } c= Domin_0 (n,m)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } or x in Domin_0 (n,m) )
assume x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ; :: thesis: x in Domin_0 (n,m)
then ex pN being Element of NAT ^omega st
( x = pN & pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) ;
hence x in Domin_0 (n,m) ; :: thesis: verum
end;
then reconsider NN = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } as Element of bool (Domin_0 (n,m)) ;
take NN ; :: thesis: S1[k,NN]
thus S1[k,NN] ; :: thesis: verum
end;
consider C being XFinSequence of bool (Domin_0 (n,m)) such that
A3: ( dom C = Segm m & ( for k being Nat st k in Segm m holds
S1[k,C . k] ) ) from STIRL2_1:sch 5(A2);
 A4: { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } c= union (rng C)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } or x in union (rng C) )
assume x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } ; :: thesis: x in union (rng C)
then consider pN being Element of NAT ^omega such that
A5: ( x = pN & pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) ;
set I = { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ;
{ N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } c= NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } or y in NAT )
assume y in { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ; :: thesis: y in NAT
then ex i being Nat st
( i = y & 2 * (Sum (pN | i)) = i & i > 0 ) ;
hence y in NAT by ORDINAL1:def 12; :: thesis: verum
end;
then reconsider I = { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } as non empty Subset of NAT by A5;
min* I in I by NAT_1:def 1;
then consider M being Nat such that
A6: min* I = M and
A7: 2 * (Sum (pN | M)) = M and
A8: M > 0 ;
Sum (pN | M) > 0 by A7, A8;
then reconsider Sum1 = (Sum (pN | M)) - 1 as Nat by NAT_1:20;
consider q being XFinSequence of NAT such that
A9: pN = (pN | M) ^ q by Th1;
Sum pN = (Sum (pN | M)) + (Sum q) by A9, AFINSQ_2:55;
then m = (Sum (pN | M)) + (Sum q) by A5, Th20;
then A10: m >= Sum (pN | M) by NAT_1:11;
Sum1 + 1 > Sum1 by NAT_1:13;
then m > Sum1 by A10, XXREAL_0:2;
then A11: Sum1 in Segm m by NAT_1:44;
then C . Sum1 = { qN where qN is Element of NAT ^omega : ( qN in Domin_0 (n,m) & 2 * (Sum1 + 1) = min* { N where N is Nat : ( 2 * (Sum (qN | N)) = N & N > 0 ) } ) } by A3;
then A12: pN in C . Sum1 by A5, A6, A7;
C . Sum1 in rng C by A3, A11, FUNCT_1:3;
hence x in union (rng C) by A5, A12, TARSKI:def 4; :: thesis: verum
end;
A13: for i, j being Nat st i in dom C & j in dom C & i <> j holds
C . i misses C . j
proof
let i, j be Nat; :: thesis: ( i in dom C & j in dom C & i <> j implies C . i misses C . j )
assume that
A14: i in dom C and
A15: j in dom C and
A16: i <> j ; :: thesis: C . i misses C . j
assume C . i meets C . j ; :: thesis: contradiction
then (C . i) /\ (C . j) <> {} ;
then consider x being object such that
A17: x in (C . i) /\ (C . j) by XBOOLE_0:def 1;
A18: x in C . j by A17, XBOOLE_0:def 4;
C . j = { qN where qN is Element of NAT ^omega : ( qN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (qN | N)) = N & N > 0 ) } ) } by A3, A15;
then A19: ex qN being Element of NAT ^omega st
( x = qN & qN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (qN | N)) = N & N > 0 ) } ) by A18;
A20: x in C . i by A17, XBOOLE_0:def 4;
C . i = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (i + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } by A3, A14;
then ex pN being Element of NAT ^omega st
( x = pN & pN in Domin_0 (n,m) & 2 * (i + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) by A20;
hence contradiction by A16, A19; :: thesis: verum
end;
A21: for k being Nat st k in dom C holds
C . k is finite
proof
let k be Nat; :: thesis: ( k in dom C implies C . k is finite )
assume k in dom C ; :: thesis: C . k is finite
then A22: C . k in rng C by FUNCT_1:3;
thus C . k is finite by A22; :: thesis: verum
end;
consider CardC being XFinSequence of NAT such that
A23: dom CardC = dom C and
A24: for i being Nat st i in dom CardC holds
CardC . i = card (C . i) and
A25: card (union (rng C)) = Sum CardC by A21, A13, STIRL2_1:66;
take CardC ; :: thesis: ( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardC & dom CardC = m & ( for j being Nat st j < m holds
CardC . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) )
union (rng C) c= { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng C) or x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } )
assume x in union (rng C) ; :: thesis: x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) }
then consider y being set such that
A26: x in y and
A27: y in rng C by TARSKI:def 4;
consider j being object such that
A28: j in dom C and
A29: C . j = y by A27, FUNCT_1:def 3;
reconsider j = j as Nat by A28;
y = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } by A3, A28, A29;
then consider pN being Element of NAT ^omega such that
A30: ( x = pN & pN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) by A26;
2 * (j + 1) <> 0 ;
then { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} by A30, NAT_1:def 1;
hence x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } by A30; :: thesis: verum
end;
hence ( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardC & dom CardC = m ) by A3, A23, A25, A4, XBOOLE_0:def 10; :: thesis: for j being Nat st j < m holds
CardC . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1)))))
let j be Nat; :: thesis: ( j < m implies CardC . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) )
assume A31: j < m ; :: thesis: CardC . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1)))))
A32: m >= j + 1 by A31, NAT_1:13;
then A33: m -' (j + 1) = m - (j + 1) by XREAL_1:233;
set P = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ;
j < len C by A3, A31;
then A34: j in dom C by A3, NAT_1:44;
then A35: C . j = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (j + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } by A3;
2 * (j + 1) <= 2 * m by A32, XREAL_1:64;
then A36: n -' (2 * (j + 1)) = n - (2 * (j + 1)) by A1, XREAL_1:233, XXREAL_0:2;
CardC . j = card (C . j) by A23, A24, A34;
hence CardC . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) by A36, A33, A35, Th36; :: thesis: verum