let m be Element of NAT ; :: thesis: for p being XFinSequence of st m = min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } & m > 0 & p is dominated_by_0 holds
ex q being XFinSequence of st
( p | m = ((1 --> 0 ) ^ q) ^ (1 --> 1) & q is dominated_by_0 )
let p be XFinSequence of ; :: thesis: ( m = min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } & m > 0 & p is dominated_by_0 implies ex q being XFinSequence of st
( p | m = ((1 --> 0 ) ^ q) ^ (1 --> 1) & q is dominated_by_0 ) )
assume that
A1:
( m = min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } & m > 0 )
and
A2:
p is dominated_by_0
; :: thesis: ex q being XFinSequence of st
( p | m = ((1 --> 0 ) ^ q) ^ (1 --> 1) & q is dominated_by_0 )
reconsider M = { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } as non empty Subset of NAT by A1, NAT_1:def 1;
min* M in M
by NAT_1:def 1;
then consider n being Element of NAT such that
A3:
( n = min* M & 2 * (Sum (p | n)) = n & n > 0 )
;
reconsider n1 = n - 1 as Element of NAT by A3, NAT_1:20;
Sum (p | n) <> 0
by A3;
then
n >= 2 * 1
by A3, NAT_1:14, XREAL_1:66;
then A4:
n1 >= 2 - 1
by XREAL_1:11;
consider q being XFinSequence of such that
A5:
p | n1 = ((p | n1) | 1) ^ q
by Th5;
take
q
; :: thesis: ( p | m = ((1 --> 0 ) ^ q) ^ (1 --> 1) & q is dominated_by_0 )
set q0 = 1 --> 0 ;
set q1 = 1 --> 1;
set qq = ((1 --> 0 ) ^ q) ^ (1 --> 1);
( n <= len p & n1 < n1 + 1 )
by A2, A3, Th15, NAT_1:13;
then A6:
n1 < len p
by XXREAL_0:2;
then
1 < len p
by A4, XXREAL_0:2;
then
( len (p | 1) = 1 & p | 1 is dominated_by_0 )
by A2, Th10, AFINSQ_1:14;
then
( p | 1 = <%((p | 1) . 0 )%> & (p | 1) . 0 = 0 & dom <%0 %> = 1 & rng <%0 %> = {0 } & 1 c= n1 )
by A4, Th7, AFINSQ_1:36, AFINSQ_1:38, NAT_1:40;
then A7:
( p | 1 = 1 --> 0 & (p | n1) | 1 = p | 1 & p | (n1 + 1) = (p | n1) ^ (1 --> 1) )
by A2, A3, Th17, FUNCOP_1:15, RELAT_1:103;
hence
p | m = ((1 --> 0 ) ^ q) ^ (1 --> 1)
by A1, A3, A5; :: thesis: q is dominated_by_0
( rng q c= rng ((1 --> 0 ) ^ q) & rng ((1 --> 0 ) ^ q) c= rng (((1 --> 0 ) ^ q) ^ (1 --> 1)) & p | m is dominated_by_0 )
by A2, Th10, AFINSQ_1:27, AFINSQ_1:28;
then
( rng q c= rng (((1 --> 0 ) ^ q) ^ (1 --> 1)) & rng (((1 --> 0 ) ^ q) ^ (1 --> 1)) c= {0 ,1} )
by A1, A3, A5, A7, Def1, XBOOLE_1:1;
hence
rng q c= {0 ,1}
by XBOOLE_1:1; :: according to CATALAN2:def 1 :: thesis: for k being Element of NAT st k <= dom q holds
2 * (Sum (q | k)) <= k
let k be Element of NAT ; :: thesis: ( k <= dom q implies 2 * (Sum (q | k)) <= k )
assume A8:
k <= dom q
; :: thesis: 2 * (Sum (q | k)) <= k
len (p | n1) = n1
by A6, AFINSQ_1:14;
then
( n1 = (len (1 --> 0 )) + (len q) & len q = dom q )
by A5, A7, AFINSQ_1:20;
then
(len (1 --> 0 )) + k <= n1
by A8, XREAL_1:8;
then
( dom (1 --> 0 ) = 1 & (len (1 --> 0 )) + k c= n1 & len (1 --> 0 ) = dom (1 --> 0 ) )
by FUNCOP_1:19, NAT_1:40;
then
( (p | n1) | (1 + k) = (1 --> 0 ) ^ (q | k) & (p | n1) | (1 + k) = p | (1 + k) & 1 + k <= n1 & n1 < n )
by A5, A7, Th3, NAT_1:13, NAT_1:40, RELAT_1:103;
then A9:
( Sum (p | (1 + k)) = (Sum (1 --> 0 )) + (Sum (q | k)) & 1 + k < n & Sum (1 --> 0 ) = 0 * 1 )
by Lm2, Lm4, XXREAL_0:2;
2 * (Sum (p | (1 + k))) < 1 + k
hence
2 * (Sum (q | k)) <= k
by A9, NAT_1:13; :: thesis: verum