let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: for f being non empty FinSequence of NAT

for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k div 2 < Sum a

let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k div 2 < Sum a

let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & k = card (rng f) implies k div 2 < Sum a )

assume that

HL00: f = OnlinePacking (a,(NextFit a)) and

BK00: k = card (rng f) ; :: thesis: k div 2 < Sum a

consider k0 being Nat such that

B00: rng f = Seg k0 by HL00, NF910;

BN00: rng f = Seg k by FINSEQ_1:57, BK00, B00;

L00: dom f = dom a by HL00, NF540;

for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k div 2 < Sum a

let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k div 2 < Sum a

let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & k = card (rng f) implies k div 2 < Sum a )

assume that

HL00: f = OnlinePacking (a,(NextFit a)) and

BK00: k = card (rng f) ; :: thesis: k div 2 < Sum a

consider k0 being Nat such that

B00: rng f = Seg k0 by HL00, NF910;

BN00: rng f = Seg k by FINSEQ_1:57, BK00, B00;

L00: dom f = dom a by HL00, NF540;

per cases
( k = 1 or 2 <= k )
by BK00, NAT_1:23;

end;

suppose L55:
k = 1
; :: thesis: k div 2 < Sum a

L57:
for n being Nat st n in dom a holds

0 <= a . n by RVSUM_3:def 1;

L575: len a >= 1 by FINSEQ_1:20;

a is positive ;

then 0 < a . 1 by L575, FINSEQ_3:25;

then 0 < Sum a by L57, L575, FINSEQ_3:25, RVSUM_1:85;

hence k div 2 < Sum a by L55, NAT_D:27; :: thesis: verum

end;0 <= a . n by RVSUM_3:def 1;

L575: len a >= 1 by FINSEQ_1:20;

a is positive ;

then 0 < a . 1 by L575, FINSEQ_3:25;

then 0 < Sum a by L57, L575, FINSEQ_3:25, RVSUM_1:85;

hence k div 2 < Sum a by L55, NAT_D:27; :: thesis: verum

suppose L60:
2 <= k
; :: thesis: k div 2 < Sum a

set kd2 = k div 2;

reconsider kd2 = k div 2 as Element of NAT by INT_1:55, INT_1:3;

2 div 2 <= k div 2 by L60, NAT_2:24;

then L80: 1 <= kd2 by NAT_2:3;

deffunc H_{1}( Nat) -> set = (SumBin (a,f,{((2 * $1) - 1)})) + (SumBin (a,f,{(2 * $1)}));

ex p being FinSequence st

( len p = kd2 & ( for i being Nat st i in dom p holds

p . i = H_{1}(i) ) )
from FINSEQ_1:sch 2();

then consider SBP being FinSequence such that

L100: len SBP = kd2 and

L101: for i being Nat st i in dom SBP holds

SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) ;

deffunc H_{2}( Nat) -> Real = SumBin (a,f,{$1});

ex p being FinSequence st

( len p = 2 * kd2 & ( for j being Nat st j in dom p holds

p . j = H_{2}(j) ) )
from FINSEQ_1:sch 2();

then consider SB being FinSequence such that

L150: len SB = 2 * kd2 and

L151: for j being Nat st j in dom SB holds

SB . j = SumBin (a,f,{j}) ;

for i being Nat st i in dom SBP holds

SBP . i in REAL

SBP is kd2 -element by L100;

then reconsider SBP = SBP as kd2 -element real-valued FinSequence by LSBP55;

for j being Nat st j in dom SB holds

SB . j in REAL

SB is 2 * kd2 -element by L150;

then reconsider SB = SB as 2 * kd2 -element real-valued FinSequence by LSB55;

set R2 = kd2 |-> 1;

reconsider R2 = kd2 |-> 1 as kd2 -element real-valued FinSequence ;

L170: Sum R2 = kd2 * 1 by RVSUM_1:80;

L175: for i being Nat st i in Seg kd2 holds

R2 . i < SBP . i

R2 . i <= SBP . i by L175;

ex i being Nat st

( i in Seg kd2 & R2 . i < SBP . i )

defpred S_{1}[ Nat] means for SBPi, SBi being real-valued FinSequence st SBPi = SBP | (Seg $1) & SBi = SB | (Seg (2 * $1)) holds

