let n, m be Nat; ( 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
; 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;
( k in Segm m implies ex x being Element of bool (Domin_0 (n,m)) st S1[k,x] )
assume
k in Segm m
;
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)
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
;
S1[k,NN]
thus
S1[
k,
NN]
;
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 ;
TARSKI:def 3 ( 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 ) } <> {} ) }
;
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
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;
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;
( 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
;
C . i misses C . j
assume
C . i meets C . j
;
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;
verum
end;
A21:
for k being Nat st k in dom C holds
C . k is finite
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
; ( 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 ) } <> {} ) }
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; 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; ( 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
; 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; verum