let n be Nat; :: thesis: for epsilon being Real

for a being non empty positive at_most_one FinSequence of REAL st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) holds

Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)

let epsilon be Real; :: thesis: for a being non empty positive at_most_one FinSequence of REAL st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) holds

Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)

let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: ( n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) implies Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) )

assume that

L010: n is odd and

L030: len a = n and

L040: epsilon = 1 / (n + 1) and

L050: for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ; :: thesis: Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)

L020: 1 <= n by L010, NF992;

L060: (n + 1) div 2 = (n + 1) / 2 by L010, NF992;

defpred S_{1}[ Nat] means ( ( $1 is odd implies Sum (a | $1) = ((2 * epsilon) * (($1 + 1) div 2)) + ((1 - epsilon) * ((($1 + 1) div 2) - 1)) ) & ( $1 is even implies Sum (a | $1) = ((2 * epsilon) * ($1 div 2)) + ((1 - epsilon) * ($1 div 2)) ) );

L199: 1 = (2 * 0) + 1 ;

1 in Seg 1 ;

then (a | 1) . 1 = a . 1 by FUNCT_1:49;

then L230: a | 1 = <*(a . 1)*> by FINSEQ_1:40;

L231: 2 = (2 * 1) + 0 ;

2 / 2 = 1 ;

then L235: (1 + 1) div 2 = 1 by L231, NAT_6:4;

L238: 1 in Seg n by L020;

Sum (a | 1) = a . 1 by L230, RVSUM_1:73

.= ((2 * epsilon) * ((1 + 1) div 2)) + ((1 - epsilon) * (((1 + 1) div 2) - 1)) by L238, L199, L050, L235 ;

then L300: S_{1}[1]
;

L400: for i being Element of NAT st 1 <= i & i < len a & S_{1}[i] holds

S_{1}[i + 1]

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

Sum (a | n) = ((2 * epsilon) * ((n + 1) div 2)) + ((1 - epsilon) * (((n + 1) div 2) - 1)) by L020, L030, L010, L899

.= ((2 * ((1 / (n + 1)) * (n + 1))) / 2) + ((1 - (1 / (n + 1))) * (((n + 1) / 2) - 1)) by L060, L040

.= (2 / 2) + ((1 - (1 / (n + 1))) * (((n + 1) / 2) - 1)) by XCMPLX_1:87

.= (((n + 1) / 2) - (((1 / (n + 1)) * (n + 1)) / 2)) + (1 / (n + 1))

.= (((n + 1) / 2) - (1 / 2)) + (1 / (n + 1)) by XCMPLX_1:87

.= (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) ;

hence Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) by L030, FINSEQ_1:58; :: thesis: verum

for a being non empty positive at_most_one FinSequence of REAL st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) holds

Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)

let epsilon be Real; :: thesis: for a being non empty positive at_most_one FinSequence of REAL st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) holds

Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)

let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: ( n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) implies Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) )

assume that

L010: n is odd and

L030: len a = n and

L040: epsilon = 1 / (n + 1) and

L050: for i being Nat st i in Seg n holds

( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ; :: thesis: Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)

L020: 1 <= n by L010, NF992;

L060: (n + 1) div 2 = (n + 1) / 2 by L010, NF992;

defpred S

L199: 1 = (2 * 0) + 1 ;

1 in Seg 1 ;

then (a | 1) . 1 = a . 1 by FUNCT_1:49;

then L230: a | 1 = <*(a . 1)*> by FINSEQ_1:40;

L231: 2 = (2 * 1) + 0 ;

2 / 2 = 1 ;

then L235: (1 + 1) div 2 = 1 by L231, NAT_6:4;

L238: 1 in Seg n by L020;

Sum (a | 1) = a . 1 by L230, RVSUM_1:73

.= ((2 * epsilon) * ((1 + 1) div 2)) + ((1 - epsilon) * (((1 + 1) div 2) - 1)) by L238, L199, L050, L235 ;

then L300: S

L400: for i being Element of NAT st 1 <= i & i < len a & S

S

proof

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

assume that

1 <= i0 and

L411: i0 < len a and

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

reconsider i0p = i0 + 1 as Nat ;

L469: 1 + 0 <= i0 + 1 by XREAL_1:7;

i0p <= n by L411, L030, NAT_1:13;

then L490: i0p in Seg n by L469;

L500: ( i0p is odd implies Sum (a | i0p) = ((2 * epsilon) * ((i0p + 1) div 2)) + ((1 - epsilon) * (((i0p + 1) div 2) - 1)) )_{1}[i0 + 1]
by L500; :: thesis: verum

end;assume that

1 <= i0 and

L411: i0 < len a and

L412: S