Sum SBPi = Sum SBi;

for SBP1, SB1 being real-valued FinSequence st SBP1 = SBP | (Seg 1) & SB1 = SB | (Seg (2 * 1)) holds

Sum SBP1 = Sum SB1_{1}[1]
;

L260: for i being Element of NAT st 1 <= i & i < kd2 & S_{1}[i] holds

S_{1}[i + 1]

S_{1}[i]
from INT_1:sch 7(L230, L260);

L298: SBP = SBP | (dom SBP)

.= SBP | (Seg kd2) by L100, FINSEQ_1:def 3 ;

SB = SB | (dom SB)

.= SB | (Seg (2 * kd2)) by L150, FINSEQ_1:def 3 ;

then L300: Sum SBP = Sum SB by L80, L298, L289;

deffunc H_{3}( Nat) -> Real = SumBin (a,f,{$1});

ex p being FinSequence st

( len p = k & ( for j being Nat st j in dom p holds

p . j = H_{3}(j) ) )
from FINSEQ_1:sch 2();

then consider R1 being FinSequence such that

LL40: len R1 = k and

LL41: for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ;

for j being Nat st j in dom R1 holds

R1 . j in REAL

R1 is k -element by LL40;

then reconsider R1 = R1 as k -element real-valued FinSequence by LL55;

L500: Sum SB <= Sum R1

.= Sum a by L00, NF260 ;

hence k div 2 < Sum a by L200, L300, L500, XXREAL_0:2; :: thesis: verum

end;reconsider kd2 = k div 2 as Element of NAT by INT_1:55, INT_1:3;

2 div 2 <= k div 2 by L60, NAT_2:24;

then L80: 1 <= kd2 by NAT_2:3;

deffunc H

ex p being FinSequence st

( len p = kd2 & ( for i being Nat st i in dom p holds

p . i = H

then consider SBP being FinSequence such that

L100: len SBP = kd2 and

L101: for i being Nat st i in dom SBP holds

SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) ;

deffunc H

ex p being FinSequence st

( len p = 2 * kd2 & ( for j being Nat st j in dom p holds

p . j = H

then consider SB being FinSequence such that

L150: len SB = 2 * kd2 and

L151: for j being Nat st j in dom SB holds

SB . j = SumBin (a,f,{j}) ;

for i being Nat st i in dom SBP holds

SBP . i in REAL

proof

then LSBP55:
SBP is FinSequence of REAL
by NF315;
let i be Nat; :: thesis: ( i in dom SBP implies SBP . i in REAL )

assume i in dom SBP ; :: thesis: SBP . i in REAL

then SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) by L101;

hence SBP . i in REAL by XREAL_0:def 1; :: thesis: verum

end;assume i in dom SBP ; :: thesis: SBP . i in REAL

then SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) by L101;

hence SBP . i in REAL by XREAL_0:def 1; :: thesis: verum

SBP is kd2 -element by L100;

then reconsider SBP = SBP as kd2 -element real-valued FinSequence by LSBP55;

for j being Nat st j in dom SB holds

SB . j in REAL

proof

then LSB55:
SB is FinSequence of REAL
by NF315;
let j be Nat; :: thesis: ( j in dom SB implies SB . j in REAL )

assume j in dom SB ; :: thesis: SB . j in REAL

then SB . j = SumBin (a,f,{j}) by L151;

hence SB . j in REAL by XREAL_0:def 1; :: thesis: verum

end;assume j in dom SB ; :: thesis: SB . j in REAL

then SB . j = SumBin (a,f,{j}) by L151;

hence SB . j in REAL by XREAL_0:def 1; :: thesis: verum

SB is 2 * kd2 -element by L150;

then reconsider SB = SB as 2 * kd2 -element real-valued FinSequence by LSB55;

set R2 = kd2 |-> 1;

reconsider R2 = kd2 |-> 1 as kd2 -element real-valued FinSequence ;

L170: Sum R2 = kd2 * 1 by RVSUM_1:80;

L175: for i being Nat st i in Seg kd2 holds

R2 . i < SBP . i

proof

L180:
for i being Nat st i in Seg kd2 holds
let i be Nat; :: thesis: ( i in Seg kd2 implies R2 . i < SBP . i )

assume LR271: i in Seg kd2 ; :: thesis: R2 . i < SBP . i

Seg kd2 = dom SBP by L100, FINSEQ_1:def 3;

then LR278: SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) by LR271, L101;

