let A be non empty closed_interval Subset of REAL; :: thesis: for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds

( delta T is 0 -convergent & delta T is non-zero )

let T be sequence of (divs A); :: thesis: ( vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) implies ( delta T is 0 -convergent & delta T is non-zero ) )

assume that

A1: vol A > 0 and

A2: for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ; :: thesis: ( delta T is 0 -convergent & delta T is non-zero )

A3: for n being Nat holds (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))_{1}( Nat) -> object = (2 ") to_power ($1 + 1);

consider seq being Real_Sequence such that

A8: for n being Nat holds seq . n = H_{1}(n)
from SEQ_1:sch 1();

A9: ( seq is convergent & lim seq = 0 ) by A8, SERIES_1:1;

for n being Nat holds (delta T) . n = (2 * (vol A)) * (seq . n)

then A11: delta T is convergent by A8, SERIES_1:1, SEQ_2:7;

A12: lim (delta T) = (2 * (vol A)) * 0 by A9, A10, SEQ_2:8

.= 0 ;

( delta T is 0 -convergent & delta T is non-zero )

let T be sequence of (divs A); :: thesis: ( vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) implies ( delta T is 0 -convergent & delta T is non-zero ) )

assume that

A1: vol A > 0 and

A2: for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ; :: thesis: ( delta T is 0 -convergent & delta T is non-zero )

A3: for n being Nat holds (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))

proof

deffunc H
let n be Nat; :: thesis: (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))

n is Element of NAT by ORDINAL1:def 12;

then (delta T) . n = delta (T . n) by INTEGRA3:def 2;

then (delta T) . n = delta (EqDiv (A,(2 |^ n))) by A2;

then A4: (delta T) . n = max (rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n)))))) by INTEGRA3:def 1;

A5: for k being Nat st k in dom (EqDiv (A,(2 |^ n))) holds

(upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))

then rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = {((2 * (vol A)) * ((2 ") |^ (n + 1)))} by ZFMISC_1:33;

hence (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1)) by A4, XXREAL_2:11; :: thesis: verum

end;n is Element of NAT by ORDINAL1:def 12;

then (delta T) . n = delta (T . n) by INTEGRA3:def 2;

then (delta T) . n = delta (EqDiv (A,(2 |^ n))) by A2;

then A4: (delta T) . n = max (rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n)))))) by INTEGRA3:def 1;

A5: for k being Nat st k in dom (EqDiv (A,(2 |^ n))) holds

(upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))

proof

let k be Nat; :: thesis: ( k in dom (EqDiv (A,(2 |^ n))) implies (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1)) )

assume A6: k in dom (EqDiv (A,(2 |^ n))) ; :: thesis: (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))

2 |^ n > 0 by NEWTON:83;

then EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n by A1, Def1;

then vol (divset ((EqDiv (A,(2 |^ n))),k)) = (vol A) / (2 |^ n) by A6, Th15;

then (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (vol A) / (2 |^ n) by A6, INTEGRA1:20

.= ((vol A) / ((2 |^ n) * 2)) * 2 by XCMPLX_1:92

.= ((vol A) / (2 |^ (n + 1))) * 2 by NEWTON:6

.= ((vol A) * ((2 |^ (n + 1)) ")) * 2 by XCMPLX_0:def 9

.= (2 * (vol A)) * ((2 |^ (n + 1)) ") ;

hence (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1)) by Th16; :: thesis: verum

end;assume A6: k in dom (EqDiv (A,(2 |^ n))) ; :: thesis: (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))

2 |^ n > 0 by NEWTON:83;

then EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n by A1, Def1;

then vol (divset ((EqDiv (A,(2 |^ n))),k)) = (vol A) / (2 |^ n) by A6, Th15;

then (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (vol A) / (2 |^ n) by A6, INTEGRA1:20

.= ((vol A) / ((2 |^ n) * 2)) * 2 by XCMPLX_1:92

.= ((vol A) / (2 |^ (n + 1))) * 2 by NEWTON:6

.= ((vol A) * ((2 |^ (n + 1)) ")) * 2 by XCMPLX_0:def 9

.= (2 * (vol A)) * ((2 |^ (n + 1)) ") ;

hence (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1)) by Th16; :: thesis: verum

now :: thesis: for q being object st q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) holds

q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}

then
rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) c= {((2 * (vol A)) * ((2 ") |^ (n + 1)))}
;q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}

let q be object ; :: thesis: ( q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) implies q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))} )

assume q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) ; :: thesis: q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}

