Theorem ioombl1lem4 21706

Description: Lemma for ioombl1 21707. (Contributed by Mario Carneiro, 16-Jun-2014.)

Hypotheses

Ref	Expression
ioombl1.b	|- B = ( A (,) +oo )
ioombl1.a	|- ( ph -> A e. RR )
ioombl1.e	|- ( ph -> E C_ RR )
ioombl1.v	|- ( ph -> ( vol* ` E ) e. RR )
ioombl1.c	|- ( ph -> C e. RR+ )
ioombl1.s	|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ioombl1.t	|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ioombl1.u	|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ioombl1.f1	|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ioombl1.f2	|- ( ph -> E C_ U. ran ( (,) o. F ) )
ioombl1.f3	|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) )
ioombl1.p	|- P = ( 1st ` ( F ` n ) )
ioombl1.q	|- Q = ( 2nd ` ( F ` n ) )
ioombl1.g	|- G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
ioombl1.h	|- H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )

Assertion

Ref	Expression
ioombl1lem4	|- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( ( vol* ` E ) + C ) )

Distinct variable groups:   B, n   C, n   n, E   n, F   n, G   n, H   ph, n   S, n

Allowed substitution hints:   A( n)   P( n)   Q( n)   T( n)   U( n)

Proof of Theorem ioombl1lem4

Dummy variables x j k z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3718	. . . . 5 |- ( E i^i B ) C_ E
2	1	a1i 11	. . . 4 |- ( ph -> ( E i^i B ) C_ E )
3		ioombl1.e	. . . 4 |- ( ph -> E C_ RR )
4		ioombl1.v	. . . 4 |- ( ph -> ( vol* ` E ) e. RR )
5		ovolsscl 21632	. . . 4 |- ( ( ( E i^i B ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i B ) ) e. RR )
6	2, 3, 4, 5	syl3anc 1228	. . 3 |- ( ph -> ( vol* ` ( E i^i B ) ) e. RR )
7		difss 3631	. . . . 5 |- ( E \ B ) C_ E
8	7	a1i 11	. . . 4 |- ( ph -> ( E \ B ) C_ E )
9		ovolsscl 21632	. . . 4 |- ( ( ( E \ B ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ B ) ) e. RR )
10	8, 3, 4, 9	syl3anc 1228	. . 3 |- ( ph -> ( vol* ` ( E \ B ) ) e. RR )
11	6, 10	readdcld 9619	. 2 |- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) e. RR )
12		ioombl1.b	. . 3 |- B = ( A (,) +oo )
13		ioombl1.a	. . 3 |- ( ph -> A e. RR )
14		ioombl1.c	. . 3 |- ( ph -> C e. RR+ )
15		ioombl1.s	. . 3 |- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
16		ioombl1.t	. . 3 |- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
17		ioombl1.u	. . 3 |- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
18		ioombl1.f1	. . 3 |- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
19		ioombl1.f2	. . 3 |- ( ph -> E C_ U. ran ( (,) o. F ) )
20		ioombl1.f3	. . 3 |- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) )
21		ioombl1.p	. . 3 |- P = ( 1st ` ( F ` n ) )
22		ioombl1.q	. . 3 |- Q = ( 2nd ` ( F ` n ) )
23		ioombl1.g	. . 3 |- G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
24		ioombl1.h	. . 3 |- H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
25	12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24	ioombl1lem2 21704	. 2 |- ( ph -> sup ( ran S , RR* , < ) e. RR )
26	14	rpred 11252	. . 3 |- ( ph -> C e. RR )
27	4, 26	readdcld 9619	. 2 |- ( ph -> ( ( vol* ` E ) + C ) e. RR )
28	12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24	ioombl1lem1 21703	. . . . . . . . 9 |- ( ph -> ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) )
29	28	simpld 459	. . . . . . . 8 |- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
30		eqid 2467	. . . . . . . . 9 |- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
31	30, 16	ovolsf 21619	. . . . . . . 8 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
32	29, 31	syl 16	. . . . . . 7 |- ( ph -> T : NN --> ( 0 [,) +oo ) )
33		frn 5735	. . . . . . 7 |- ( T : NN --> ( 0 [,) +oo ) -> ran T C_ ( 0 [,) +oo ) )
34	32, 33	syl 16	. . . . . 6 |- ( ph -> ran T C_ ( 0 [,) +oo ) )
35		0re 9592	. . . . . . 7 |- 0 e. RR
36		pnfxr 11317	. . . . . . 7 |- +oo e. RR*
37		icossre 11601	. . . . . . 7 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
38	35, 36, 37	mp2an 672	. . . . . 6 |- ( 0 [,) +oo ) C_ RR
39	34, 38	syl6ss 3516	. . . . 5 |- ( ph -> ran T C_ RR )
40		1nn 10543	. . . . . . . 8 |- 1 e. NN
41		fdm 5733	. . . . . . . . 9 |- ( T : NN --> ( 0 [,) +oo ) -> dom T = NN )
42	32, 41	syl 16	. . . . . . . 8 |- ( ph -> dom T = NN )
43	40, 42	syl5eleqr 2562	. . . . . . 7 |- ( ph -> 1 e. dom T )
44		ne0i 3791	. . . . . . 7 |- ( 1 e. dom T -> dom T =/= (/) )
45	43, 44	syl 16	. . . . . 6 |- ( ph -> dom T =/= (/) )
46		dm0rn0 5217	. . . . . . 7 |- ( dom T = (/) <-> ran T = (/) )
47	46	necon3bii 2735	. . . . . 6 |- ( dom T =/= (/) <-> ran T =/= (/) )
48	45, 47	sylib 196	. . . . 5 |- ( ph -> ran T =/= (/) )
49	32	ffvelrnda 6019	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( T ` j ) e. ( 0 [,) +oo ) )
50	38, 49	sseldi 3502	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( T ` j ) e. RR )
51		eqid 2467	. . . . . . . . . . . . 13 |- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
52	51, 15	ovolsf 21619	. . . . . . . . . . . 12 |- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
53	18, 52	syl 16	. . . . . . . . . . 11 |- ( ph -> S : NN --> ( 0 [,) +oo ) )
54	53	ffvelrnda 6019	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( S ` j ) e. ( 0 [,) +oo ) )
55	38, 54	sseldi 3502	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( S ` j ) e. RR )
56	25	adantr 465	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> sup ( ran S , RR* , < ) e. RR )
57		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> j e. NN )
58		nnuz 11113	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
59	57, 58	syl6eleq 2565	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
60		simpl 457	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> ph )
61		elfznn 11710	. . . . . . . . . . . 12 |- ( n e. ( 1 ... j ) -> n e. NN )
62	30	ovolfsf 21618	. . . . . . . . . . . . . . 15 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
63	29, 62	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
64	63	ffvelrnda 6019	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) )
65	38, 64	sseldi 3502	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR )
66	60, 61, 65	syl2an 477	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR )
67	51	ovolfsf 21618	. . . . . . . . . . . . . . . 16 |- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
68	18, 67	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
69	68	ffvelrnda 6019	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) )
70		elrege0 11623	. . . . . . . . . . . . . 14 |- ( ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) )
71	69, 70	sylib 196	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) )
72	71	simpld 459	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
73	60, 61, 72	syl2an 477	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
74	28	simprd 463	. . . . . . . . . . . . . . . . . 18 |- ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
75		eqid 2467	. . . . . . . . . . . . . . . . . . 19 |- ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
76	75	ovolfsf 21618	. . . . . . . . . . . . . . . . . 18 |- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
77	74, 76	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
78	77	ffvelrnda 6019	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) )
79		elrege0 11623	. . . . . . . . . . . . . . . 16 |- ( ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) )
80	78, 79	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) )
81	80	simprd 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` n ) )
82	80	simpld 459	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR )
83	65, 82	addge01d 10136	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( ( abs o. - ) o. H ) ` n ) <-> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) )
84	81, 83	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
85	12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24	ioombl1lem3 21705	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( ( abs o. - ) o. F ) ` n ) )
86	84, 85	breqtrd 4471	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
87	60, 61, 86	syl2an 477	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
88	59, 66, 73, 87	serle 12126	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) )
89	16	fveq1i 5865	. . . . . . . . . 10 |- ( T ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j )
90	15	fveq1i 5865	. . . . . . . . . 10 |- ( S ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j )
91	88, 89, 90	3brtr4g 4479	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( T ` j ) <_ ( S ` j ) )
92		1zzd 10891	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. ZZ )
93		eqidd 2468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( abs o. - ) o. F ) ` n ) )
94	71	simprd 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) )
95		frn 5735	. . . . . . . . . . . . . . . . . . . . 21 |- ( S : NN --> ( 0 [,) +oo ) -> ran S C_ ( 0 [,) +oo ) )
96	53, 95	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran S C_ ( 0 [,) +oo ) )
97		icossxr 11605	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 [,) +oo ) C_ RR*
98	96, 97	syl6ss 3516	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ran S C_ RR* )
99	98	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ran S C_ RR* )
100		ffn 5729	. . . . . . . . . . . . . . . . . . . 20 |- ( S : NN --> ( 0 [,) +oo ) -> S Fn NN )
101	53, 100	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> S Fn NN )
102		fnfvelrn 6016	. . . . . . . . . . . . . . . . . . 19 |- ( ( S Fn NN /\ k e. NN ) -> ( S ` k ) e. ran S )
103	101, 102	sylan 471	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( S ` k ) e. ran S )
104		supxrub 11512	. . . . . . . . . . . . . . . . . 18 |- ( ( ran S C_ RR* /\ ( S ` k ) e. ran S ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) )
105	99, 103, 104	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) )
106	105	ralrimiva 2878	. . . . . . . . . . . . . . . 16 |- ( ph -> A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) )
107		breq2 4451	. . . . . . . . . . . . . . . . . 18 |- ( x = sup ( ran S , RR* , < ) -> ( ( S ` k ) <_ x <-> ( S ` k ) <_ sup ( ran S , RR* , < ) ) )
108	107	ralbidv 2903	. . . . . . . . . . . . . . . . 17 |- ( x = sup ( ran S , RR* , < ) -> ( A. k e. NN ( S ` k ) <_ x <-> A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) ) )
109	108	rspcev 3214	. . . . . . . . . . . . . . . 16 |- ( ( sup ( ran S , RR* , < ) e. RR /\ A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. k e. NN ( S ` k ) <_ x )
110	25, 106, 109	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> E. x e. RR A. k e. NN ( S ` k ) <_ x )
111	58, 15, 92, 93, 72, 94, 110	isumsup2 13617	. . . . . . . . . . . . . 14 |- ( ph -> S ~~> sup ( ran S , RR , < ) )
112	96, 38	syl6ss 3516	. . . . . . . . . . . . . . 15 |- ( ph -> ran S C_ RR )
113		fdm 5733	. . . . . . . . . . . . . . . . . . 19 |- ( S : NN --> ( 0 [,) +oo ) -> dom S = NN )
114	53, 113	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom S = NN )
115	40, 114	syl5eleqr 2562	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. dom S )
116		ne0i 3791	. . . . . . . . . . . . . . . . 17 |- ( 1 e. dom S -> dom S =/= (/) )
117	115, 116	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom S =/= (/) )
118		dm0rn0 5217	. . . . . . . . . . . . . . . . 17 |- ( dom S = (/) <-> ran S = (/) )
119	118	necon3bii 2735	. . . . . . . . . . . . . . . 16 |- ( dom S =/= (/) <-> ran S =/= (/) )
120	117, 119	sylib 196	. . . . . . . . . . . . . . 15 |- ( ph -> ran S =/= (/) )
121		breq1 4450	. . . . . . . . . . . . . . . . . . 19 |- ( z = ( S ` k ) -> ( z <_ x <-> ( S ` k ) <_ x ) )
122	121	ralrn 6022	. . . . . . . . . . . . . . . . . 18 |- ( S Fn NN -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
123	101, 122	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
124	123	rexbidv 2973	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E. x e. RR A. z e. ran S z <_ x <-> E. x e. RR A. k e. NN ( S ` k ) <_ x ) )
125	110, 124	mpbird 232	. . . . . . . . . . . . . . 15 |- ( ph -> E. x e. RR A. z e. ran S z <_ x )
126		supxrre 11515	. . . . . . . . . . . . . . 15 |- ( ( ran S C_ RR /\ ran S =/= (/) /\ E. x e. RR A. z e. ran S z <_ x ) -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
127	112, 120, 125, 126	syl3anc 1228	. . . . . . . . . . . . . 14 |- ( ph -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
128	111, 127	breqtrrd 4473	. . . . . . . . . . . . 13 |- ( ph -> S ~~> sup ( ran S , RR* , < ) )
129	128	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> S ~~> sup ( ran S , RR* , < ) )
130	15, 129	syl5eqbrr 4481	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. F ) ) ~~> sup ( ran S , RR* , < ) )
131	72	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
132	94	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) )
133	58, 57, 130, 131, 132	climserle 13444	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) <_ sup ( ran S , RR* , < ) )
134	90, 133	syl5eqbr 4480	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( S ` j ) <_ sup ( ran S , RR* , < ) )
135	50, 55, 56, 91, 134	letrd 9734	. . . . . . . 8 |- ( ( ph /\ j e. NN ) -> ( T ` j ) <_ sup ( ran S , RR* , < ) )
136	135	ralrimiva 2878	. . . . . . 7 |- ( ph -> A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) )
137		breq2 4451	. . . . . . . . 9 |- ( x = sup ( ran S , RR* , < ) -> ( ( T ` j ) <_ x <-> ( T ` j ) <_ sup ( ran S , RR* , < ) ) )
138	137	ralbidv 2903	. . . . . . . 8 |- ( x = sup ( ran S , RR* , < ) -> ( A. j e. NN ( T ` j ) <_ x <-> A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) ) )
139	138	rspcev 3214	. . . . . . 7 |- ( ( sup ( ran S , RR* , < ) e. RR /\ A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. j e. NN ( T ` j ) <_ x )
140	25, 136, 139	syl2anc 661	. . . . . 6 |- ( ph -> E. x e. RR A. j e. NN ( T ` j ) <_ x )
141		ffn 5729	. . . . . . . . 9 |- ( T : NN --> ( 0 [,) +oo ) -> T Fn NN )
142	32, 141	syl 16	. . . . . . . 8 |- ( ph -> T Fn NN )
143		breq1 4450	. . . . . . . . 9 |- ( z = ( T ` j ) -> ( z <_ x <-> ( T ` j ) <_ x ) )
144	143	ralrn 6022	. . . . . . . 8 |- ( T Fn NN -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) )
145	142, 144	syl 16	. . . . . . 7 |- ( ph -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) )
146	145	rexbidv 2973	. . . . . 6 |- ( ph -> ( E. x e. RR A. z e. ran T z <_ x <-> E. x e. RR A. j e. NN ( T ` j ) <_ x ) )
147	140, 146	mpbird 232	. . . . 5 |- ( ph -> E. x e. RR A. z e. ran T z <_ x )
148		suprcl 10499	. . . . 5 |- ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR , < ) e. RR )
149	39, 48, 147, 148	syl3anc 1228	. . . 4 |- ( ph -> sup ( ran T , RR , < ) e. RR )
150	75, 17	ovolsf 21619	. . . . . . . 8 |- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
151	74, 150	syl 16	. . . . . . 7 |- ( ph -> U : NN --> ( 0 [,) +oo ) )
152		frn 5735	. . . . . . 7 |- ( U : NN --> ( 0 [,) +oo ) -> ran U C_ ( 0 [,) +oo ) )
153	151, 152	syl 16	. . . . . 6 |- ( ph -> ran U C_ ( 0 [,) +oo ) )
154	153, 38	syl6ss 3516	. . . . 5 |- ( ph -> ran U C_ RR )
155		fdm 5733	. . . . . . . . 9 |- ( U : NN --> ( 0 [,) +oo ) -> dom U = NN )
156	151, 155	syl 16	. . . . . . . 8 |- ( ph -> dom U = NN )
157	40, 156	syl5eleqr 2562	. . . . . . 7 |- ( ph -> 1 e. dom U )
158		ne0i 3791	. . . . . . 7 |- ( 1 e. dom U -> dom U =/= (/) )
159	157, 158	syl 16	. . . . . 6 |- ( ph -> dom U =/= (/) )
160		dm0rn0 5217	. . . . . . 7 |- ( dom U = (/) <-> ran U = (/) )
161	160	necon3bii 2735	. . . . . 6 |- ( dom U =/= (/) <-> ran U =/= (/) )
162	159, 161	sylib 196	. . . . 5 |- ( ph -> ran U =/= (/) )
163	151	ffvelrnda 6019	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( U ` j ) e. ( 0 [,) +oo ) )
164	38, 163	sseldi 3502	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( U ` j ) e. RR )
165	60, 61, 82	syl2an 477	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR )
166		elrege0 11623	. . . . . . . . . . . . . . . 16 |- ( ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) )
167	64, 166	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) )
168	167	simprd 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. G ) ` n ) )
169	82, 65	addge02d 10137	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( ( abs o. - ) o. G ) ` n ) <-> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) )
170	168, 169	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
171	170, 85	breqtrd 4471	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
172	60, 61, 171	syl2an 477	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
173	59, 165, 73, 172	serle 12126	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) )
174	17	fveq1i 5865	. . . . . . . . . 10 |- ( U ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j )
175	173, 174, 90	3brtr4g 4479	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( U ` j ) <_ ( S ` j ) )
176	164, 55, 56, 175, 134	letrd 9734	. . . . . . . 8 |- ( ( ph /\ j e. NN ) -> ( U ` j ) <_ sup ( ran S , RR* , < ) )
177	176	ralrimiva 2878	. . . . . . 7 |- ( ph -> A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) )
178		breq2 4451	. . . . . . . . 9 |- ( x = sup ( ran S , RR* , < ) -> ( ( U ` j ) <_ x <-> ( U ` j ) <_ sup ( ran S , RR* , < ) ) )
179	178	ralbidv 2903	. . . . . . . 8 |- ( x = sup ( ran S , RR* , < ) -> ( A. j e. NN ( U ` j ) <_ x <-> A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) ) )
180	179	rspcev 3214	. . . . . . 7 |- ( ( sup ( ran S , RR* , < ) e. RR /\ A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. j e. NN ( U ` j ) <_ x )
181	25, 177, 180	syl2anc 661	. . . . . 6 |- ( ph -> E. x e. RR A. j e. NN ( U ` j ) <_ x )
182		ffn 5729	. . . . . . . . 9 |- ( U : NN --> ( 0 [,) +oo ) -> U Fn NN )
183	151, 182	syl 16	. . . . . . . 8 |- ( ph -> U Fn NN )
184		breq1 4450	. . . . . . . . 9 |- ( z = ( U ` j ) -> ( z <_ x <-> ( U ` j ) <_ x ) )
185	184	ralrn 6022	. . . . . . . 8 |- ( U Fn NN -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) )
186	183, 185	syl 16	. . . . . . 7 |- ( ph -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) )
187	186	rexbidv 2973	. . . . . 6 |- ( ph -> ( E. x e. RR A. z e. ran U z <_ x <-> E. x e. RR A. j e. NN ( U ` j ) <_ x ) )
188	181, 187	mpbird 232	. . . . 5 |- ( ph -> E. x e. RR A. z e. ran U z <_ x )
189		suprcl 10499	. . . . 5 |- ( ( ran U C_ RR /\ ran U =/= (/) /\ E. x e. RR A. z e. ran U z <_ x ) -> sup ( ran U , RR , < ) e. RR )
190	154, 162, 188, 189	syl3anc 1228	. . . 4 |- ( ph -> sup ( ran U , RR , < ) e. RR )
191		ssralv 3564	. . . . . . . . . 10 |- ( ( E i^i B ) C_ E -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
192	1, 191	ax-mp 5	. . . . . . . . 9 |- ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) )
193	21	breq1i 4454	. . . . . . . . . . . . 13 |- ( P < x <-> ( 1st ` ( F ` n ) ) < x )
194		ovolfcl 21613	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
195	18, 194	sylan 471	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
196	195	simp1d 1008	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR )
197	21, 196	syl5eqel 2559	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> P e. RR )
198	197	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> P e. RR )
199	1, 3	syl5ss 3515	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( E i^i B ) C_ RR )
200	199	sselda 3504	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( E i^i B ) ) -> x e. RR )
201	200	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> x e. RR )
202		ltle 9669	. . . . . . . . . . . . . . 15 |- ( ( P e. RR /\ x e. RR ) -> ( P < x -> P <_ x ) )
203	198, 201, 202	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) )
204		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n e. NN ) -> n e. NN )
205		opex 4711	. . . . . . . . . . . . . . . . . . . 20 |- <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V
206	23	fvmpt2 5955	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. NN /\ <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
207	204, 205, 206	sylancl 662	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
208	207	fveq2d 5868	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
209	13	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ n e. NN ) -> A e. RR )
210		ifcl 3981	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. RR /\ P e. RR ) -> if ( P <_ A , A , P ) e. RR )
211	209, 197, 210	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n e. NN ) -> if ( P <_ A , A , P ) e. RR )
212	195	simp2d 1009	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR )
213	22, 212	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n e. NN ) -> Q e. RR )
214		ifcl 3981	. . . . . . . . . . . . . . . . . . . 20 |- ( ( if ( P <_ A , A , P ) e. RR /\ Q e. RR ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
215	211, 213, 214	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
216		op1stg 6793	. . . . . . . . . . . . . . . . . . 19 |- ( ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR /\ Q e. RR ) -> ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
217	215, 213, 216	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
218	208, 217	eqtrd 2508	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
219	218	ad2ant2r 746	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
220	215	ad2ant2r 746	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
221	211	ad2ant2r 746	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) e. RR )
222	199	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( E i^i B ) C_ RR )
223		simplr 754	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. ( E i^i B ) )
224	222, 223	sseldd 3505	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. RR )
225	213	ad2ant2r 746	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> Q e. RR )
226		min1 11385	. . . . . . . . . . . . . . . . . 18 |- ( ( if ( P <_ A , A , P ) e. RR /\ Q e. RR ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ if ( P <_ A , A , P ) )
227	221, 225, 226	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ if ( P <_ A , A , P ) )
228	13	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A e. RR )
229		inss2 3719	. . . . . . . . . . . . . . . . . . . . . 22 |- ( E i^i B ) C_ B
230	229	sseli 3500	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( E i^i B ) -> x e. B )
231	230	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. B )
232	13	rexrd 9639	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> A e. RR* )
233		elioo2 11566	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR* /\ +oo e. RR* ) -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
234	232, 36, 233	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
235	12	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. B <-> x e. ( A (,) +oo ) )
236		ltpnf 11327	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. RR -> x < +oo )
237	236	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( x e. RR /\ A < x ) -> x < +oo )
238	237	pm4.71i 632	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x e. RR /\ A < x ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) )
239		df-3an 975	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x e. RR /\ A < x /\ x < +oo ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) )
240	238, 239	bitr4i 252	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. RR /\ A < x ) <-> ( x e. RR /\ A < x /\ x < +oo ) )
241	234, 235, 240	3bitr4g 288	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( x e. B <-> ( x e. RR /\ A < x ) ) )
242		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. RR /\ A < x ) -> A < x )
243	241, 242	syl6bi 228	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( x e. B -> A < x ) )
244	243	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( x e. B -> A < x ) )
245	231, 244	mpd 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A < x )
246	228, 224, 245	ltled 9728	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A <_ x )
247		simprr 756	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> P <_ x )
248		breq1 4450	. . . . . . . . . . . . . . . . . . 19 |- ( A = if ( P <_ A , A , P ) -> ( A <_ x <-> if ( P <_ A , A , P ) <_ x ) )
249		breq1 4450	. . . . . . . . . . . . . . . . . . 19 |- ( P = if ( P <_ A , A , P ) -> ( P <_ x <-> if ( P <_ A , A , P ) <_ x ) )
250	248, 249	ifboth 3975	. . . . . . . . . . . . . . . . . 18 |- ( ( A <_ x /\ P <_ x ) -> if ( P <_ A , A , P ) <_ x )
251	246, 247, 250	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) <_ x )
252	220, 221, 224, 227, 251	letrd 9734	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ x )
253	219, 252	eqbrtrd 4467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) <_ x )
254	253	expr 615	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P <_ x -> ( 1st ` ( G ` n ) ) <_ x ) )
255	203, 254	syld 44	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> ( 1st ` ( G ` n ) ) <_ x ) )
256	193, 255	syl5bir 218	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( G ` n ) ) <_ x ) )
257	22	breq2i 4455	. . . . . . . . . . . . . 14 |- ( x < Q <-> x < ( 2nd ` ( F ` n ) ) )
258	213	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> Q e. RR )
259		ltle 9669	. . . . . . . . . . . . . . 15 |- ( ( x e. RR /\ Q e. RR ) -> ( x < Q -> x <_ Q ) )
260	201, 258, 259	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) )
261	257, 260	syl5bir 218	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ Q ) )
262	207	fveq2d 5868	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
263		op2ndg 6794	. . . . . . . . . . . . . . . . 17 |- ( ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR /\ Q e. RR ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q )
264	215, 213, 263	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q )
265	262, 264	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
266	265	adantlr 714	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
267	266	breq2d 4459	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x <_ ( 2nd ` ( G ` n ) ) <-> x <_ Q ) )
268	261, 267	sylibrd 234	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( G ` n ) ) ) )
269	256, 268	anim12d 563	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
270	269	reximdva 2938	. . . . . . . . . 10 |- ( ( ph /\ x e. ( E i^i B ) ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
271	270	ralimdva 2872	. . . . . . . . 9 |- ( ph -> ( A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
272	192, 271	syl5 32	. . . . . . . 8 |- ( ph -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
273		ovolfioo 21614	. . . . . . . . 9 |- ( ( E C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
274	3, 18, 273	syl2anc 661	. . . . . . . 8 |- ( ph -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
275		ovolficc 21615	. . . . . . . . 9 |- ( ( ( E i^i B ) C_ RR /\ G : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( E i^i B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
276	199, 29, 275	syl2anc 661	. . . . . . . 8 |- ( ph -> ( ( E i^i B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
277	272, 274, 276	3imtr4d 268	. . . . . . 7 |- ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E i^i B ) C_ U. ran ( [,] o. G ) ) )
278	19, 277	mpd 15	. . . . . 6 |- ( ph -> ( E i^i B ) C_ U. ran ( [,] o. G ) )
279	16	ovollb2 21635	. . . . . 6 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E i^i B ) C_ U. ran ( [,] o. G ) ) -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) )
280	29, 278, 279	syl2anc 661	. . . . 5 |- ( ph -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) )
281		supxrre 11515	. . . . . 6 |- ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
282	39, 48, 147, 281	syl3anc 1228	. . . . 5 |- ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
283	280, 282	breqtrd 4471	. . . 4 |- ( ph -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR , < ) )
284		ssralv 3564	. . . . . . . . . 10 |- ( ( E \ B ) C_ E -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
285	7, 284	ax-mp 5	. . . . . . . . 9 |- ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) )
286	197	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> P e. RR )
287	7, 3	syl5ss 3515	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( E \ B ) C_ RR )
288	287	sselda 3504	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( E \ B ) ) -> x e. RR )
289	288	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> x e. RR )
290	286, 289, 202	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) )
291	193, 290	syl5bir 218	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> P <_ x ) )
292		opex 4711	. . . . . . . . . . . . . . . . . 18 |- <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V
293	24	fvmpt2 5955	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. NN /\ <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
294	204, 292, 293	sylancl 662	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
295	294	fveq2d 5868	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
296		op1stg 6793	. . . . . . . . . . . . . . . . 17 |- ( ( P e. RR /\ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P )
297	197, 215, 296	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P )
298	295, 297	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
299	298	adantlr 714	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
300	299	breq1d 4457	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( H ` n ) ) <_ x <-> P <_ x ) )
301	291, 300	sylibrd 234	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( H ` n ) ) <_ x ) )
302	213	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> Q e. RR )
303	289, 302, 259	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) )
304	287	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( E \ B ) C_ RR )
305		simplr 754	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. ( E \ B ) )
306	304, 305	sseldd 3505	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. RR )
307	13	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A e. RR )
308	197	ad2ant2r 746	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> P e. RR )
309	307, 308, 210	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> if ( P <_ A , A , P ) e. RR )
310		eldifn 3627	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( E \ B ) -> -. x e. B )
311	310	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. x e. B )
312	306	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> ( x e. RR /\ A < x ) ) )
313	241	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( x e. B <-> ( x e. RR /\ A < x ) ) )
314	312, 313	bitr4d 256	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> x e. B ) )
315	311, 314	mtbird 301	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. A < x )
316	306, 307	lenltd 9726	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( x <_ A <-> -. A < x ) )
317	315, 316	mpbird 232	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ A )
318		max2 11384	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. RR /\ A e. RR ) -> A <_ if ( P <_ A , A , P ) )
319	308, 307, 318	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A <_ if ( P <_ A , A , P ) )
320	306, 307, 309, 317, 319	letrd 9734	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( P <_ A , A , P ) )
321		simprr 756	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ Q )
322		breq2 4451	. . . . . . . . . . . . . . . . . 18 |- ( if ( P <_ A , A , P ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( x <_ if ( P <_ A , A , P ) <-> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
323		breq2 4451	. . . . . . . . . . . . . . . . . 18 |- ( Q = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( x <_ Q <-> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
324	322, 323	ifboth 3975	. . . . . . . . . . . . . . . . 17 |- ( ( x <_ if ( P <_ A , A , P ) /\ x <_ Q ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
325	320, 321, 324	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
326	294	fveq2d 5868	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
327		op2ndg 6794	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. RR /\ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) -> ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
328	197, 215, 327	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
329	326, 328	eqtrd 2508	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
330	329	ad2ant2r 746	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
331	325, 330	breqtrrd 4473	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ ( 2nd ` ( H ` n ) ) )
332	331	expr 615	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x <_ Q -> x <_ ( 2nd ` ( H ` n ) ) ) )
333	303, 332	syld 44	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ ( 2nd ` ( H ` n ) ) ) )
334	257, 333	syl5bir 218	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( H ` n ) ) ) )
335	301, 334	anim12d 563	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
336	335	reximdva 2938	. . . . . . . . . 10 |- ( ( ph /\ x e. ( E \ B ) ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
337	336	ralimdva 2872	. . . . . . . . 9 |- ( ph -> ( A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
338	285, 337	syl5 32	. . . . . . . 8 |- ( ph -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
339		ovolficc 21615	. . . . . . . . 9 |- ( ( ( E \ B ) C_ RR /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( E \ B ) C_ U. ran ( [,] o. H ) <-> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
340	287, 74, 339	syl2anc 661	. . . . . . . 8 |- ( ph -> ( ( E \ B ) C_ U. ran ( [,] o. H ) <-> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
341	338, 274, 340	3imtr4d 268	. . . . . . 7 |- ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E \ B ) C_ U. ran ( [,] o. H ) ) )
342	19, 341	mpd 15	. . . . . 6 |- ( ph -> ( E \ B ) C_ U. ran ( [,] o. H ) )
343	17	ovollb2 21635	. . . . . 6 |- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E \ B ) C_ U. ran ( [,] o. H ) ) -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) )
344	74, 342, 343	syl2anc 661	. . . . 5 |- ( ph -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) )
345		supxrre 11515	. . . . . 6 |- ( ( ran U C_ RR /\ ran U =/= (/) /\ E. x e. RR A. z e. ran U z <_ x ) -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) )
346	154, 162, 188, 345	syl3anc 1228	. . . . 5 |- ( ph -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) )
347	344, 346	breqtrd 4471	. . . 4 |- ( ph -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR , < ) )
348	6, 10, 149, 190, 283, 347	le2addd 10166	. . 3 |- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) )
349		eqidd 2468	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( ( abs o. - ) o. G ) ` n ) )
350	58, 16, 92, 349, 65, 168, 140	isumsup2 13617	. . . . 5 |- ( ph -> T ~~> sup ( ran T , RR , < ) )
351		seqex 12073	. . . . . . 7 |- seq 1 ( + , ( ( abs o. - ) o. F ) ) e. _V
352	15, 351	eqeltri 2551	. . . . . 6 |- S e. _V
353	352	a1i 11	. . . . 5 |- ( ph -> S e. _V )
354		eqidd 2468	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( ( ( abs o. - ) o. H ) ` n ) )
355	58, 17, 92, 354, 82, 81, 181	isumsup2 13617	. . . . 5 |- ( ph -> U ~~> sup ( ran U , RR , < ) )
356	50	recnd 9618	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( T ` j ) e. CC )
357	164	recnd 9618	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( U ` j ) e. CC )
358	65	recnd 9618	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC )
359	60, 61, 358	syl2an 477	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC )
360	82	recnd 9618	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC )
361	60, 61, 360	syl2an 477	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC )
362	85	eqcomd 2475	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
363	60, 61, 362	syl2an 477	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
364	59, 359, 361, 363	seradd 12113	. . . . . 6 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) ) )
365	89, 174	oveq12i 6294	. . . . . 6 |- ( ( T ` j ) + ( U ` j ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) )
366	364, 90, 365	3eqtr4g 2533	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( S ` j ) = ( ( T ` j ) + ( U ` j ) ) )
367	58, 92, 350, 353, 355, 356, 357, 366	climadd 13413	. . . 4 |- ( ph -> S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) )
368		climuni 13334	. . . 4 |- ( ( S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) /\ S ~~> sup ( ran S , RR* , < ) ) -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) )
369	367, 128, 368	syl2anc 661	. . 3 |- ( ph -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) )
370	348, 369	breqtrd 4471	. 2 |- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ sup ( ran S , RR* , < ) )
371	11, 25, 27, 370, 20	letrd 9734	1 |- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( ( vol* ` E ) + C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   \ cdif 3473   i^i cin 3475   C_ wss 3476   (/)c0 3785   ifcif 3939   <.cop 4033   U.cuni 4245   class class class wbr 4447   |-> cmpt 4505   X. cxp 4997   dom cdm 4999   ran crn 5000   o. ccom 5003   Fn wfn 5581   -->wf 5582   ` cfv 5586  (class class class)co 6282   1stc1st 6779   2ndc2nd 6780   supcsup 7896   CCcc 9486   RRcr 9487   0cc0 9488   1c1 9489   + caddc 9491   +oocpnf 9621   RR*cxr 9623   < clt 9624   <_ cle 9625   - cmin 9801   NNcn 10532   ZZ>=cuz 11078   RR+crp 11216   (,)cioo 11525   [,)cico 11527   [,]cicc 11528   ...cfz 11668   seqcseq 12071   abscabs 13026   ~~> cli 13266   vol*covol 21609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-map 7419  df-pm 7420  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-sup 7897  df-oi 7931  df-card 8316  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11079  df-q 11179  df-rp 11217  df-ioo 11529  df-ico 11531  df-icc 11532  df-fz 11669  df-fzo 11789  df-fl 11893  df-seq 12072  df-exp 12131  df-hash 12370  df-cj 12891  df-re 12892  df-im 12893  df-sqrt 13027  df-abs 13028  df-clim 13270  df-rlim 13271  df-sum 13468  df-ovol 21611

This theorem is referenced by:  ioombl1  21707