LR279: R2 . i = 1 by LR271, FINSEQ_2:57;

( 1 <= i & i <= k div 2 ) by LR271, FINSEQ_1:1;

hence R2 . i < SBP . i by HL00, BN00, NF950, LR278, LR279; :: thesis: verum

end;assume LR271: i in Seg kd2 ; :: thesis: R2 . i < SBP . i

Seg kd2 = dom SBP by L100, FINSEQ_1:def 3;

then LR278: SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) by LR271, L101;

LR279: R2 . i = 1 by LR271, FINSEQ_2:57;

( 1 <= i & i <= k div 2 ) by LR271, FINSEQ_1:1;

hence R2 . i < SBP . i by HL00, BN00, NF950, LR278, LR279; :: thesis: verum

R2 . i <= SBP . i by L175;

ex i being Nat st

( i in Seg kd2 & R2 . i < SBP . i )

proof

then L200:
kd2 < Sum SBP
by L180, RVSUM_1:83, L170;
reconsider i0 = 1 as Nat ;

take i0 ; :: thesis: ( i0 in Seg kd2 & R2 . i0 < SBP . i0 )

i0 in Seg kd2 by L80;

hence ( i0 in Seg kd2 & R2 . i0 < SBP . i0 ) by L175; :: thesis: verum

end;take i0 ; :: thesis: ( i0 in Seg kd2 & R2 . i0 < SBP . i0 )

i0 in Seg kd2 by L80;

hence ( i0 in Seg kd2 & R2 . i0 < SBP . i0 ) by L175; :: thesis: verum

defpred S

Sum SBPi = Sum SBi;

for SBP1, SB1 being real-valued FinSequence st SBP1 = SBP | (Seg 1) & SB1 = SB | (Seg (2 * 1)) holds

Sum SBP1 = Sum SB1

proof

then L230:
S
let sbp1, sb1 be real-valued FinSequence; :: thesis: ( sbp1 = SBP | (Seg 1) & sb1 = SB | (Seg (2 * 1)) implies Sum sbp1 = Sum sb1 )

assume that

B00: sbp1 = SBP | (Seg 1) and

B01: sb1 = SB | (Seg (2 * 1)) ; :: thesis: Sum sbp1 = Sum sb1

Seg kd2 = dom SBP by FINSEQ_1:def 3, L100;

then B140: 1 in dom SBP by L80;

1 in Seg 1 ;

then B160: sbp1 . 1 = SBP . 1 by B00, FUNCT_1:49

.= (SumBin (a,f,{((2 * 1) - 1)})) + (SumBin (a,f,{(2 * 1)})) by B140, L101

.= (SumBin (a,f,{1})) + (SumBin (a,f,{2})) ;

dom sbp1 = Seg 1 by L100, L80, B00, FINSEQ_1:17;

then B180: sbp1 = <*((SumBin (a,f,{1})) + (SumBin (a,f,{2})))*> by B160, FINSEQ_1:def 8;

B220: Seg (2 * kd2) = dom SB by FINSEQ_1:def 3, L150;

B229: 1 * 2 <= kd2 * 2 by XREAL_1:64, L80;

then 2 - 1 <= (2 * kd2) - 0 by XREAL_1:13;

then B240: 1 in dom SB by B220;

B241: 2 in dom SB by B229, B220;

B250: 1 in Seg 2 ;

B251: 2 in Seg 2 ;

B260: sb1 . 1 = SB . 1 by B01, B250, FUNCT_1:49

.= SumBin (a,f,{1}) by B240, L151 ;

B261: sb1 . 2 = SB . 2 by B01, B251, FUNCT_1:49

.= SumBin (a,f,{2}) by B241, L151 ;

B263: 1 * 2 <= kd2 * 2 by XREAL_1:64, L80;

len sb1 = min (2,(len SB)) by B01, FINSEQ_2:21

.= 2 by B263, L150, XXREAL_0:def 9 ;

then B280: sb1 = <*(SumBin (a,f,{1})),(SumBin (a,f,{2}))*> by B260, B261, FINSEQ_1:44;

