let p be XFinSequence of NAT ; ( p is dominated_by_0 & { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} & len p > 0 implies ex q being XFinSequence of NAT st
( p = <%0%> ^ q & q is dominated_by_0 ) )
assume that
A1:
p is dominated_by_0
and
A2:
( { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} & len p > 0 )
; ex q being XFinSequence of NAT st
( p = <%0%> ^ q & q is dominated_by_0 )
set M = { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } ;
consider q being XFinSequence of NAT such that
A3:
p = (p | 1) ^ q
by Th1;
take
q
; ( p = <%0%> ^ q & q is dominated_by_0 )
A4:
rng p c= {0,1}
by A1;
rng q c= rng p
by A3, AFINSQ_1:25;
then A5:
rng q c= {0,1}
by A4;
len p >= 1
by A2, NAT_1:14;
then
Segm 1 c= Segm (len p)
by NAT_1:39;
then A6:
dom (p | 1) = 1
by RELAT_1:62;
A7:
p | 1 = <%((p | 1) . 0)%>
by A6, AFINSQ_1:34;
0 in Segm 1
by NAT_1:44;
then A8:
(p | 1) . 0 = p . 0
by A6, FUNCT_1:47;
hence
p = <%0%> ^ q
by A1, A3, A7, Th3; q is dominated_by_0
assume
not q is dominated_by_0
; contradiction
then consider i being Nat such that
i <= dom q
and
A9:
2 * (Sum (q | i)) > i
by A5;
reconsider i = i as Nat ;
p | (1 + i) = (p | 1) ^ (q | i)
by A3, A6, AFINSQ_1:59;
then A10:
Sum (p | (1 + i)) = (Sum <%(p . 0)%>) + (Sum (q | i))
by A7, A8, AFINSQ_2:55;
A11:
2 * (Sum (q | i)) >= i + 1
by A9, NAT_1:13;
Sum <%(p . 0)%> = p . 0
by AFINSQ_2:53;
then A12:
Sum (p | (1 + i)) = 0 + (Sum (q | i))
by A1, A10, Th3;
then
1 + i >= 2 * (Sum (q | i))
by A1, Th2;
then
1 + i = 2 * (Sum (q | i))
by A11, XXREAL_0:1;
then
1 + i in { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) }
by A12;
hence
contradiction
by A2; verum