Theorem mblfinlem2

Description: Lemma for ismblfin , effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different definition of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018) (Revised by Brendan Leahy, 13-Jul-2018)

	Ref	Expression
Assertion	mblfinlem2	|- ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )

Proof

Step	Hyp	Ref	Expression
1		retop	|- ( topGen ` ran (,) ) e. Top
2		0cld	|- ( ( topGen ` ran (,) ) e. Top -> (/) e. ( Clsd ` ( topGen ` ran (,) ) ) )
3	1 2	ax-mp	|- (/) e. ( Clsd ` ( topGen ` ran (,) ) )
4		simpl3	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A = (/) ) -> M < ( vol* ` A ) )
5		fveq2	|- ( A = (/) -> ( vol* ` A ) = ( vol* ` (/) ) )
6	5	adantl	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A = (/) ) -> ( vol* ` A ) = ( vol* ` (/) ) )
7	4 6	breqtrd	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A = (/) ) -> M < ( vol* ` (/) ) )
8		0ss	|- (/) C_ A
9	7 8	jctil	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A = (/) ) -> ( (/) C_ A /\ M < ( vol* ` (/) ) ) )
10		sseq1	|- ( s = (/) -> ( s C_ A <-> (/) C_ A ) )
11		fveq2	|- ( s = (/) -> ( vol* ` s ) = ( vol* ` (/) ) )
12	11	breq2d	|- ( s = (/) -> ( M < ( vol* ` s ) <-> M < ( vol* ` (/) ) ) )
13	10 12	anbi12d	|- ( s = (/) -> ( ( s C_ A /\ M < ( vol* ` s ) ) <-> ( (/) C_ A /\ M < ( vol* ` (/) ) ) ) )
14	13	rspcev	|- ( ( (/) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( (/) C_ A /\ M < ( vol* ` (/) ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
15	3 9 14	sylancr	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A = (/) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
16		mblfinlem1	|- ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> E. f f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
17	16	3ad2antl1	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A =/= (/) ) -> E. f f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
18		simpl3	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> M < ( vol* ` A ) )
19		f1ofo	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> f : NN -onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
20		rnco2	|- ran ( [,] o. f ) = ( [,] " ran f )
21		forn	|- ( f : NN -onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ran f = { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
22	21	imaeq2d	|- ( f : NN -onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( [,] " ran f ) = ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
23	20 22	syl5eq	|- ( f : NN -onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ran ( [,] o. f ) = ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
24	23	unieqd	|- ( f : NN -onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> U. ran ( [,] o. f ) = U. ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
25	19 24	syl	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> U. ran ( [,] o. f ) = U. ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
26	25	adantl	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> U. ran ( [,] o. f ) = U. ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
27		oveq1	|- ( x = u -> ( x / ( 2 ^ y ) ) = ( u / ( 2 ^ y ) ) )
28		oveq1	|- ( x = u -> ( x + 1 ) = ( u + 1 ) )
29	28	oveq1d	|- ( x = u -> ( ( x + 1 ) / ( 2 ^ y ) ) = ( ( u + 1 ) / ( 2 ^ y ) ) )
30	27 29	opeq12d	|- ( x = u -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. = <. ( u / ( 2 ^ y ) ) , ( ( u + 1 ) / ( 2 ^ y ) ) >. )
31		oveq2	|- ( y = v -> ( 2 ^ y ) = ( 2 ^ v ) )
32	31	oveq2d	|- ( y = v -> ( u / ( 2 ^ y ) ) = ( u / ( 2 ^ v ) ) )
33	31	oveq2d	|- ( y = v -> ( ( u + 1 ) / ( 2 ^ y ) ) = ( ( u + 1 ) / ( 2 ^ v ) ) )
34	32 33	opeq12d	|- ( y = v -> <. ( u / ( 2 ^ y ) ) , ( ( u + 1 ) / ( 2 ^ y ) ) >. = <. ( u / ( 2 ^ v ) ) , ( ( u + 1 ) / ( 2 ^ v ) ) >. )
35	30 34	cbvmpov	|- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) = ( u e. ZZ , v e. NN0 |-> <. ( u / ( 2 ^ v ) ) , ( ( u + 1 ) / ( 2 ^ v ) ) >. )
36		fveq2	|- ( a = z -> ( [,] ` a ) = ( [,] ` z ) )
37	36	sseq1d	|- ( a = z -> ( ( [,] ` a ) C_ ( [,] ` c ) <-> ( [,] ` z ) C_ ( [,] ` c ) ) )
38		eqeq1	|- ( a = z -> ( a = c <-> z = c ) )
39	37 38	imbi12d	|- ( a = z -> ( ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) ) )
40	39	ralbidv	|- ( a = z -> ( A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) ) )
41	40	cbvrabv	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } = { z e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) }
42		ssrab2	|- { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
43	42	a1i	|- ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) -> { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
44	35 41 43	dyadmbllem	|- ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = U. ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
45	44	adantr	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = U. ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
46	26 45	eqtr4d	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> U. ran ( [,] o. f ) = U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) )
47		opnmbllem0	|- ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = A )
48	47	3ad2ant1	|- ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = A )
49	48	adantr	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = A )
50	46 49	eqtrd	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> U. ran ( [,] o. f ) = A )
51	50	fveq2d	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( vol* ` U. ran ( [,] o. f ) ) = ( vol* ` A ) )
52		f1of	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
53		ssrab2	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A }
54	35	dyadf	|- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
55		frn	|- ( ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( <_ i^i ( RR X. RR ) ) )
56	54 55	ax-mp	|- ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( <_ i^i ( RR X. RR ) )
57	42 56	sstri	|- { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ( <_ i^i ( RR X. RR ) )
58	53 57	sstri	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ( <_ i^i ( RR X. RR ) )
59		fss	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ( <_ i^i ( RR X. RR ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
60	52 58 59	sylancl	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
61	53 42	sstri	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
62		ffvelrn	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
63	61 62	sseldi	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( f ` m ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
64	63	adantrr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( f ` m ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
65		ffvelrn	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
66	61 65	sseldi	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( f ` z ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
67	66	adantrl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( f ` z ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
68	35	dyaddisj	|- ( ( ( f ` m ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) /\ ( f ` z ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) ) -> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
69	64 67 68	syl2anc	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
70	52 69	sylan	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
71		df-3or	|- ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
72	70 71	sylib	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
73		elrabi	|- ( ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( f ` z ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } )
74		fveq2	|- ( a = ( f ` m ) -> ( [,] ` a ) = ( [,] ` ( f ` m ) ) )
75	74	sseq1d	|- ( a = ( f ` m ) -> ( ( [,] ` a ) C_ ( [,] ` c ) <-> ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) ) )
76		eqeq1	|- ( a = ( f ` m ) -> ( a = c <-> ( f ` m ) = c ) )
77	75 76	imbi12d	|- ( a = ( f ` m ) -> ( ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) -> ( f ` m ) = c ) ) )
78	77	ralbidv	|- ( a = ( f ` m ) -> ( A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) -> ( f ` m ) = c ) ) )
79	78	elrab	|- ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } <-> ( ( f ` m ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } /\ A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) -> ( f ` m ) = c ) ) )
80	79	simprbi	|- ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) -> ( f ` m ) = c ) )
81		fveq2	|- ( c = ( f ` z ) -> ( [,] ` c ) = ( [,] ` ( f ` z ) ) )
82	81	sseq2d	|- ( c = ( f ` z ) -> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) <-> ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) ) )
83		eqeq2	|- ( c = ( f ` z ) -> ( ( f ` m ) = c <-> ( f ` m ) = ( f ` z ) ) )
84	82 83	imbi12d	|- ( c = ( f ` z ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) -> ( f ` m ) = c ) <-> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) -> ( f ` m ) = ( f ` z ) ) ) )
85	84	rspcva	|- ( ( ( f ` z ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } /\ A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` m ) ) C_ ( [,] ` c ) -> ( f ` m ) = c ) ) -> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) -> ( f ` m ) = ( f ` z ) ) )
86	73 80 85	syl2anr	|- ( ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) -> ( f ` m ) = ( f ` z ) ) )
87		elrabi	|- ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( f ` m ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } )
88		fveq2	|- ( a = ( f ` z ) -> ( [,] ` a ) = ( [,] ` ( f ` z ) ) )
89	88	sseq1d	|- ( a = ( f ` z ) -> ( ( [,] ` a ) C_ ( [,] ` c ) <-> ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) ) )
90		eqeq1	|- ( a = ( f ` z ) -> ( a = c <-> ( f ` z ) = c ) )
91	89 90	imbi12d	|- ( a = ( f ` z ) -> ( ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) -> ( f ` z ) = c ) ) )
92	91	ralbidv	|- ( a = ( f ` z ) -> ( A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) -> ( f ` z ) = c ) ) )
93	92	elrab	|- ( ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } <-> ( ( f ` z ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } /\ A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) -> ( f ` z ) = c ) ) )
94	93	simprbi	|- ( ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) -> ( f ` z ) = c ) )
95		fveq2	|- ( c = ( f ` m ) -> ( [,] ` c ) = ( [,] ` ( f ` m ) ) )
96	95	sseq2d	|- ( c = ( f ` m ) -> ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) <-> ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) )
97		eqeq2	|- ( c = ( f ` m ) -> ( ( f ` z ) = c <-> ( f ` z ) = ( f ` m ) ) )
98	96 97	imbi12d	|- ( c = ( f ` m ) -> ( ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) -> ( f ` z ) = c ) <-> ( ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) -> ( f ` z ) = ( f ` m ) ) ) )
99	98	rspcva	|- ( ( ( f ` m ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } /\ A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` ( f ` z ) ) C_ ( [,] ` c ) -> ( f ` z ) = c ) ) -> ( ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) -> ( f ` z ) = ( f ` m ) ) )
100	87 94 99	syl2an	|- ( ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) -> ( f ` z ) = ( f ` m ) ) )
101		eqcom	|- ( ( f ` z ) = ( f ` m ) <-> ( f ` m ) = ( f ` z ) )
102	100 101	syl6ib	|- ( ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) -> ( f ` m ) = ( f ` z ) ) )
103	86 102	jaod	|- ( ( ( f ` m ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( f ` z ) e. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) -> ( f ` m ) = ( f ` z ) ) )
104	62 65 103	syl2an	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) /\ ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) -> ( f ` m ) = ( f ` z ) ) )
105	104	anandis	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) -> ( f ` m ) = ( f ` z ) ) )
106	52 105	sylan	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) -> ( f ` m ) = ( f ` z ) ) )
107		f1of1	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> f : NN -1-1-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
108		f1veqaeq	|- ( ( f : NN -1-1-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( f ` m ) = ( f ` z ) -> m = z ) )
109	107 108	sylan	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( f ` m ) = ( f ` z ) -> m = z ) )
110	106 109	syld	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) -> m = z ) )
111	110	orim1d	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( ( ( ( [,] ` ( f ` m ) ) C_ ( [,] ` ( f ` z ) ) \/ ( [,] ` ( f ` z ) ) C_ ( [,] ` ( f ` m ) ) ) \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) -> ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) ) )
112	72 111	mpd	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
113	112	ralrimivva	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. m e. NN A. z e. NN ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
114		eqeq1	|- ( m = z -> ( m = p <-> z = p ) )
115		2fveq3	|- ( m = z -> ( (,) ` ( f ` m ) ) = ( (,) ` ( f ` z ) ) )
116	115	ineq1d	|- ( m = z -> ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = ( ( (,) ` ( f ` z ) ) i^i ( (,) ` ( f ` p ) ) ) )
117	116	eqeq1d	|- ( m = z -> ( ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) <-> ( ( (,) ` ( f ` z ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) )
118	114 117	orbi12d	|- ( m = z -> ( ( m = p \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) <-> ( z = p \/ ( ( (,) ` ( f ` z ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) ) )
119	118	ralbidv	|- ( m = z -> ( A. p e. NN ( m = p \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) <-> A. p e. NN ( z = p \/ ( ( (,) ` ( f ` z ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) ) )
120	119	cbvralvw	|- ( A. m e. NN A. p e. NN ( m = p \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) <-> A. z e. NN A. p e. NN ( z = p \/ ( ( (,) ` ( f ` z ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) )
121		eqeq2	|- ( z = p -> ( m = z <-> m = p ) )
122		2fveq3	|- ( z = p -> ( (,) ` ( f ` z ) ) = ( (,) ` ( f ` p ) ) )
123	122	ineq2d	|- ( z = p -> ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) )
124	123	eqeq1d	|- ( z = p -> ( ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) <-> ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) )
125	121 124	orbi12d	|- ( z = p -> ( ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> ( m = p \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) ) )
126	125	cbvralvw	|- ( A. z e. NN ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> A. p e. NN ( m = p \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) )
127	126	ralbii	|- ( A. m e. NN A. z e. NN ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> A. m e. NN A. p e. NN ( m = p \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) )
128	122	disjor	|- ( Disj_ z e. NN ( (,) ` ( f ` z ) ) <-> A. z e. NN A. p e. NN ( z = p \/ ( ( (,) ` ( f ` z ) ) i^i ( (,) ` ( f ` p ) ) ) = (/) ) )
129	120 127 128	3bitr4ri	|- ( Disj_ z e. NN ( (,) ` ( f ` z ) ) <-> A. m e. NN A. z e. NN ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
130	113 129	sylibr	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> Disj_ z e. NN ( (,) ` ( f ` z ) ) )
131		eqid	|- seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
132	60 130 131	uniiccvol	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( vol* ` U. ran ( [,] o. f ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
133	132	adantl	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( vol* ` U. ran ( [,] o. f ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
134	51 133	eqtr3d	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( vol* ` A ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
135	18 134	breqtrd	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> M < sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
136		absf	|- abs : CC --> RR
137		subf	|- - : ( CC X. CC ) --> CC
138		fco	|- ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
139	136 137 138	mp2an	|- ( abs o. - ) : ( CC X. CC ) --> RR
140		zre	|- ( x e. ZZ -> x e. RR )
141		2re	|- 2 e. RR
142		reexpcl	|- ( ( 2 e. RR /\ y e. NN0 ) -> ( 2 ^ y ) e. RR )
143	141 142	mpan	|- ( y e. NN0 -> ( 2 ^ y ) e. RR )
144		2cn	|- 2 e. CC
145		2ne0	|- 2 =/= 0
146		nn0z	|- ( y e. NN0 -> y e. ZZ )
147		expne0i	|- ( ( 2 e. CC /\ 2 =/= 0 /\ y e. ZZ ) -> ( 2 ^ y ) =/= 0 )
148	144 145 146 147	mp3an12i	|- ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
149	143 148	jca	|- ( y e. NN0 -> ( ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) )
150		redivcl	|- ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( x / ( 2 ^ y ) ) e. RR )
151		peano2re	|- ( x e. RR -> ( x + 1 ) e. RR )
152		redivcl	|- ( ( ( x + 1 ) e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
153	151 152	syl3an1	|- ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
154	150 153	opelxpd	|- ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
155	154	3expb	|- ( ( x e. RR /\ ( ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
156	140 149 155	syl2an	|- ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
157	156	rgen2	|- A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR )
158		eqid	|- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
159	158	fmpo	|- ( A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) <-> ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( RR X. RR ) )
160	157 159	mpbi	|- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( RR X. RR )
161		frn	|- ( ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( RR X. RR ) -> ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( RR X. RR ) )
162	160 161	ax-mp	|- ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( RR X. RR )
163	42 162	sstri	|- { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ( RR X. RR )
164	53 163	sstri	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ( RR X. RR )
165		ax-resscn	|- RR C_ CC
166		xpss12	|- ( ( RR C_ CC /\ RR C_ CC ) -> ( RR X. RR ) C_ ( CC X. CC ) )
167	165 165 166	mp2an	|- ( RR X. RR ) C_ ( CC X. CC )
168	164 167	sstri	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ( CC X. CC )
169		fss	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ( CC X. CC ) ) -> f : NN --> ( CC X. CC ) )
170	168 169	mpan2	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> f : NN --> ( CC X. CC ) )
171		fco	|- ( ( ( abs o. - ) : ( CC X. CC ) --> RR /\ f : NN --> ( CC X. CC ) ) -> ( ( abs o. - ) o. f ) : NN --> RR )
172	139 170 171	sylancr	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( ( abs o. - ) o. f ) : NN --> RR )
173		nnuz	|- NN = ( ZZ>= ` 1 )
174		1z	|- 1 e. ZZ
175	174	a1i	|- ( ( ( abs o. - ) o. f ) : NN --> RR -> 1 e. ZZ )
176		ffvelrn	|- ( ( ( ( abs o. - ) o. f ) : NN --> RR /\ n e. NN ) -> ( ( ( abs o. - ) o. f ) ` n ) e. RR )
177	173 175 176	serfre	|- ( ( ( abs o. - ) o. f ) : NN --> RR -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> RR )
178		frn	|- ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> RR -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR )
179		ressxr	|- RR C_ RR*
180	178 179	sstrdi	|- ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> RR -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
181	52 172 177 180	4syl	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
182		rexr	|- ( M e. RR -> M e. RR* )
183	182	3ad2ant2	|- ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) -> M e. RR* )
184		supxrlub	|- ( ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* /\ M e. RR* ) -> ( M < sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <-> E. z e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) M < z ) )
185	181 183 184	syl2anr	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( M < sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <-> E. z e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) M < z ) )
186	135 185	mpbid	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> E. z e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) M < z )
187		seqfn	|- ( 1 e. ZZ -> seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn ( ZZ>= ` 1 ) )
188	174 187	ax-mp	|- seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn ( ZZ>= ` 1 )
189	173	fneq2i	|- ( seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn NN <-> seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn ( ZZ>= ` 1 ) )
190	188 189	mpbir	|- seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn NN
191		breq2	|- ( z = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) -> ( M < z <-> M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) ) )
192	191	rexrn	|- ( seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn NN -> ( E. z e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) M < z <-> E. n e. NN M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) ) )
193	190 192	ax-mp	|- ( E. z e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) M < z <-> E. n e. NN M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
194	186 193	sylib	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> E. n e. NN M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
195	60	ffvelrnda	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( f ` z ) e. ( <_ i^i ( RR X. RR ) ) )
196		0le0	|- 0 <_ 0
197		df-br	|- ( 0 <_ 0 <-> <. 0 , 0 >. e. <_ )
198	196 197	mpbi	|- <. 0 , 0 >. e. <_
199		0re	|- 0 e. RR
200		opelxpi	|- ( ( 0 e. RR /\ 0 e. RR ) -> <. 0 , 0 >. e. ( RR X. RR ) )
201	199 199 200	mp2an	|- <. 0 , 0 >. e. ( RR X. RR )
202		elin	|- ( <. 0 , 0 >. e. ( <_ i^i ( RR X. RR ) ) <-> ( <. 0 , 0 >. e. <_ /\ <. 0 , 0 >. e. ( RR X. RR ) ) )
203	198 201 202	mpbir2an	|- <. 0 , 0 >. e. ( <_ i^i ( RR X. RR ) )
204		ifcl	|- ( ( ( f ` z ) e. ( <_ i^i ( RR X. RR ) ) /\ <. 0 , 0 >. e. ( <_ i^i ( RR X. RR ) ) ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. ( <_ i^i ( RR X. RR ) ) )
205	195 203 204	sylancl	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. ( <_ i^i ( RR X. RR ) ) )
206	205	fmpttd	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
207		df-ov	|- ( 0 (,) 0 ) = ( (,) ` <. 0 , 0 >. )
208		iooid	|- ( 0 (,) 0 ) = (/)
209	207 208	eqtr3i	|- ( (,) ` <. 0 , 0 >. ) = (/)
210	209	ineq1i	|- ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = ( (/) i^i ( (,) ` ( f ` z ) ) )
211		0in	|- ( (/) i^i ( (,) ` ( f ` z ) ) ) = (/)
212	210 211	eqtri	|- ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = (/)
213	212	olci	|- ( m = z \/ ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = (/) )
214		ineq1	|- ( ( (,) ` ( f ` m ) ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) )
215	214	eqeq1d	|- ( ( (,) ` ( f ` m ) ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) <-> ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
216	215	orbi2d	|- ( ( (,) ` ( f ` m ) ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) ) )
217		ineq1	|- ( ( (,) ` <. 0 , 0 >. ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) )
218	217	eqeq1d	|- ( ( (,) ` <. 0 , 0 >. ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = (/) <-> ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
219	218	orbi2d	|- ( ( (,) ` <. 0 , 0 >. ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( m = z \/ ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) ) )
220	216 219	ifboth	|- ( ( ( m = z \/ ( ( (,) ` ( f ` m ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) /\ ( m = z \/ ( ( (,) ` <. 0 , 0 >. ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) ) -> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
221	112 213 220	sylancl	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) )
222	209	ineq2i	|- ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i (/) )
223		in0	|- ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i (/) ) = (/)
224	222 223	eqtri	|- ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = (/)
225	224	olci	|- ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = (/) )
226		ineq2	|- ( ( (,) ` ( f ` z ) ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) )
227	226	eqeq1d	|- ( ( (,) ` ( f ` z ) ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) <-> ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
228	227	orbi2d	|- ( ( (,) ` ( f ` z ) ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) <-> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) ) )
229		ineq2	|- ( ( (,) ` <. 0 , 0 >. ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) )
230	229	eqeq1d	|- ( ( (,) ` <. 0 , 0 >. ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = (/) <-> ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
231	230	orbi2d	|- ( ( (,) ` <. 0 , 0 >. ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = (/) ) <-> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) ) )
232	228 231	ifboth	|- ( ( ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` ( f ` z ) ) ) = (/) ) /\ ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i ( (,) ` <. 0 , 0 >. ) ) = (/) ) ) -> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
233	221 225 232	sylancl	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( m e. NN /\ z e. NN ) ) -> ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
234	233	ralrimivva	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. m e. NN A. z e. NN ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
235		disjeq2	|- ( A. m e. NN ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) -> ( Disj_ m e. NN ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) <-> Disj_ m e. NN if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) ) )
236		eleq1w	|- ( z = m -> ( z e. ( 1 ... n ) <-> m e. ( 1 ... n ) ) )
237		fveq2	|- ( z = m -> ( f ` z ) = ( f ` m ) )
238	236 237	ifbieq1d	|- ( z = m -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) = if ( m e. ( 1 ... n ) , ( f ` m ) , <. 0 , 0 >. ) )
239		eqid	|- ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) )
240		fvex	|- ( f ` m ) e. _V
241		opex	|- <. 0 , 0 >. e. _V
242	240 241	ifex	|- if ( m e. ( 1 ... n ) , ( f ` m ) , <. 0 , 0 >. ) e. _V
243	238 239 242	fvmpt	|- ( m e. NN -> ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) = if ( m e. ( 1 ... n ) , ( f ` m ) , <. 0 , 0 >. ) )
244	243	fveq2d	|- ( m e. NN -> ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) = ( (,) ` if ( m e. ( 1 ... n ) , ( f ` m ) , <. 0 , 0 >. ) ) )
245		fvif	|- ( (,) ` if ( m e. ( 1 ... n ) , ( f ` m ) , <. 0 , 0 >. ) ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) )
246	244 245	eqtrdi	|- ( m e. NN -> ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) = if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) )
247	235 246	mprg	|- ( Disj_ m e. NN ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) <-> Disj_ m e. NN if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) )
248		eleq1w	|- ( m = z -> ( m e. ( 1 ... n ) <-> z e. ( 1 ... n ) ) )
249	248 115	ifbieq1d	|- ( m = z -> if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) = if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) )
250	249	disjor	|- ( Disj_ m e. NN if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) <-> A. m e. NN A. z e. NN ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
251	247 250	bitri	|- ( Disj_ m e. NN ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) <-> A. m e. NN A. z e. NN ( m = z \/ ( if ( m e. ( 1 ... n ) , ( (,) ` ( f ` m ) ) , ( (,) ` <. 0 , 0 >. ) ) i^i if ( z e. ( 1 ... n ) , ( (,) ` ( f ` z ) ) , ( (,) ` <. 0 , 0 >. ) ) ) = (/) ) )
252	234 251	sylibr	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> Disj_ m e. NN ( (,) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
253		eqid	|- seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) )
254	206 252 253	uniiccvol	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( vol* ` U. ran ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) , RR* , < ) )
255	254	adantr	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( vol* ` U. ran ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) , RR* , < ) )
256		rexpssxrxp	|- ( RR X. RR ) C_ ( RR* X. RR* )
257	164 256	sstri	|- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } C_ ( RR* X. RR* )
258	257 65	sseldi	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( f ` z ) e. ( RR* X. RR* ) )
259		0xr	|- 0 e. RR*
260		opelxpi	|- ( ( 0 e. RR* /\ 0 e. RR* ) -> <. 0 , 0 >. e. ( RR* X. RR* ) )
261	259 259 260	mp2an	|- <. 0 , 0 >. e. ( RR* X. RR* )
262		ifcl	|- ( ( ( f ` z ) e. ( RR* X. RR* ) /\ <. 0 , 0 >. e. ( RR* X. RR* ) ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. ( RR* X. RR* ) )
263	258 261 262	sylancl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. ( RR* X. RR* ) )
264		eqidd	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) )
265		iccf	|- [,] : ( RR* X. RR* ) --> ~P RR*
266	265	a1i	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> [,] : ( RR* X. RR* ) --> ~P RR* )
267	266	feqmptd	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> [,] = ( m e. ( RR* X. RR* ) |-> ( [,] ` m ) ) )
268		fveq2	|- ( m = if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) -> ( [,] ` m ) = ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) )
269	263 264 267 268	fmptco	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) )
270	52 269	syl	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) )
271	270	rneqd	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ran ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = ran ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) )
272	271	unieqd	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> U. ran ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = U. ran ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) )
273		peano2nn	|- ( n e. NN -> ( n + 1 ) e. NN )
274	273 173	eleqtrdi	|- ( n e. NN -> ( n + 1 ) e. ( ZZ>= ` 1 ) )
275		fzouzsplit	|- ( ( n + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ..^ ( n + 1 ) ) u. ( ZZ>= ` ( n + 1 ) ) ) )
276	274 275	syl	|- ( n e. NN -> ( ZZ>= ` 1 ) = ( ( 1 ..^ ( n + 1 ) ) u. ( ZZ>= ` ( n + 1 ) ) ) )
277	173 276	syl5eq	|- ( n e. NN -> NN = ( ( 1 ..^ ( n + 1 ) ) u. ( ZZ>= ` ( n + 1 ) ) ) )
278		nnz	|- ( n e. NN -> n e. ZZ )
279		fzval3	|- ( n e. ZZ -> ( 1 ... n ) = ( 1 ..^ ( n + 1 ) ) )
280	278 279	syl	|- ( n e. NN -> ( 1 ... n ) = ( 1 ..^ ( n + 1 ) ) )
281	280	uneq1d	|- ( n e. NN -> ( ( 1 ... n ) u. ( ZZ>= ` ( n + 1 ) ) ) = ( ( 1 ..^ ( n + 1 ) ) u. ( ZZ>= ` ( n + 1 ) ) ) )
282	277 281	eqtr4d	|- ( n e. NN -> NN = ( ( 1 ... n ) u. ( ZZ>= ` ( n + 1 ) ) ) )
283		fvif	|- ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) )
284	283	a1i	|- ( n e. NN -> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) )
285	282 284	iuneq12d	|- ( n e. NN -> U_ z e. NN ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = U_ z e. ( ( 1 ... n ) u. ( ZZ>= ` ( n + 1 ) ) ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) )
286		fvex	|- ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) e. _V
287	286	dfiun3	|- U_ z e. NN ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = U. ran ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) )
288		iunxun	|- U_ z e. ( ( 1 ... n ) u. ( ZZ>= ` ( n + 1 ) ) ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) = ( U_ z e. ( 1 ... n ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) )
289	285 287 288	3eqtr3g	|- ( n e. NN -> U. ran ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = ( U_ z e. ( 1 ... n ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) ) )
290		iftrue	|- ( z e. ( 1 ... n ) -> if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) = ( [,] ` ( f ` z ) ) )
291	290	iuneq2i	|- U_ z e. ( 1 ... n ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) = U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) )
292	291	a1i	|- ( n e. NN -> U_ z e. ( 1 ... n ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) = U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) )
293		uznfz	|- ( z e. ( ZZ>= ` ( n + 1 ) ) -> -. z e. ( 1 ... ( ( n + 1 ) - 1 ) ) )
294	293	adantl	|- ( ( n e. NN /\ z e. ( ZZ>= ` ( n + 1 ) ) ) -> -. z e. ( 1 ... ( ( n + 1 ) - 1 ) ) )
295		nncn	|- ( n e. NN -> n e. CC )
296		ax-1cn	|- 1 e. CC
297		pncan	|- ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
298	295 296 297	sylancl	|- ( n e. NN -> ( ( n + 1 ) - 1 ) = n )
299	298	oveq2d	|- ( n e. NN -> ( 1 ... ( ( n + 1 ) - 1 ) ) = ( 1 ... n ) )
300	299	eleq2d	|- ( n e. NN -> ( z e. ( 1 ... ( ( n + 1 ) - 1 ) ) <-> z e. ( 1 ... n ) ) )
301	300	notbid	|- ( n e. NN -> ( -. z e. ( 1 ... ( ( n + 1 ) - 1 ) ) <-> -. z e. ( 1 ... n ) ) )
302	301	adantr	|- ( ( n e. NN /\ z e. ( ZZ>= ` ( n + 1 ) ) ) -> ( -. z e. ( 1 ... ( ( n + 1 ) - 1 ) ) <-> -. z e. ( 1 ... n ) ) )
303	294 302	mpbid	|- ( ( n e. NN /\ z e. ( ZZ>= ` ( n + 1 ) ) ) -> -. z e. ( 1 ... n ) )
304	303	iffalsed	|- ( ( n e. NN /\ z e. ( ZZ>= ` ( n + 1 ) ) ) -> if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) = ( [,] ` <. 0 , 0 >. ) )
305	304	iuneq2dv	|- ( n e. NN -> U_ z e. ( ZZ>= ` ( n + 1 ) ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) = U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) )
306	292 305	uneq12d	|- ( n e. NN -> ( U_ z e. ( 1 ... n ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) if ( z e. ( 1 ... n ) , ( [,] ` ( f ` z ) ) , ( [,] ` <. 0 , 0 >. ) ) ) = ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) )
307	289 306	eqtrd	|- ( n e. NN -> U. ran ( z e. NN |-> ( [,] ` if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) )
308	272 307	sylan9eq	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> U. ran ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) = ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) )
309	308	fveq2d	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( vol* ` U. ran ( [,] o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) = ( vol* ` ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) ) )
310		xrltso	|- < Or RR*
311	310	a1i	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> < Or RR* )
312		elnnuz	|- ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
313	312	biimpi	|- ( n e. NN -> n e. ( ZZ>= ` 1 ) )
314	313	adantl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
315		elfznn	|- ( u e. ( 1 ... n ) -> u e. NN )
316	172	ffvelrnda	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ u e. NN ) -> ( ( ( abs o. - ) o. f ) ` u ) e. RR )
317	315 316	sylan2	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ u e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` u ) e. RR )
318	317	adantlr	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ u e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` u ) e. RR )
319		readdcl	|- ( ( u e. RR /\ v e. RR ) -> ( u + v ) e. RR )
320	319	adantl	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ ( u e. RR /\ v e. RR ) ) -> ( u + v ) e. RR )
321	314 318 320	seqcl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. RR )
322	321	rexrd	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. RR* )
323		eqidd	|- ( m e. ( 1 ... n ) -> ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) )
324		iftrue	|- ( m e. ( 1 ... n ) -> if ( m e. ( 1 ... n ) , ( f ` m ) , <. 0 , 0 >. ) = ( f ` m ) )
325	238 324	sylan9eqr	|- ( ( m e. ( 1 ... n ) /\ z = m ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) = ( f ` m ) )
326		elfznn	|- ( m e. ( 1 ... n ) -> m e. NN )
327	240	a1i	|- ( m e. ( 1 ... n ) -> ( f ` m ) e. _V )
328	323 325 326 327	fvmptd	|- ( m e. ( 1 ... n ) -> ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) = ( f ` m ) )
329	328	adantl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. ( 1 ... n ) ) -> ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) = ( f ` m ) )
330	329	fveq2d	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. ( 1 ... n ) ) -> ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) = ( ( abs o. - ) ` ( f ` m ) ) )
331		fvex	|- ( f ` z ) e. _V
332	331 241	ifex	|- if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. _V
333	332 239	fnmpti	|- ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) Fn NN
334		fvco2	|- ( ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) Fn NN /\ m e. NN ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
335	333 326 334	sylancr	|- ( m e. ( 1 ... n ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
336	335	adantl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
337		ffn	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> f Fn NN )
338		fvco2	|- ( ( f Fn NN /\ m e. NN ) -> ( ( ( abs o. - ) o. f ) ` m ) = ( ( abs o. - ) ` ( f ` m ) ) )
339	337 326 338	syl2an	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` m ) = ( ( abs o. - ) ` ( f ` m ) ) )
340	330 336 339	3eqtr4d	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( ( abs o. - ) o. f ) ` m ) )
341	340	adantlr	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( ( abs o. - ) o. f ) ` m ) )
342	314 341	seqfveq	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
343	174	a1i	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> 1 e. ZZ )
344	168 65	sseldi	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( f ` z ) e. ( CC X. CC ) )
345		0cn	|- 0 e. CC
346		opelxpi	|- ( ( 0 e. CC /\ 0 e. CC ) -> <. 0 , 0 >. e. ( CC X. CC ) )
347	345 345 346	mp2an	|- <. 0 , 0 >. e. ( CC X. CC )
348		ifcl	|- ( ( ( f ` z ) e. ( CC X. CC ) /\ <. 0 , 0 >. e. ( CC X. CC ) ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. ( CC X. CC ) )
349	344 347 348	sylancl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) e. ( CC X. CC ) )
350	349	fmpttd	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) : NN --> ( CC X. CC ) )
351		fco	|- ( ( ( abs o. - ) : ( CC X. CC ) --> RR /\ ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) : NN --> ( CC X. CC ) ) -> ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) : NN --> RR )
352	139 350 351	sylancr	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) : NN --> RR )
353	352	ffvelrnda	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) e. RR )
354	173 343 353	serfre	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) : NN --> RR )
355	354	ffnd	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) Fn NN )
356		fnfvelrn	|- ( ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) Fn NN /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) )
357	355 356	sylan	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) )
358	342 357	eqeltrrd	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) )
359	354	frnd	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) C_ RR )
360	359	adantr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) C_ RR )
361	360	sselda	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ) -> m e. RR )
362	321	adantr	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. RR )
363		readdcl	|- ( ( m e. RR /\ u e. RR ) -> ( m + u ) e. RR )
364	363	adantl	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) /\ ( m e. RR /\ u e. RR ) ) -> ( m + u ) e. RR )
365		recn	|- ( m e. RR -> m e. CC )
366		recn	|- ( u e. RR -> u e. CC )
367		recn	|- ( v e. RR -> v e. CC )
368		addass	|- ( ( m e. CC /\ u e. CC /\ v e. CC ) -> ( ( m + u ) + v ) = ( m + ( u + v ) ) )
369	365 366 367 368	syl3an	|- ( ( m e. RR /\ u e. RR /\ v e. RR ) -> ( ( m + u ) + v ) = ( m + ( u + v ) ) )
370	369	adantl	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) /\ ( m e. RR /\ u e. RR /\ v e. RR ) ) -> ( ( m + u ) + v ) = ( m + ( u + v ) ) )
371		nnltp1le	|- ( ( n e. NN /\ t e. NN ) -> ( n < t <-> ( n + 1 ) <_ t ) )
372	371	biimpa	|- ( ( ( n e. NN /\ t e. NN ) /\ n < t ) -> ( n + 1 ) <_ t )
373	273	nnzd	|- ( n e. NN -> ( n + 1 ) e. ZZ )
374		nnz	|- ( t e. NN -> t e. ZZ )
375		eluz	|- ( ( ( n + 1 ) e. ZZ /\ t e. ZZ ) -> ( t e. ( ZZ>= ` ( n + 1 ) ) <-> ( n + 1 ) <_ t ) )
376	373 374 375	syl2an	|- ( ( n e. NN /\ t e. NN ) -> ( t e. ( ZZ>= ` ( n + 1 ) ) <-> ( n + 1 ) <_ t ) )
377	376	adantr	|- ( ( ( n e. NN /\ t e. NN ) /\ n < t ) -> ( t e. ( ZZ>= ` ( n + 1 ) ) <-> ( n + 1 ) <_ t ) )
378	372 377	mpbird	|- ( ( ( n e. NN /\ t e. NN ) /\ n < t ) -> t e. ( ZZ>= ` ( n + 1 ) ) )
379	378	adantlll	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> t e. ( ZZ>= ` ( n + 1 ) ) )
380	313	ad3antlr	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> n e. ( ZZ>= ` 1 ) )
381		simplll	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
382		elfznn	|- ( m e. ( 1 ... t ) -> m e. NN )
383	381 382 353	syl2an	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) /\ m e. ( 1 ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) e. RR )
384	364 370 379 380 383	seqsplit	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) = ( ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) + ( seq ( n + 1 ) ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) ) )
385	342	ad2antrr	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
386		elfzelz	|- ( m e. ( ( n + 1 ) ... t ) -> m e. ZZ )
387	386	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> m e. ZZ )
388		0red	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> 0 e. RR )
389	273	nnred	|- ( n e. NN -> ( n + 1 ) e. RR )
390	389	ad3antrrr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( n + 1 ) e. RR )
391	386	zred	|- ( m e. ( ( n + 1 ) ... t ) -> m e. RR )
392	391	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> m e. RR )
393	273	nngt0d	|- ( n e. NN -> 0 < ( n + 1 ) )
394	393	ad3antrrr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> 0 < ( n + 1 ) )
395		elfzle1	|- ( m e. ( ( n + 1 ) ... t ) -> ( n + 1 ) <_ m )
396	395	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( n + 1 ) <_ m )
397	388 390 392 394 396	ltletrd	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> 0 < m )
398		elnnz	|- ( m e. NN <-> ( m e. ZZ /\ 0 < m ) )
399	387 397 398	sylanbrc	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> m e. NN )
400	333 399 334	sylancr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
401		eqidd	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) )
402		nnre	|- ( n e. NN -> n e. RR )
403	402	adantr	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> n e. RR )
404	389	adantr	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> ( n + 1 ) e. RR )
405	391	adantl	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> m e. RR )
406	402	ltp1d	|- ( n e. NN -> n < ( n + 1 ) )
407	406	adantr	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> n < ( n + 1 ) )
408	395	adantl	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> ( n + 1 ) <_ m )
409	403 404 405 407 408	ltletrd	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> n < m )
410	409	adantr	|- ( ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) /\ z = m ) -> n < m )
411	403 405	ltnled	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> ( n < m <-> -. m <_ n ) )
412		breq1	|- ( m = z -> ( m <_ n <-> z <_ n ) )
413	412	equcoms	|- ( z = m -> ( m <_ n <-> z <_ n ) )
414	413	notbid	|- ( z = m -> ( -. m <_ n <-> -. z <_ n ) )
415	411 414	sylan9bb	|- ( ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) /\ z = m ) -> ( n < m <-> -. z <_ n ) )
416	410 415	mpbid	|- ( ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) /\ z = m ) -> -. z <_ n )
417		elfzle2	|- ( z e. ( 1 ... n ) -> z <_ n )
418	416 417	nsyl	|- ( ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) /\ z = m ) -> -. z e. ( 1 ... n ) )
419	418	iffalsed	|- ( ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) /\ z = m ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) = <. 0 , 0 >. )
420	386	adantl	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> m e. ZZ )
421		0red	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> 0 e. RR )
422	393	adantr	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> 0 < ( n + 1 ) )
423	421 404 405 422 408	ltletrd	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> 0 < m )
424	420 423 398	sylanbrc	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> m e. NN )
425	241	a1i	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> <. 0 , 0 >. e. _V )
426	401 419 424 425	fvmptd	|- ( ( n e. NN /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) = <. 0 , 0 >. )
427	426	ad4ant14	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) = <. 0 , 0 >. )
428	427	fveq2d	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) = ( ( abs o. - ) ` <. 0 , 0 >. ) )
429	400 428	eqtrd	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` <. 0 , 0 >. ) )
430		fvco3	|- ( ( - : ( CC X. CC ) --> CC /\ <. 0 , 0 >. e. ( CC X. CC ) ) -> ( ( abs o. - ) ` <. 0 , 0 >. ) = ( abs ` ( - ` <. 0 , 0 >. ) ) )
431	137 347 430	mp2an	|- ( ( abs o. - ) ` <. 0 , 0 >. ) = ( abs ` ( - ` <. 0 , 0 >. ) )
432		df-ov	|- ( 0 - 0 ) = ( - ` <. 0 , 0 >. )
433		0m0e0	|- ( 0 - 0 ) = 0
434	432 433	eqtr3i	|- ( - ` <. 0 , 0 >. ) = 0
435	434	fveq2i	|- ( abs ` ( - ` <. 0 , 0 >. ) ) = ( abs ` 0 )
436		abs0	|- ( abs ` 0 ) = 0
437	435 436	eqtri	|- ( abs ` ( - ` <. 0 , 0 >. ) ) = 0
438	431 437	eqtri	|- ( ( abs o. - ) ` <. 0 , 0 >. ) = 0
439	429 438	eqtrdi	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = 0 )
440		elfzuz	|- ( m e. ( ( n + 1 ) ... t ) -> m e. ( ZZ>= ` ( n + 1 ) ) )
441		c0ex	|- 0 e. _V
442	441	fvconst2	|- ( m e. ( ZZ>= ` ( n + 1 ) ) -> ( ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ` m ) = 0 )
443	440 442	syl	|- ( m e. ( ( n + 1 ) ... t ) -> ( ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ` m ) = 0 )
444	443	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ` m ) = 0 )
445	439 444	eqtr4d	|- ( ( ( ( n e. NN /\ t e. NN ) /\ n < t ) /\ m e. ( ( n + 1 ) ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ` m ) )
446	378 445	seqfveq	|- ( ( ( n e. NN /\ t e. NN ) /\ n < t ) -> ( seq ( n + 1 ) ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) = ( seq ( n + 1 ) ( + , ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ) ` t ) )
447		eqid	|- ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` ( n + 1 ) )
448	447	ser0	|- ( t e. ( ZZ>= ` ( n + 1 ) ) -> ( seq ( n + 1 ) ( + , ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ) ` t ) = 0 )
449	378 448	syl	|- ( ( ( n e. NN /\ t e. NN ) /\ n < t ) -> ( seq ( n + 1 ) ( + , ( ( ZZ>= ` ( n + 1 ) ) X. { 0 } ) ) ` t ) = 0 )
450	446 449	eqtrd	|- ( ( ( n e. NN /\ t e. NN ) /\ n < t ) -> ( seq ( n + 1 ) ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) = 0 )
451	450	adantlll	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq ( n + 1 ) ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) = 0 )
452	385 451	oveq12d	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) + ( seq ( n + 1 ) ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) + 0 ) )
453	172	ffvelrnda	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( ( ( abs o. - ) o. f ) ` m ) e. RR )
454	326 453	sylan2	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` m ) e. RR )
455	454	adantlr	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` m ) e. RR )
456		readdcl	|- ( ( m e. RR /\ v e. RR ) -> ( m + v ) e. RR )
457	456	adantl	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ ( m e. RR /\ v e. RR ) ) -> ( m + v ) e. RR )
458	314 455 457	seqcl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. RR )
459	458	ad2antrr	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. RR )
460	459	recnd	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. CC )
461	460	addid1d	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) + 0 ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
462	452 461	eqtrd	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` n ) + ( seq ( n + 1 ) ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
463	384 462	eqtrd	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
464	453	ad5ant15	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) /\ m e. NN ) -> ( ( ( abs o. - ) o. f ) ` m ) e. RR )
465	326 464	sylan2	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` m ) e. RR )
466	380 465 364	seqcl	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) e. RR )
467	466	leidd	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
468	463 467	eqbrtrd	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ n < t ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
469		elnnuz	|- ( t e. NN <-> t e. ( ZZ>= ` 1 ) )
470	469	biimpi	|- ( t e. NN -> t e. ( ZZ>= ` 1 ) )
471	470	ad2antlr	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) -> t e. ( ZZ>= ` 1 ) )
472		eqidd	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) = ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) )
473		simpr	|- ( ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) /\ z = m ) -> z = m )
474		elfzle1	|- ( m e. ( 1 ... t ) -> 1 <_ m )
475	474	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> 1 <_ m )
476	382	nnred	|- ( m e. ( 1 ... t ) -> m e. RR )
477	476	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> m e. RR )
478		nnre	|- ( t e. NN -> t e. RR )
479	478	ad3antlr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> t e. RR )
480	402	ad3antrrr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> n e. RR )
481		elfzle2	|- ( m e. ( 1 ... t ) -> m <_ t )
482	481	adantl	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> m <_ t )
483		simplr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> t <_ n )
484	477 479 480 482 483	letrd	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> m <_ n )
485		elfzelz	|- ( m e. ( 1 ... t ) -> m e. ZZ )
486	278	ad2antrr	|- ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) -> n e. ZZ )
487		elfz	|- ( ( m e. ZZ /\ 1 e. ZZ /\ n e. ZZ ) -> ( m e. ( 1 ... n ) <-> ( 1 <_ m /\ m <_ n ) ) )
488	174 487	mp3an2	|- ( ( m e. ZZ /\ n e. ZZ ) -> ( m e. ( 1 ... n ) <-> ( 1 <_ m /\ m <_ n ) ) )
489	485 486 488	syl2anr	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( m e. ( 1 ... n ) <-> ( 1 <_ m /\ m <_ n ) ) )
490	475 484 489	mpbir2and	|- ( ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> m e. ( 1 ... n ) )
491	490	ad5ant2345	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> m e. ( 1 ... n ) )
492	491	adantr	|- ( ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) /\ z = m ) -> m e. ( 1 ... n ) )
493	473 492	eqeltrd	|- ( ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) /\ z = m ) -> z e. ( 1 ... n ) )
494		iftrue	|- ( z e. ( 1 ... n ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) = ( f ` z ) )
495	493 494	syl	|- ( ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) /\ z = m ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) = ( f ` z ) )
496	237	adantl	|- ( ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) /\ z = m ) -> ( f ` z ) = ( f ` m ) )
497	495 496	eqtrd	|- ( ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) /\ z = m ) -> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) = ( f ` m ) )
498	382	adantl	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> m e. NN )
499	240	a1i	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( f ` m ) e. _V )
500	472 497 498 499	fvmptd	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) = ( f ` m ) )
501	500	fveq2d	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) = ( ( abs o. - ) ` ( f ` m ) ) )
502	333 382 334	sylancr	|- ( m e. ( 1 ... t ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
503	502	adantl	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( abs o. - ) ` ( ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ` m ) ) )
504		simplll	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) -> f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
505		fvco3	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( ( ( abs o. - ) o. f ) ` m ) = ( ( abs o. - ) ` ( f ` m ) ) )
506	504 382 505	syl2an	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( ( ( abs o. - ) o. f ) ` m ) = ( ( abs o. - ) ` ( f ` m ) ) )
507	501 503 506	3eqtr4d	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... t ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ` m ) = ( ( ( abs o. - ) o. f ) ` m ) )
508	471 507	seqfveq	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` t ) )
509		eluz	|- ( ( t e. ZZ /\ n e. ZZ ) -> ( n e. ( ZZ>= ` t ) <-> t <_ n ) )
510	374 278 509	syl2anr	|- ( ( n e. NN /\ t e. NN ) -> ( n e. ( ZZ>= ` t ) <-> t <_ n ) )
511	510	biimpar	|- ( ( ( n e. NN /\ t e. NN ) /\ t <_ n ) -> n e. ( ZZ>= ` t ) )
512	511	adantlll	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) -> n e. ( ZZ>= ` t ) )
513	504 326 453	syl2an	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. f ) ` m ) e. RR )
514		elfzelz	|- ( m e. ( ( t + 1 ) ... n ) -> m e. ZZ )
515	514	adantl	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> m e. ZZ )
516		0red	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> 0 e. RR )
517		peano2nn	|- ( t e. NN -> ( t + 1 ) e. NN )
518	517	nnred	|- ( t e. NN -> ( t + 1 ) e. RR )
519	518	adantr	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> ( t + 1 ) e. RR )
520	514	zred	|- ( m e. ( ( t + 1 ) ... n ) -> m e. RR )
521	520	adantl	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> m e. RR )
522	517	nngt0d	|- ( t e. NN -> 0 < ( t + 1 ) )
523	522	adantr	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> 0 < ( t + 1 ) )
524		elfzle1	|- ( m e. ( ( t + 1 ) ... n ) -> ( t + 1 ) <_ m )
525	524	adantl	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> ( t + 1 ) <_ m )
526	516 519 521 523 525	ltletrd	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> 0 < m )
527	515 526 398	sylanbrc	|- ( ( t e. NN /\ m e. ( ( t + 1 ) ... n ) ) -> m e. NN )
528	527	adantlr	|- ( ( ( t e. NN /\ t <_ n ) /\ m e. ( ( t + 1 ) ... n ) ) -> m e. NN )
529	528	adantlll	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( ( t + 1 ) ... n ) ) -> m e. NN )
530	170	ffvelrnda	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( f ` m ) e. ( CC X. CC ) )
531		ffvelrn	|- ( ( - : ( CC X. CC ) --> CC /\ ( f ` m ) e. ( CC X. CC ) ) -> ( - ` ( f ` m ) ) e. CC )
532	137 530 531	sylancr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( - ` ( f ` m ) ) e. CC )
533	532	absge0d	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> 0 <_ ( abs ` ( - ` ( f ` m ) ) ) )
534		fvco3	|- ( ( - : ( CC X. CC ) --> CC /\ ( f ` m ) e. ( CC X. CC ) ) -> ( ( abs o. - ) ` ( f ` m ) ) = ( abs ` ( - ` ( f ` m ) ) ) )
535	137 530 534	sylancr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( ( abs o. - ) ` ( f ` m ) ) = ( abs ` ( - ` ( f ` m ) ) ) )
536	505 535	eqtrd	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> ( ( ( abs o. - ) o. f ) ` m ) = ( abs ` ( - ` ( f ` m ) ) ) )
537	533 536	breqtrrd	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ m e. NN ) -> 0 <_ ( ( ( abs o. - ) o. f ) ` m ) )
538	537	ad5ant15	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. NN ) -> 0 <_ ( ( ( abs o. - ) o. f ) ` m ) )
539	529 538	syldan	|- ( ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) /\ m e. ( ( t + 1 ) ... n ) ) -> 0 <_ ( ( ( abs o. - ) o. f ) ` m ) )
540	471 512 513 539	sermono	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
541	508 540	eqbrtrd	|- ( ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) /\ t <_ n ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
542	402	ad2antlr	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) -> n e. RR )
543	478	adantl	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) -> t e. RR )
544	468 541 542 543	ltlecasei	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ t e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
545	544	ralrimiva	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> A. t e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
546		breq1	|- ( m = ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) -> ( m <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) <-> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) ) )
547	546	ralrn	|- ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) Fn NN -> ( A. m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) m <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) <-> A. t e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) ) )
548	355 547	syl	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( A. m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) m <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) <-> A. t e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) ) )
549	548	adantr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( A. m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) m <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) <-> A. t e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ` t ) <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) ) )
550	545 549	mpbird	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> A. m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) m <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
551	550	r19.21bi	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ) -> m <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
552	361 362 551	lensymd	|- ( ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) /\ m e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) ) -> -. ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) < m )
553	311 322 358 552	supmax	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) , RR* , < ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
554	52 553	sylan	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> if ( z e. ( 1 ... n ) , ( f ` z ) , <. 0 , 0 >. ) ) ) ) , RR* , < ) = ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) )
555	255 309 554	3eqtr3rd	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) = ( vol* ` ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) ) )
556		elfznn	|- ( z e. ( 1 ... n ) -> z e. NN )
557	164 65	sseldi	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( f ` z ) e. ( RR X. RR ) )
558		1st2nd2	|- ( ( f ` z ) e. ( RR X. RR ) -> ( f ` z ) = <. ( 1st ` ( f ` z ) ) , ( 2nd ` ( f ` z ) ) >. )
559	558	fveq2d	|- ( ( f ` z ) e. ( RR X. RR ) -> ( [,] ` ( f ` z ) ) = ( [,] ` <. ( 1st ` ( f ` z ) ) , ( 2nd ` ( f ` z ) ) >. ) )
560		df-ov	|- ( ( 1st ` ( f ` z ) ) [,] ( 2nd ` ( f ` z ) ) ) = ( [,] ` <. ( 1st ` ( f ` z ) ) , ( 2nd ` ( f ` z ) ) >. )
561	559 560	eqtr4di	|- ( ( f ` z ) e. ( RR X. RR ) -> ( [,] ` ( f ` z ) ) = ( ( 1st ` ( f ` z ) ) [,] ( 2nd ` ( f ` z ) ) ) )
562		xp1st	|- ( ( f ` z ) e. ( RR X. RR ) -> ( 1st ` ( f ` z ) ) e. RR )
563		xp2nd	|- ( ( f ` z ) e. ( RR X. RR ) -> ( 2nd ` ( f ` z ) ) e. RR )
564		iccssre	|- ( ( ( 1st ` ( f ` z ) ) e. RR /\ ( 2nd ` ( f ` z ) ) e. RR ) -> ( ( 1st ` ( f ` z ) ) [,] ( 2nd ` ( f ` z ) ) ) C_ RR )
565	562 563 564	syl2anc	|- ( ( f ` z ) e. ( RR X. RR ) -> ( ( 1st ` ( f ` z ) ) [,] ( 2nd ` ( f ` z ) ) ) C_ RR )
566	561 565	eqsstrd	|- ( ( f ` z ) e. ( RR X. RR ) -> ( [,] ` ( f ` z ) ) C_ RR )
567	557 566	syl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( [,] ` ( f ` z ) ) C_ RR )
568	52 556 567	syl2an	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. ( 1 ... n ) ) -> ( [,] ` ( f ` z ) ) C_ RR )
569	568	ralrimiva	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ RR )
570		iunss	|- ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ RR <-> A. z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ RR )
571	569 570	sylibr	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ RR )
572	571	adantr	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ RR )
573		uzid	|- ( ( n + 1 ) e. ZZ -> ( n + 1 ) e. ( ZZ>= ` ( n + 1 ) ) )
574		ne0i	|- ( ( n + 1 ) e. ( ZZ>= ` ( n + 1 ) ) -> ( ZZ>= ` ( n + 1 ) ) =/= (/) )
575		iunconst	|- ( ( ZZ>= ` ( n + 1 ) ) =/= (/) -> U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) = ( [,] ` <. 0 , 0 >. ) )
576	373 573 574 575	4syl	|- ( n e. NN -> U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) = ( [,] ` <. 0 , 0 >. ) )
577		iccid	|- ( 0 e. RR* -> ( 0 [,] 0 ) = { 0 } )
578	259 577	ax-mp	|- ( 0 [,] 0 ) = { 0 }
579		df-ov	|- ( 0 [,] 0 ) = ( [,] ` <. 0 , 0 >. )
580	578 579	eqtr3i	|- { 0 } = ( [,] ` <. 0 , 0 >. )
581	576 580	eqtr4di	|- ( n e. NN -> U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) = { 0 } )
582		snssi	|- ( 0 e. RR -> { 0 } C_ RR )
583	199 582	ax-mp	|- { 0 } C_ RR
584	581 583	eqsstrdi	|- ( n e. NN -> U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) C_ RR )
585	584	adantl	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) C_ RR )
586	581	fveq2d	|- ( n e. NN -> ( vol* ` U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) = ( vol* ` { 0 } ) )
587	586	adantl	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( vol* ` U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) = ( vol* ` { 0 } ) )
588		ovolsn	|- ( 0 e. RR -> ( vol* ` { 0 } ) = 0 )
589	199 588	ax-mp	|- ( vol* ` { 0 } ) = 0
590	587 589	eqtrdi	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( vol* ` U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) = 0 )
591		ovolunnul	|- ( ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ RR /\ U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) C_ RR /\ ( vol* ` U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) = 0 ) -> ( vol* ` ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) ) = ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) )
592	572 585 590 591	syl3anc	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( vol* ` ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) u. U_ z e. ( ZZ>= ` ( n + 1 ) ) ( [,] ` <. 0 , 0 >. ) ) ) = ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) )
593	555 592	eqtrd	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) = ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) )
594	593	breq2d	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) <-> M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) )
595	594	biimpd	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ n e. NN ) -> ( M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) -> M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) )
596	595	reximdva	|- ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> ( E. n e. NN M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) -> E. n e. NN M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) )
597	596	adantl	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> ( E. n e. NN M < ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` n ) -> E. n e. NN M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) )
598	194 597	mpd	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> E. n e. NN M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) )
599		fzfi	|- ( 1 ... n ) e. Fin
600		icccld	|- ( ( ( 1st ` ( f ` z ) ) e. RR /\ ( 2nd ` ( f ` z ) ) e. RR ) -> ( ( 1st ` ( f ` z ) ) [,] ( 2nd ` ( f ` z ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
601	562 563 600	syl2anc	|- ( ( f ` z ) e. ( RR X. RR ) -> ( ( 1st ` ( f ` z ) ) [,] ( 2nd ` ( f ` z ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
602	561 601	eqeltrd	|- ( ( f ` z ) e. ( RR X. RR ) -> ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
603	557 602	syl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
604	556 603	sylan2	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. ( 1 ... n ) ) -> ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
605	604	ralrimiva	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
606		uniretop	|- RR = U. ( topGen ` ran (,) )
607	606	iuncld	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( 1 ... n ) e. Fin /\ A. z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
608	1 599 605 607	mp3an12i	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
609	608	adantr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( n e. NN /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
610		fveq2	|- ( b = ( f ` z ) -> ( [,] ` b ) = ( [,] ` ( f ` z ) ) )
611	610	sseq1d	|- ( b = ( f ` z ) -> ( ( [,] ` b ) C_ A <-> ( [,] ` ( f ` z ) ) C_ A ) )
612	611	elrab	|- ( ( f ` z ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } <-> ( ( f ` z ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) /\ ( [,] ` ( f ` z ) ) C_ A ) )
613	612	simprbi	|- ( ( f ` z ) e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } -> ( [,] ` ( f ` z ) ) C_ A )
614	65 73 613	3syl	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. NN ) -> ( [,] ` ( f ` z ) ) C_ A )
615	556 614	sylan2	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ z e. ( 1 ... n ) ) -> ( [,] ` ( f ` z ) ) C_ A )
616	615	ralrimiva	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> A. z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A )
617		iunss	|- ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A <-> A. z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A )
618	616 617	sylibr	|- ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A )
619	618	adantr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( n e. NN /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A )
620		simprr	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( n e. NN /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) )
621		sseq1	|- ( s = U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) -> ( s C_ A <-> U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A ) )
622		fveq2	|- ( s = U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) -> ( vol* ` s ) = ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) )
623	622	breq2d	|- ( s = U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) -> ( M < ( vol* ` s ) <-> M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) )
624	621 623	anbi12d	|- ( s = U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) -> ( ( s C_ A /\ M < ( vol* ` s ) ) <-> ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) )
625	624	rspcev	|- ( ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) C_ A /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
626	609 619 620 625	syl12anc	|- ( ( f : NN --> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( n e. NN /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
627	52 626	sylan	|- ( ( f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } /\ ( n e. NN /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
628	627	adantll	|- ( ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) /\ ( n e. NN /\ M < ( vol* ` U_ z e. ( 1 ... n ) ( [,] ` ( f ` z ) ) ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
629	598 628	rexlimddv	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
630	629	adantlr	|- ( ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A =/= (/) ) /\ f : NN -1-1-onto-> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
631	17 630	exlimddv	|- ( ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) /\ A =/= (/) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )
632	15 631	pm2.61dane	|- ( ( A e. ( topGen ` ran (,) ) /\ M e. RR /\ M < ( vol* ` A ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ M < ( vol* ` s ) ) )