Sum sbp1 = (SumBin (a,f,{1})) + (SumBin (a,f,{2})) by B180, RVSUM_1:73

.= Sum sb1 by B280, RVSUM_1:77 ;

hence Sum sbp1 = Sum sb1 ; :: thesis: verum

end;assume that

B00: sbp1 = SBP | (Seg 1) and

B01: sb1 = SB | (Seg (2 * 1)) ; :: thesis: Sum sbp1 = Sum sb1

Seg kd2 = dom SBP by FINSEQ_1:def 3, L100;

then B140: 1 in dom SBP by L80;

1 in Seg 1 ;

then B160: sbp1 . 1 = SBP . 1 by B00, FUNCT_1:49

.= (SumBin (a,f,{((2 * 1) - 1)})) + (SumBin (a,f,{(2 * 1)})) by B140, L101

.= (SumBin (a,f,{1})) + (SumBin (a,f,{2})) ;

dom sbp1 = Seg 1 by L100, L80, B00, FINSEQ_1:17;

then B180: sbp1 = <*((SumBin (a,f,{1})) + (SumBin (a,f,{2})))*> by B160, FINSEQ_1:def 8;

B220: Seg (2 * kd2) = dom SB by FINSEQ_1:def 3, L150;

B229: 1 * 2 <= kd2 * 2 by XREAL_1:64, L80;

then 2 - 1 <= (2 * kd2) - 0 by XREAL_1:13;

then B240: 1 in dom SB by B220;

B241: 2 in dom SB by B229, B220;

B250: 1 in Seg 2 ;

B251: 2 in Seg 2 ;

B260: sb1 . 1 = SB . 1 by B01, B250, FUNCT_1:49

.= SumBin (a,f,{1}) by B240, L151 ;

B261: sb1 . 2 = SB . 2 by B01, B251, FUNCT_1:49

.= SumBin (a,f,{2}) by B241, L151 ;

B263: 1 * 2 <= kd2 * 2 by XREAL_1:64, L80;

len sb1 = min (2,(len SB)) by B01, FINSEQ_2:21

.= 2 by B263, L150, XXREAL_0:def 9 ;

then B280: sb1 = <*(SumBin (a,f,{1})),(SumBin (a,f,{2}))*> by B260, B261, FINSEQ_1:44;

Sum sbp1 = (SumBin (a,f,{1})) + (SumBin (a,f,{2})) by B180, RVSUM_1:73

.= Sum sb1 by B280, RVSUM_1:77 ;

hence Sum sbp1 = Sum sb1 ; :: thesis: verum

L260: for i being Element of NAT st 1 <= i & i < kd2 & S

S

proof

L289:
for i being Element of NAT st 1 <= i & i <= kd2 holds
let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < kd2 & S_{1}[i0] implies S_{1}[i0 + 1] )

assume that

1 <= i0 and

A262: i0 < kd2 and

A263: S_{1}[i0]
; :: thesis: S_{1}[i0 + 1]

reconsider sbpi0 = SBP | (Seg i0) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbi0 = SB | (Seg (2 * i0)) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbpi0p = SBP | (Seg (i0 + 1)) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbi0p = SB | (Seg (2 * (i0 + 1))) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbi0h = SB | (Seg ((2 * i0) + 1)) as real-valued FinSequence by FINSEQ_1:15;

A270: 1 <= i0 + 1 by NAT_1:12;

A271: i0 + 1 <= kd2 by A262, INT_1:7;

i0 + 1 in Seg kd2 by A270, A271;

then A272: i0 + 1 in dom SBP by L100, FINSEQ_1:def 3;

then A274: SBP . (i0 + 1) = (SumBin (a,f,{((2 * (i0 + 1)) - 1)})) + (SumBin (a,f,{(2 * (i0 + 1))})) by L101;

A280: Sum sbpi0p = Sum (sbpi0 ^ <*(SBP . (i0 + 1))*>) by A272, FINSEQ_5:10

.= (Sum sbpi0) + (SBP . (i0 + 1)) by RVSUM_1:74

.= ((Sum sbpi0) + (SumBin (a,f,{((2 * i0) + 1)}))) + (SumBin (a,f,{((2 * i0) + 2)})) by A274 ;

A300: 1 <= (2 * i0) + 2 by NAT_1:12;

