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₁[ 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] ;
L400: for i being Element of NAT st 1 <= i & i < len a & S₁[i] holds
S₁[i + 1]

proof

let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < len a & S₁[i0] implies S₁[i0 + 1] )
assume that
1 <= i0 and
L411: i0 < len a and
L412: S₁[i0] ; :: thesis: S₁[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)) )

proof

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;

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

proof

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;

hence S₁[i0 + 1] by L500; :: thesis: verum

end;

L899: for i being Element of NAT st 1 <= i & i <= len a holds
S₁[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