reconsider i0p = i0 + 1 as Nat ;

L469: 1 + 0 <= i0 + 1 by XREAL_1:7;

i0p <= n by L411, L030, NAT_1:13;

then L490: i0p in Seg n by L469;

L500: ( i0p is odd implies Sum (a | i0p) = ((2 * epsilon) * ((i0p + 1) div 2)) + ((1 - epsilon) * (((i0p + 1) div 2) - 1)) )

proof

( i0p is even implies Sum (a | i0p) = ((2 * epsilon) * (i0p div 2)) + ((1 - epsilon) * (i0p div 2)) )
assume L510:
i0p is odd
; :: thesis: Sum (a | i0p) = ((2 * epsilon) * ((i0p + 1) div 2)) + ((1 - epsilon) * (((i0p + 1) div 2) - 1))

then L530: i0 is even ;

i0 / 2 = ((i0p + 1) / 2) - 1 ;

then i0 / 2 = ((i0p + 1) div 2) - 1 by L510, NAT_6:4;

then L580: i0 div 2 = ((i0p + 1) div 2) - 1 by L530, NAT_6:4;

thus Sum (a | i0p) = Sum ((a | i0) ^ <*(a . i0p)*>) by L411, FINSEQ_5:83

.= (Sum (a | i0)) + (a . i0p) by RVSUM_1:74

.= (((2 * epsilon) * (i0 div 2)) + ((1 - epsilon) * (i0 div 2))) + (2 * epsilon) by L050, L490, L510, L412

.= ((2 * epsilon) * ((i0p + 1) div 2)) + ((1 - epsilon) * (((i0p + 1) div 2) - 1)) by L580 ; :: thesis: verum

end;then L530: i0 is even ;

i0 / 2 = ((i0p + 1) / 2) - 1 ;

then i0 / 2 = ((i0p + 1) div 2) - 1 by L510, NAT_6:4;

then L580: i0 div 2 = ((i0p + 1) div 2) - 1 by L530, NAT_6:4;

thus Sum (a | i0p) = Sum ((a | i0) ^ <*(a . i0p)*>) by L411, FINSEQ_5:83

.= (Sum (a | i0)) + (a . i0p) by RVSUM_1:74

.= (((2 * epsilon) * (i0 div 2)) + ((1 - epsilon) * (i0 div 2))) + (2 * epsilon) by L050, L490, L510, L412

.= ((2 * epsilon) * ((i0p + 1) div 2)) + ((1 - epsilon) * (((i0p + 1) div 2) - 1)) by L580 ; :: thesis: verum

proof

hence
S
assume L710:
i0p is even
; :: thesis: Sum (a | i0p) = ((2 * epsilon) * (i0p div 2)) + ((1 - epsilon) * (i0p div 2))

thus Sum (a | i0p) = Sum ((a | i0) ^ <*(a . i0p)*>) by L411, FINSEQ_5:83

.= (Sum (a | i0)) + (a . i0p) by RVSUM_1:74

.= (((2 * epsilon) * ((i0 + 1) div 2)) + ((1 - epsilon) * (((i0 + 1) div 2) - 1))) + (1 - epsilon) by L050, L490, L412, L710

.= ((2 * epsilon) * (i0p div 2)) + ((1 - epsilon) * (i0p div 2)) ; :: thesis: verum

end;thus Sum (a | i0p) = Sum ((a | i0) ^ <*(a . i0p)*>) by L411, FINSEQ_5:83

.= (Sum (a | i0)) + (a . i0p) by RVSUM_1:74

.= (((2 * epsilon) * ((i0 + 1) div 2)) + ((1 - epsilon) * (((i0 + 1) div 2) - 1))) + (1 - epsilon) by L050, L490, L412, L710

.= ((2 * epsilon) * (i0p div 2)) + ((1 - epsilon) * (i0p div 2)) ; :: thesis: verum

S

Sum (a | n) = ((2 * epsilon) * ((n + 1) div 2)) + ((1 - epsilon) * (((n + 1) div 2) - 1)) by L020, L030, L010, L899

.= ((2 * ((1 / (n + 1)) * (n + 1))) / 2) + ((1 - (1 / (n + 1))) * (((n + 1) / 2) - 1)) by L060, L040

.= (2 / 2) + ((1 - (1 / (n + 1))) * (((n + 1) / 2) - 1)) by XCMPLX_1:87

.= (((n + 1) / 2) - (((1 / (n + 1)) * (n + 1)) / 2)) + (1 / (n + 1))

.= (((n + 1) / 2) - (1 / 2)) + (1 / (n + 1)) by XCMPLX_1:87

.= (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) ;

hence Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) by L030, FINSEQ_1:58; :: thesis: verum