A304: 2 * (i0 + 1) <= 2 * kd2 by A271, XREAL_1:64;

2 * (i0 + 1) in Seg (2 * kd2) by A300, A304;

then A320: (2 * i0) + 2 in dom SB by L150, FINSEQ_1:def 3;

A330: 1 <= (2 * i0) + 1 by NAT_1:12;

((2 * i0) + 2) - 1 <= (2 * kd2) - 0 by A304, XREAL_1:13;

then (2 * i0) + 1 in Seg (2 * kd2) by A330;

then A340: (2 * i0) + 1 in dom SB by L150, FINSEQ_1:def 3;

A370: SB | (Seg (2 * (i0 + 1))) = SB | (Seg (((2 * i0) + 1) + 1))

.= sbi0h ^ <*(SB . ((2 * i0) + 2))*> by A320, FINSEQ_5:10 ;

A380: sbi0h = sbi0 ^ <*(SB . ((2 * i0) + 1))*> by A340, FINSEQ_5:10;

A390: Sum sbi0h = (Sum sbi0) + (SB . ((2 * i0) + 1)) by A380, RVSUM_1:74

.= (Sum sbi0) + (SumBin (a,f,{((2 * i0) + 1)})) by A340, L151 ;

Sum sbi0p = (Sum sbi0h) + (SB . ((2 * i0) + 2)) by A370, RVSUM_1:74

.= ((Sum sbi0) + (SumBin (a,f,{((2 * i0) + 1)}))) + (SumBin (a,f,{((2 * i0) + 2)})) by A320, L151, A390 ;

hence for SBPi, SBi being real-valued FinSequence st SBPi = SBP | (Seg (i0 + 1)) & SBi = SB | (Seg (2 * (i0 + 1))) holds

Sum SBPi = Sum SBi by A280, A263; :: thesis: verum

end;assume that

1 <= i0 and

A262: i0 < kd2 and

A263: S

reconsider sbpi0 = SBP | (Seg i0) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbi0 = SB | (Seg (2 * i0)) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbpi0p = SBP | (Seg (i0 + 1)) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbi0p = SB | (Seg (2 * (i0 + 1))) as real-valued FinSequence by FINSEQ_1:15;

reconsider sbi0h = SB | (Seg ((2 * i0) + 1)) as real-valued FinSequence by FINSEQ_1:15;

A270: 1 <= i0 + 1 by NAT_1:12;

A271: i0 + 1 <= kd2 by A262, INT_1:7;

i0 + 1 in Seg kd2 by A270, A271;

then A272: i0 + 1 in dom SBP by L100, FINSEQ_1:def 3;

then A274: SBP . (i0 + 1) = (SumBin (a,f,{((2 * (i0 + 1)) - 1)})) + (SumBin (a,f,{(2 * (i0 + 1))})) by L101;

A280: Sum sbpi0p = Sum (sbpi0 ^ <*(SBP . (i0 + 1))*>) by A272, FINSEQ_5:10

.= (Sum sbpi0) + (SBP . (i0 + 1)) by RVSUM_1:74

.= ((Sum sbpi0) + (SumBin (a,f,{((2 * i0) + 1)}))) + (SumBin (a,f,{((2 * i0) + 2)})) by A274 ;

A300: 1 <= (2 * i0) + 2 by NAT_1:12;

A304: 2 * (i0 + 1) <= 2 * kd2 by A271, XREAL_1:64;

2 * (i0 + 1) in Seg (2 * kd2) by A300, A304;

then A320: (2 * i0) + 2 in dom SB by L150, FINSEQ_1:def 3;

A330: 1 <= (2 * i0) + 1 by NAT_1:12;

((2 * i0) + 2) - 1 <= (2 * kd2) - 0 by A304, XREAL_1:13;

then (2 * i0) + 1 in Seg (2 * kd2) by A330;

then A340: (2 * i0) + 1 in dom SB by L150, FINSEQ_1:def 3;

A370: SB | (Seg (2 * (i0 + 1))) = SB | (Seg (((2 * i0) + 1) + 1))

.= sbi0h ^ <*(SB . ((2 * i0) + 2))*> by A320, FINSEQ_5:10 ;

A380: sbi0h = sbi0 ^ <*(SB . ((2 * i0) + 1))*> by A340, FINSEQ_5:10;