then consider p being Element of NAT such that

A7: ( p in dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) & q = (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . p ) by PARTFUN1:3;

len (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = len (EqDiv (A,(2 |^ n))) by INTEGRA1:def 6;

then dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = dom (EqDiv (A,(2 |^ n))) by FINSEQ_3:29;

then q = (2 * (vol A)) * ((2 ") |^ (n + 1)) by A5, A7;

hence q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))} by TARSKI:def 1; :: thesis: verum

end;assume q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) ; :: thesis: q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}

then consider p being Element of NAT such that

A7: ( p in dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) & q = (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . p ) by PARTFUN1:3;

len (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = len (EqDiv (A,(2 |^ n))) by INTEGRA1:def 6;

then dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = dom (EqDiv (A,(2 |^ n))) by FINSEQ_3:29;

then q = (2 * (vol A)) * ((2 ") |^ (n + 1)) by A5, A7;

hence q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))} by TARSKI:def 1; :: thesis: verum

then rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = {((2 * (vol A)) * ((2 ") |^ (n + 1)))} by ZFMISC_1:33;

hence (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1)) by A4, XXREAL_2:11; :: thesis: verum

consider seq being Real_Sequence such that

A8: for n being Nat holds seq . n = H

A9: ( seq is convergent & lim seq = 0 ) by A8, SERIES_1:1;

for n being Nat holds (delta T) . n = (2 * (vol A)) * (seq . n)

proof

then A10:
delta T = (2 * (vol A)) (#) seq
by SEQ_1:9;
let n be Nat; :: thesis: (delta T) . n = (2 * (vol A)) * (seq . n)

seq . n = (2 ") to_power (n + 1) by A8

.= (2 ") |^ (n + 1) by POWER:41 ;

hence (delta T) . n = (2 * (vol A)) * (seq . n) by A3; :: thesis: verum

end;seq . n = (2 ") to_power (n + 1) by A8

.= (2 ") |^ (n + 1) by POWER:41 ;

hence (delta T) . n = (2 * (vol A)) * (seq . n) by A3; :: thesis: verum

then A11: delta T is convergent by A8, SERIES_1:1, SEQ_2:7;

A12: lim (delta T) = (2 * (vol A)) * 0 by A9, A10, SEQ_2:8

.= 0 ;

now :: thesis: not 0 in rng (delta T)

hence
( delta T is 0 -convergent & delta T is non-zero )
by A11, A12, FDIFF_1:def 1, ORDINAL1:def 15; :: thesis: verumassume
0 in rng (delta T)
; :: thesis: contradiction

then consider m being Element of NAT such that

A13: ( m in dom (delta T) & 0 = (delta T) . m ) by PARTFUN1:3;

A14: (2 * (vol A)) * ((2 ") |^ (m + 1)) = 0 by A3, A13;

( 2 * (vol A) <> 0 & (2 ") |^ (m + 1) <> 0 ) by A1, NEWTON:83;

hence contradiction by A14, XCMPLX_1:6; :: thesis: verum

end;then consider m being Element of NAT such that

A13: ( m in dom (delta T) & 0 = (delta T) . m ) by PARTFUN1:3;

A14: (2 * (vol A)) * ((2 ") |^ (m + 1)) = 0 by A3, A13;

( 2 * (vol A) <> 0 & (2 ") |^ (m + 1) <> 0 ) by A1, NEWTON:83;

hence contradiction by A14, XCMPLX_1:6; :: thesis: verum