A390: Sum sbi0h = (Sum sbi0) + (SB . ((2 * i0) + 1)) by A380, RVSUM_1:74

.= (Sum sbi0) + (SumBin (a,f,{((2 * i0) + 1)})) by A340, L151 ;

Sum sbi0p = (Sum sbi0h) + (SB . ((2 * i0) + 2)) by A370, RVSUM_1:74

.= ((Sum sbi0) + (SumBin (a,f,{((2 * i0) + 1)}))) + (SumBin (a,f,{((2 * i0) + 2)})) by A320, L151, A390 ;

hence for SBPi, SBi being real-valued FinSequence st SBPi = SBP | (Seg (i0 + 1)) & SBi = SB | (Seg (2 * (i0 + 1))) holds

Sum SBPi = Sum SBi by A280, A263; :: thesis: verum

S

L298: SBP = SBP | (dom SBP)

.= SBP | (Seg kd2) by L100, FINSEQ_1:def 3 ;

SB = SB | (dom SB)

.= SB | (Seg (2 * kd2)) by L150, FINSEQ_1:def 3 ;

then L300: Sum SBP = Sum SB by L80, L298, L289;

deffunc H

ex p being FinSequence st

( len p = k & ( for j being Nat st j in dom p holds

p . j = H

then consider R1 being FinSequence such that

LL40: len R1 = k and

LL41: for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ;

for j being Nat st j in dom R1 holds

R1 . j in REAL

proof

then LL55:
R1 is FinSequence of REAL
by NF315;
let j be Nat; :: thesis: ( j in dom R1 implies R1 . j in REAL )

assume j in dom R1 ; :: thesis: R1 . j in REAL

then R1 . j = SumBin (a,f,{j}) by LL41;

hence R1 . j in REAL by XREAL_0:def 1; :: thesis: verum

end;assume j in dom R1 ; :: thesis: R1 . j in REAL

then R1 . j = SumBin (a,f,{j}) by LL41;

hence R1 . j in REAL by XREAL_0:def 1; :: thesis: verum

R1 is k -element by LL40;

then reconsider R1 = R1 as k -element real-valued FinSequence by LL55;

L500: Sum SB <= Sum R1

proof
end;

Sum R1 =
SumBin (a,f,(rng f))
by L00, FINSEQ_1:57, BK00, B00, LL40, LL41, NF310
per cases
( k is even or k is odd )
;

end;

suppose L530:
k is even
; :: thesis: Sum SB <= Sum R1

L539:
k div 2 = k / 2
by L530, NAT_6:4;

SB = R1

end;SB = R1

proof

hence
Sum SB <= Sum R1
; :: thesis: verum
L5505:
dom R1 = Seg (2 * kd2)
by LL40, L539, FINSEQ_1:def 3;

L5510: dom SB = Seg (2 * kd2) by L150, FINSEQ_1:def 3;

for k0 being Nat st k0 in dom SB holds

SB . k0 = R1 . k0

end;L5510: dom SB = Seg (2 * kd2) by L150, FINSEQ_1:def 3;

for k0 being Nat st k0 in dom SB holds

SB . k0 = R1 . k0

proof

hence
SB = R1
by L5505, L5510, FINSEQ_1:13; :: thesis: verum
let k0 be Nat; :: thesis: ( k0 in dom SB implies SB . k0 = R1 . k0 )

assume L55310: k0 in dom SB ; :: thesis: SB . k0 = R1 . k0

SB . k0 = SumBin (a,f,{k0}) by L55310, L151;

hence SB . k0 = R1 . k0 by L55310, L5505, L5510, LL41; :: thesis: verum

end;assume L55310: k0 in dom SB ; :: thesis: SB . k0 = R1 . k0

SB . k0 = SumBin (a,f,{k0}) by L55310, L151;

hence SB . k0 = R1 . k0 by L55310, L5505, L5510, LL41; :: thesis: verum

suppose L560:
k is odd
; :: thesis: Sum SB <= Sum R1

L569:
k div 2 = (k - 1) / 2
by L560, NAT_6:5;

reconsider r12kd2 = R1 | (Seg (2 * kd2)) as real-valued FinSequence by FINSEQ_1:15;

L580: SB = r12kd2

(2 * 0) + 1 <= (2 * kd2) + 1 by XREAL_1:7;

then L587: (2 * kd2) + 1 in dom R1 by L584;

R1 = R1 | (dom R1)

.= R1 | (Seg ((2 * kd2) + 1)) by LL40, FINSEQ_1:def 3, L569

.= r12kd2 ^ <*(R1 . ((2 * kd2) + 1))*> by L587, FINSEQ_5:10

.= SB ^ <*(SumBin (a,f,{((2 * kd2) + 1)}))*> by L587, LL41, L580 ;

then Sum R1 = (Sum SB) + (SumBin (a,f,{((2 * kd2) + 1)})) by RVSUM_1:74;

then SumBin (a,f,{((2 * kd2) + 1)}) = (Sum R1) - (Sum SB) ;

then Sum SB <= (Sum R1) - 0 by NF280, XREAL_1:11;

hence Sum SB <= Sum R1 ; :: thesis: verum

end;reconsider r12kd2 = R1 | (Seg (2 * kd2)) as real-valued FinSequence by FINSEQ_1:15;

L580: SB = r12kd2

proof

L584:
Seg ((2 * kd2) + 1) = dom R1
by LL40, FINSEQ_1:def 3, L569;
((2 * kd2) + 1) - 1 <= k - 0
by L569, XREAL_1:13;

then L5805: dom r12kd2 = Seg (2 * kd2) by LL40, FINSEQ_1:17;

L5810: dom SB = Seg (2 * kd2) by L150, FINSEQ_1:def 3;

for k0 being Nat st k0 in dom SB holds

SB . k0 = r12kd2 . k0

end;then L5805: dom r12kd2 = Seg (2 * kd2) by LL40, FINSEQ_1:17;

L5810: dom SB = Seg (2 * kd2) by L150, FINSEQ_1:def 3;

for k0 being Nat st k0 in dom SB holds

SB . k0 = r12kd2 . k0

proof

hence
SB = r12kd2
by L5805, L5810, FINSEQ_1:13; :: thesis: verum
let k0 be Nat; :: thesis: ( k0 in dom SB implies SB . k0 = r12kd2 . k0 )

assume L58310: k0 in dom SB ; :: thesis: SB . k0 = r12kd2 . k0

L58329: dom r12kd2 c= dom R1 by RELAT_1:60;

k0 in Seg (2 * kd2) by L58310, L150, FINSEQ_1:def 3;

then r12kd2 . k0 = R1 . k0 by FUNCT_1:49

.= SumBin (a,f,{k0}) by L58329, L58310, L5805, L5810, LL41 ;

hence SB . k0 = r12kd2 . k0 by L58310, L151; :: thesis: verum

end;assume L58310: k0 in dom SB ; :: thesis: SB . k0 = r12kd2 . k0

L58329: dom r12kd2 c= dom R1 by RELAT_1:60;

k0 in Seg (2 * kd2) by L58310, L150, FINSEQ_1:def 3;

then r12kd2 . k0 = R1 . k0 by FUNCT_1:49

.= SumBin (a,f,{k0}) by L58329, L58310, L5805, L5810, LL41 ;

hence SB . k0 = r12kd2 . k0 by L58310, L151; :: thesis: verum

(2 * 0) + 1 <= (2 * kd2) + 1 by XREAL_1:7;

then L587: (2 * kd2) + 1 in dom R1 by L584;

R1 = R1 | (dom R1)

.= R1 | (Seg ((2 * kd2) + 1)) by LL40, FINSEQ_1:def 3, L569

.= r12kd2 ^ <*(R1 . ((2 * kd2) + 1))*> by L587, FINSEQ_5:10

.= SB ^ <*(SumBin (a,f,{((2 * kd2) + 1)}))*> by L587, LL41, L580 ;

then Sum R1 = (Sum SB) + (SumBin (a,f,{((2 * kd2) + 1)})) by RVSUM_1:74;

then SumBin (a,f,{((2 * kd2) + 1)}) = (Sum R1) - (Sum SB) ;

then Sum SB <= (Sum R1) - 0 by NF280, XREAL_1:11;

hence Sum SB <= Sum R1 ; :: thesis: verum

.= Sum a by L00, NF260 ;

hence k div 2 < Sum a by L200, L300, L500, XXREAL_0:2; :: thesis: verum