Theorem ioombl1lem4 19408

Description: Lemma for ioombl1 19409. (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 3521	. . . . 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 19335	. . . 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 1184	. . 3 |- ( ph -> ( vol * ` ( E i^i B ) ) e. RR )
7		difss 3434	. . . . 5 |- ( E \ B ) C_ E
8	7	a1i 11	. . . 4 |- ( ph -> ( E \ B ) C_ E )
9		ovolsscl 19335	. . . 4 |- ( ( ( E \ B ) C_ E /\ E C_ RR /\ ( vol * ` E ) e. RR ) -> ( vol * ` ( E \ B ) ) e. RR )
10	8, 3, 4, 9	syl3anc 1184	. . 3 |- ( ph -> ( vol * ` ( E \ B ) ) e. RR )
11	6, 10	readdcld 9071	. 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 19406	. 2 |- ( ph -> sup ( ran S , RR* , < ) e. RR )
26	14	rpred 10604	. . 3 |- ( ph -> C e. RR )
27	4, 26	readdcld 9071	. 2 |- ( ph -> ( ( vol * ` E ) + C ) e. RR )
28	12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24	ioombl1lem1 19405	. . . . . . . . 9 |- ( ph -> ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) )
29	28	simpld 446	. . . . . . . 8 |- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
30		eqid 2404	. . . . . . . . 9 |- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
31	30, 16	ovolsf 19322	. . . . . . . 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 5556	. . . . . . 7 |- ( T : NN --> ( 0 [,) +oo ) -> ran T C_ ( 0 [,) +oo ) )
34	32, 33	syl 16	. . . . . 6 |- ( ph -> ran T C_ ( 0 [,) +oo ) )
35		0re 9047	. . . . . . 7 |- 0 e. RR
36		pnfxr 10669	. . . . . . 7 |- +oo e. RR*
37		icossre 10947	. . . . . . 7 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
38	35, 36, 37	mp2an 654	. . . . . 6 |- ( 0 [,) +oo ) C_ RR
39	34, 38	syl6ss 3320	. . . . 5 |- ( ph -> ran T C_ RR )
40		1nn 9967	. . . . . . . 8 |- 1 e. NN
41		fdm 5554	. . . . . . . . 9 |- ( T : NN --> ( 0 [,) +oo ) -> dom T = NN )
42	32, 41	syl 16	. . . . . . . 8 |- ( ph -> dom T = NN )
43	40, 42	syl5eleqr 2491	. . . . . . 7 |- ( ph -> 1 e. dom T )
44		ne0i 3594	. . . . . . 7 |- ( 1 e. dom T -> dom T =/= (/) )
45	43, 44	syl 16	. . . . . 6 |- ( ph -> dom T =/= (/) )
46		dm0rn0 5045	. . . . . . 7 |- ( dom T = (/) <-> ran T = (/) )
47	46	necon3bii 2599	. . . . . 6 |- ( dom T =/= (/) <-> ran T =/= (/) )
48	45, 47	sylib 189	. . . . 5 |- ( ph -> ran T =/= (/) )
49	32	ffvelrnda 5829	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( T ` j ) e. ( 0 [,) +oo ) )
50	38, 49	sseldi 3306	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( T ` j ) e. RR )
51		eqid 2404	. . . . . . . . . . . . 13 |- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
52	51, 15	ovolsf 19322	. . . . . . . . . . . 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 5829	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( S ` j ) e. ( 0 [,) +oo ) )
55	38, 54	sseldi 3306	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( S ` j ) e. RR )
56	25	adantr 452	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> sup ( ran S , RR* , < ) e. RR )
57		simpr 448	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> j e. NN )
58		nnuz 10477	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
59	57, 58	syl6eleq 2494	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
60		simpl 444	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> ph )
61		elfznn 11036	. . . . . . . . . . . 12 |- ( n e. ( 1 ... j ) -> n e. NN )
62	30	ovolfsf 19321	. . . . . . . . . . . . . . 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 5829	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) )
65	38, 64	sseldi 3306	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR )
66	60, 61, 65	syl2an 464	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR )
67	51	ovolfsf 19321	. . . . . . . . . . . . . . . 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 5829	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) )
70		elrege0 10963	. . . . . . . . . . . . . 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 189	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) )
72	71	simpld 446	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
73	60, 61, 72	syl2an 464	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
74	28	simprd 450	. . . . . . . . . . . . . . . . . 18 |- ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
75		eqid 2404	. . . . . . . . . . . . . . . . . . 19 |- ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
76	75	ovolfsf 19321	. . . . . . . . . . . . . . . . . 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 5829	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) )
79		elrege0 10963	. . . . . . . . . . . . . . . 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 189	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) )
81	80	simprd 450	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` n ) )
82	80	simpld 446	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR )
83	65, 82	addge01d 9570	. . . . . . . . . . . . . 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 202	. . . . . . . . . . . . 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 19407	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( ( abs o. - ) o. F ) ` n ) )
86	84, 85	breqtrd 4196	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
87	60, 61, 86	syl2an 464	. . . . . . . . . . 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 11333	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) )
89	16	fveq1i 5688	. . . . . . . . . 10 |- ( T ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j )
90	15	fveq1i 5688	. . . . . . . . . 10 |- ( S ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j )
91	88, 89, 90	3brtr4g 4204	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( T ` j ) <_ ( S ` j ) )
92		1z 10267	. . . . . . . . . . . . . . . 16 |- 1 e. ZZ
93	92	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. ZZ )
94		eqidd 2405	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( abs o. - ) o. F ) ` n ) )
95	71	simprd 450	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) )
96		frn 5556	. . . . . . . . . . . . . . . . . . . . 21 |- ( S : NN --> ( 0 [,) +oo ) -> ran S C_ ( 0 [,) +oo ) )
97	53, 96	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran S C_ ( 0 [,) +oo ) )
98		icossxr 10951	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 [,) +oo ) C_ RR*
99	97, 98	syl6ss 3320	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ran S C_ RR* )
100	99	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ran S C_ RR* )
101		ffn 5550	. . . . . . . . . . . . . . . . . . . 20 |- ( S : NN --> ( 0 [,) +oo ) -> S Fn NN )
102	53, 101	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> S Fn NN )
103		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . 19 |- ( ( S Fn NN /\ k e. NN ) -> ( S ` k ) e. ran S )
104	102, 103	sylan 458	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( S ` k ) e. ran S )
105		supxrub 10859	. . . . . . . . . . . . . . . . . 18 |- ( ( ran S C_ RR* /\ ( S ` k ) e. ran S ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) )
106	100, 104, 105	syl2anc 643	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) )
107	106	ralrimiva 2749	. . . . . . . . . . . . . . . 16 |- ( ph -> A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) )
108		breq2 4176	. . . . . . . . . . . . . . . . . 18 |- ( x = sup ( ran S , RR* , < ) -> ( ( S ` k ) <_ x <-> ( S ` k ) <_ sup ( ran S , RR* , < ) ) )
109	108	ralbidv 2686	. . . . . . . . . . . . . . . . 17 |- ( x = sup ( ran S , RR* , < ) -> ( A. k e. NN ( S ` k ) <_ x <-> A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) ) )
110	109	rspcev 3012	. . . . . . . . . . . . . . . 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 )
111	25, 107, 110	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> E. x e. RR A. k e. NN ( S ` k ) <_ x )
112	58, 15, 93, 94, 72, 95, 111	isumsup2 12581	. . . . . . . . . . . . . 14 |- ( ph -> S ~~> sup ( ran S , RR , < ) )
113	97, 38	syl6ss 3320	. . . . . . . . . . . . . . 15 |- ( ph -> ran S C_ RR )
114		fdm 5554	. . . . . . . . . . . . . . . . . . 19 |- ( S : NN --> ( 0 [,) +oo ) -> dom S = NN )
115	53, 114	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom S = NN )
116	40, 115	syl5eleqr 2491	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. dom S )
117		ne0i 3594	. . . . . . . . . . . . . . . . 17 |- ( 1 e. dom S -> dom S =/= (/) )
118	116, 117	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom S =/= (/) )
119		dm0rn0 5045	. . . . . . . . . . . . . . . . 17 |- ( dom S = (/) <-> ran S = (/) )
120	119	necon3bii 2599	. . . . . . . . . . . . . . . 16 |- ( dom S =/= (/) <-> ran S =/= (/) )
121	118, 120	sylib 189	. . . . . . . . . . . . . . 15 |- ( ph -> ran S =/= (/) )
122		breq1 4175	. . . . . . . . . . . . . . . . . . 19 |- ( z = ( S ` k ) -> ( z <_ x <-> ( S ` k ) <_ x ) )
123	122	ralrn 5832	. . . . . . . . . . . . . . . . . 18 |- ( S Fn NN -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
124	102, 123	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
125	124	rexbidv 2687	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E. x e. RR A. z e. ran S z <_ x <-> E. x e. RR A. k e. NN ( S ` k ) <_ x ) )
126	111, 125	mpbird 224	. . . . . . . . . . . . . . 15 |- ( ph -> E. x e. RR A. z e. ran S z <_ x )
127		supxrre 10862	. . . . . . . . . . . . . . 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 , < ) )
128	113, 121, 126, 127	syl3anc 1184	. . . . . . . . . . . . . 14 |- ( ph -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
129	112, 128	breqtrrd 4198	. . . . . . . . . . . . 13 |- ( ph -> S ~~> sup ( ran S , RR* , < ) )
130	129	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> S ~~> sup ( ran S , RR* , < ) )
131	15, 130	syl5eqbrr 4206	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. F ) ) ~~> sup ( ran S , RR* , < ) )
132	72	adantlr 696	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
133	95	adantlr 696	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) )
134	58, 57, 131, 132, 133	climserle 12411	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) <_ sup ( ran S , RR* , < ) )
135	90, 134	syl5eqbr 4205	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( S ` j ) <_ sup ( ran S , RR* , < ) )
136	50, 55, 56, 91, 135	letrd 9183	. . . . . . . 8 |- ( ( ph /\ j e. NN ) -> ( T ` j ) <_ sup ( ran S , RR* , < ) )
137	136	ralrimiva 2749	. . . . . . 7 |- ( ph -> A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) )
138		breq2 4176	. . . . . . . . 9 |- ( x = sup ( ran S , RR* , < ) -> ( ( T ` j ) <_ x <-> ( T ` j ) <_ sup ( ran S , RR* , < ) ) )
139	138	ralbidv 2686	. . . . . . . 8 |- ( x = sup ( ran S , RR* , < ) -> ( A. j e. NN ( T ` j ) <_ x <-> A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) ) )
140	139	rspcev 3012	. . . . . . 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 )
141	25, 137, 140	syl2anc 643	. . . . . 6 |- ( ph -> E. x e. RR A. j e. NN ( T ` j ) <_ x )
142		ffn 5550	. . . . . . . . 9 |- ( T : NN --> ( 0 [,) +oo ) -> T Fn NN )
143	32, 142	syl 16	. . . . . . . 8 |- ( ph -> T Fn NN )
144		breq1 4175	. . . . . . . . 9 |- ( z = ( T ` j ) -> ( z <_ x <-> ( T ` j ) <_ x ) )
145	144	ralrn 5832	. . . . . . . 8 |- ( T Fn NN -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) )
146	143, 145	syl 16	. . . . . . 7 |- ( ph -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) )
147	146	rexbidv 2687	. . . . . 6 |- ( ph -> ( E. x e. RR A. z e. ran T z <_ x <-> E. x e. RR A. j e. NN ( T ` j ) <_ x ) )
148	141, 147	mpbird 224	. . . . 5 |- ( ph -> E. x e. RR A. z e. ran T z <_ x )
149		suprcl 9924	. . . . 5 |- ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR , < ) e. RR )
150	39, 48, 148, 149	syl3anc 1184	. . . 4 |- ( ph -> sup ( ran T , RR , < ) e. RR )
151	75, 17	ovolsf 19322	. . . . . . . 8 |- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
152	74, 151	syl 16	. . . . . . 7 |- ( ph -> U : NN --> ( 0 [,) +oo ) )
153		frn 5556	. . . . . . 7 |- ( U : NN --> ( 0 [,) +oo ) -> ran U C_ ( 0 [,) +oo ) )
154	152, 153	syl 16	. . . . . 6 |- ( ph -> ran U C_ ( 0 [,) +oo ) )
155	154, 38	syl6ss 3320	. . . . 5 |- ( ph -> ran U C_ RR )
156		fdm 5554	. . . . . . . . 9 |- ( U : NN --> ( 0 [,) +oo ) -> dom U = NN )
157	152, 156	syl 16	. . . . . . . 8 |- ( ph -> dom U = NN )
158	40, 157	syl5eleqr 2491	. . . . . . 7 |- ( ph -> 1 e. dom U )
159		ne0i 3594	. . . . . . 7 |- ( 1 e. dom U -> dom U =/= (/) )
160	158, 159	syl 16	. . . . . 6 |- ( ph -> dom U =/= (/) )
161		dm0rn0 5045	. . . . . . 7 |- ( dom U = (/) <-> ran U = (/) )
162	161	necon3bii 2599	. . . . . 6 |- ( dom U =/= (/) <-> ran U =/= (/) )
163	160, 162	sylib 189	. . . . 5 |- ( ph -> ran U =/= (/) )
164	152	ffvelrnda 5829	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( U ` j ) e. ( 0 [,) +oo ) )
165	38, 164	sseldi 3306	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( U ` j ) e. RR )
166	60, 61, 82	syl2an 464	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR )
167		elrege0 10963	. . . . . . . . . . . . . . . 16 |- ( ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) )
168	64, 167	sylib 189	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) )
169	168	simprd 450	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. G ) ` n ) )
170	82, 65	addge02d 9571	. . . . . . . . . . . . . 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 ) ) ) )
171	169, 170	mpbid 202	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
172	171, 85	breqtrd 4196	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
173	60, 61, 172	syl2an 464	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
174	59, 166, 73, 173	serle 11333	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) )
175	17	fveq1i 5688	. . . . . . . . . 10 |- ( U ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j )
176	174, 175, 90	3brtr4g 4204	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( U ` j ) <_ ( S ` j ) )
177	165, 55, 56, 176, 135	letrd 9183	. . . . . . . 8 |- ( ( ph /\ j e. NN ) -> ( U ` j ) <_ sup ( ran S , RR* , < ) )
178	177	ralrimiva 2749	. . . . . . 7 |- ( ph -> A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) )
179		breq2 4176	. . . . . . . . 9 |- ( x = sup ( ran S , RR* , < ) -> ( ( U ` j ) <_ x <-> ( U ` j ) <_ sup ( ran S , RR* , < ) ) )
180	179	ralbidv 2686	. . . . . . . 8 |- ( x = sup ( ran S , RR* , < ) -> ( A. j e. NN ( U ` j ) <_ x <-> A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) ) )
181	180	rspcev 3012	. . . . . . 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 )
182	25, 178, 181	syl2anc 643	. . . . . 6 |- ( ph -> E. x e. RR A. j e. NN ( U ` j ) <_ x )
183		ffn 5550	. . . . . . . . 9 |- ( U : NN --> ( 0 [,) +oo ) -> U Fn NN )
184	152, 183	syl 16	. . . . . . . 8 |- ( ph -> U Fn NN )
185		breq1 4175	. . . . . . . . 9 |- ( z = ( U ` j ) -> ( z <_ x <-> ( U ` j ) <_ x ) )
186	185	ralrn 5832	. . . . . . . 8 |- ( U Fn NN -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) )
187	184, 186	syl 16	. . . . . . 7 |- ( ph -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) )
188	187	rexbidv 2687	. . . . . 6 |- ( ph -> ( E. x e. RR A. z e. ran U z <_ x <-> E. x e. RR A. j e. NN ( U ` j ) <_ x ) )
189	182, 188	mpbird 224	. . . . 5 |- ( ph -> E. x e. RR A. z e. ran U z <_ x )
190		suprcl 9924	. . . . 5 |- ( ( ran U C_ RR /\ ran U =/= (/) /\ E. x e. RR A. z e. ran U z <_ x ) -> sup ( ran U , RR , < ) e. RR )
191	155, 163, 189, 190	syl3anc 1184	. . . 4 |- ( ph -> sup ( ran U , RR , < ) e. RR )
192		ssralv 3367	. . . . . . . . . 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 ) ) ) ) )
193	1, 192	ax-mp 8	. . . . . . . . 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 ) ) ) )
194	21	breq1i 4179	. . . . . . . . . . . . 13 |- ( P < x <-> ( 1st ` ( F ` n ) ) < x )
195		ovolfcl 19316	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
196	18, 195	sylan 458	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
197	196	simp1d 969	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR )
198	21, 197	syl5eqel 2488	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> P e. RR )
199	198	adantlr 696	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> P e. RR )
200	1, 3	syl5ss 3319	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( E i^i B ) C_ RR )
201	200	sselda 3308	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( E i^i B ) ) -> x e. RR )
202	201	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> x e. RR )
203		ltle 9119	. . . . . . . . . . . . . . 15 |- ( ( P e. RR /\ x e. RR ) -> ( P < x -> P <_ x ) )
204	199, 202, 203	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) )
205		simpr 448	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n e. NN ) -> n e. NN )
206		opex 4387	. . . . . . . . . . . . . . . . . . . 20 |- <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V
207	23	fvmpt2 5771	. . . . . . . . . . . . . . . . . . . 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 >. )
208	205, 206, 207	sylancl 644	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
209	208	fveq2d 5691	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
210	13	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ n e. NN ) -> A e. RR )
211		ifcl 3735	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. RR /\ P e. RR ) -> if ( P <_ A , A , P ) e. RR )
212	210, 198, 211	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n e. NN ) -> if ( P <_ A , A , P ) e. RR )
213	196	simp2d 970	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR )
214	22, 213	syl5eqel 2488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n e. NN ) -> Q e. RR )
215		ifcl 3735	. . . . . . . . . . . . . . . . . . . 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 )
216	212, 214, 215	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
217		op1stg 6318	. . . . . . . . . . . . . . . . . . 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 ) )
218	216, 214, 217	syl2anc 643	. . . . . . . . . . . . . . . . . 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 ) )
219	209, 218	eqtrd 2436	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
220	219	ad2ant2r 728	. . . . . . . . . . . . . . . 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 ) )
221	216	ad2ant2r 728	. . . . . . . . . . . . . . . . 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 )
222	212	ad2ant2r 728	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) e. RR )
223	200	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( E i^i B ) C_ RR )
224		simplr 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. ( E i^i B ) )
225	223, 224	sseldd 3309	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. RR )
226	214	ad2ant2r 728	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> Q e. RR )
227		min1 10732	. . . . . . . . . . . . . . . . . 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 ) )
228	222, 226, 227	syl2anc 643	. . . . . . . . . . . . . . . . 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 ) )
229	13	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A e. RR )
230		inss2 3522	. . . . . . . . . . . . . . . . . . . . . 22 |- ( E i^i B ) C_ B
231	230	sseli 3304	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( E i^i B ) -> x e. B )
232	231	ad2antlr 708	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. B )
233	13	rexrd 9090	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> A e. RR* )
234		elioo2 10913	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR* /\ +oo e. RR* ) -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
235	233, 36, 234	sylancl 644	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
236	12	eleq2i 2468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. B <-> x e. ( A (,) +oo ) )
237		ltpnf 10677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. RR -> x < +oo )
238	237	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( x e. RR /\ A < x ) -> x < +oo )
239	238	pm4.71i 614	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x e. RR /\ A < x ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) )
240		df-3an 938	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x e. RR /\ A < x /\ x < +oo ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) )
241	239, 240	bitr4i 244	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. RR /\ A < x ) <-> ( x e. RR /\ A < x /\ x < +oo ) )
242	235, 236, 241	3bitr4g 280	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( x e. B <-> ( x e. RR /\ A < x ) ) )
243		simpr 448	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. RR /\ A < x ) -> A < x )
244	242, 243	syl6bi 220	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( x e. B -> A < x ) )
245	244	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( x e. B -> A < x ) )
246	232, 245	mpd 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A < x )
247	229, 225, 246	ltled 9177	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A <_ x )
248		simprr 734	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> P <_ x )
249		breq1 4175	. . . . . . . . . . . . . . . . . . 19 |- ( A = if ( P <_ A , A , P ) -> ( A <_ x <-> if ( P <_ A , A , P ) <_ x ) )
250		breq1 4175	. . . . . . . . . . . . . . . . . . 19 |- ( P = if ( P <_ A , A , P ) -> ( P <_ x <-> if ( P <_ A , A , P ) <_ x ) )
251	249, 250	ifboth 3730	. . . . . . . . . . . . . . . . . 18 |- ( ( A <_ x /\ P <_ x ) -> if ( P <_ A , A , P ) <_ x )
252	247, 248, 251	syl2anc 643	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) <_ x )
253	221, 222, 225, 228, 252	letrd 9183	. . . . . . . . . . . . . . . 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 )
254	220, 253	eqbrtrd 4192	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) <_ x )
255	254	expr 599	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P <_ x -> ( 1st ` ( G ` n ) ) <_ x ) )
256	204, 255	syld 42	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> ( 1st ` ( G ` n ) ) <_ x ) )
257	194, 256	syl5bir 210	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( G ` n ) ) <_ x ) )
258	22	breq2i 4180	. . . . . . . . . . . . . 14 |- ( x < Q <-> x < ( 2nd ` ( F ` n ) ) )
259	214	adantlr 696	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> Q e. RR )
260		ltle 9119	. . . . . . . . . . . . . . 15 |- ( ( x e. RR /\ Q e. RR ) -> ( x < Q -> x <_ Q ) )
261	202, 259, 260	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) )
262	258, 261	syl5bir 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ Q ) )
263	208	fveq2d 5691	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
264		op2ndg 6319	. . . . . . . . . . . . . . . . 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 )
265	216, 214, 264	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q )
266	263, 265	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
267	266	adantlr 696	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
268	267	breq2d 4184	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x <_ ( 2nd ` ( G ` n ) ) <-> x <_ Q ) )
269	262, 268	sylibrd 226	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( G ` n ) ) ) )
270	257, 269	anim12d 547	. . . . . . . . . . 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 ) ) ) ) )
271	270	reximdva 2778	. . . . . . . . . 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 ) ) ) ) )
272	271	ralimdva 2744	. . . . . . . . 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 ) ) ) ) )
273	193, 272	syl5 30	. . . . . . . 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 ) ) ) ) )
274		ovolfioo 19317	. . . . . . . . 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 ) ) ) ) )
275	3, 18, 274	syl2anc 643	. . . . . . . 8 |- ( ph -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
276		ovolficc 19318	. . . . . . . . 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 ) ) ) ) )
277	200, 29, 276	syl2anc 643	. . . . . . . 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 ) ) ) ) )
278	273, 275, 277	3imtr4d 260	. . . . . . 7 |- ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E i^i B ) C_ U. ran ( [,] o. G ) ) )
279	19, 278	mpd 15	. . . . . 6 |- ( ph -> ( E i^i B ) C_ U. ran ( [,] o. G ) )
280	16	ovollb2 19338	. . . . . 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* , < ) )
281	29, 279, 280	syl2anc 643	. . . . 5 |- ( ph -> ( vol * ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) )
282		supxrre 10862	. . . . . 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 , < ) )
283	39, 48, 148, 282	syl3anc 1184	. . . . 5 |- ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
284	281, 283	breqtrd 4196	. . . 4 |- ( ph -> ( vol * ` ( E i^i B ) ) <_ sup ( ran T , RR , < ) )
285		ssralv 3367	. . . . . . . . . 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 ) ) ) ) )
286	7, 285	ax-mp 8	. . . . . . . . 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 ) ) ) )
287	198	adantlr 696	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> P e. RR )
288	7, 3	syl5ss 3319	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( E \ B ) C_ RR )
289	288	sselda 3308	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( E \ B ) ) -> x e. RR )
290	289	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> x e. RR )
291	287, 290, 203	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) )
292	194, 291	syl5bir 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> P <_ x ) )
293		opex 4387	. . . . . . . . . . . . . . . . . 18 |- <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V
294	24	fvmpt2 5771	. . . . . . . . . . . . . . . . . 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 ) >. )
295	205, 293, 294	sylancl 644	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
296	295	fveq2d 5691	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
297		op1stg 6318	. . . . . . . . . . . . . . . . 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 )
298	198, 216, 297	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P )
299	296, 298	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
300	299	adantlr 696	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
301	300	breq1d 4182	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( H ` n ) ) <_ x <-> P <_ x ) )
302	292, 301	sylibrd 226	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( H ` n ) ) <_ x ) )
303	214	adantlr 696	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> Q e. RR )
304	290, 303, 260	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) )
305	288	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( E \ B ) C_ RR )
306		simplr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. ( E \ B ) )
307	305, 306	sseldd 3309	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. RR )
308	13	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A e. RR )
309	198	ad2ant2r 728	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> P e. RR )
310	308, 309, 211	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> if ( P <_ A , A , P ) e. RR )
311		eldifn 3430	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( E \ B ) -> -. x e. B )
312	311	ad2antlr 708	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. x e. B )
313	307	biantrurd 495	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> ( x e. RR /\ A < x ) ) )
314	242	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( x e. B <-> ( x e. RR /\ A < x ) ) )
315	313, 314	bitr4d 248	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> x e. B ) )
316	312, 315	mtbird 293	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. A < x )
317	307, 308	lenltd 9175	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( x <_ A <-> -. A < x ) )
318	316, 317	mpbird 224	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ A )
319		max2 10731	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. RR /\ A e. RR ) -> A <_ if ( P <_ A , A , P ) )
320	309, 308, 319	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A <_ if ( P <_ A , A , P ) )
321	307, 308, 310, 318, 320	letrd 9183	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( P <_ A , A , P ) )
322		simprr 734	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ Q )
323		breq2 4176	. . . . . . . . . . . . . . . . . 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 ) ) )
324		breq2 4176	. . . . . . . . . . . . . . . . . 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 ) ) )
325	323, 324	ifboth 3730	. . . . . . . . . . . . . . . . 17 |- ( ( x <_ if ( P <_ A , A , P ) /\ x <_ Q ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
326	321, 322, 325	syl2anc 643	. . . . . . . . . . . . . . . 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 ) )
327	295	fveq2d 5691	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
328		op2ndg 6319	. . . . . . . . . . . . . . . . . . 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 ) )
329	198, 216, 328	syl2anc 643	. . . . . . . . . . . . . . . . . 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 ) )
330	327, 329	eqtrd 2436	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
331	330	ad2ant2r 728	. . . . . . . . . . . . . . . 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 ) )
332	326, 331	breqtrrd 4198	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ ( 2nd ` ( H ` n ) ) )
333	332	expr 599	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x <_ Q -> x <_ ( 2nd ` ( H ` n ) ) ) )
334	304, 333	syld 42	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ ( 2nd ` ( H ` n ) ) ) )
335	258, 334	syl5bir 210	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( H ` n ) ) ) )
336	302, 335	anim12d 547	. . . . . . . . . . 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 ) ) ) ) )
337	336	reximdva 2778	. . . . . . . . . 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 ) ) ) ) )
338	337	ralimdva 2744	. . . . . . . . 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 ) ) ) ) )
339	286, 338	syl5 30	. . . . . . . 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 ) ) ) ) )
340		ovolficc 19318	. . . . . . . . 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 ) ) ) ) )
341	288, 74, 340	syl2anc 643	. . . . . . . 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 ) ) ) ) )
342	339, 275, 341	3imtr4d 260	. . . . . . 7 |- ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E \ B ) C_ U. ran ( [,] o. H ) ) )
343	19, 342	mpd 15	. . . . . 6 |- ( ph -> ( E \ B ) C_ U. ran ( [,] o. H ) )
344	17	ovollb2 19338	. . . . . 6 |- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E \ B ) C_ U. ran ( [,] o. H ) ) -> ( vol * ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) )
345	74, 343, 344	syl2anc 643	. . . . 5 |- ( ph -> ( vol * ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) )
346		supxrre 10862	. . . . . 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 , < ) )
347	155, 163, 189, 346	syl3anc 1184	. . . . 5 |- ( ph -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) )
348	345, 347	breqtrd 4196	. . . 4 |- ( ph -> ( vol * ` ( E \ B ) ) <_ sup ( ran U , RR , < ) )
349	6, 10, 150, 191, 284, 348	le2addd 9600	. . 3 |- ( ph -> ( ( vol * ` ( E i^i B ) ) + ( vol * ` ( E \ B ) ) ) <_ ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) )
350		eqidd 2405	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( ( abs o. - ) o. G ) ` n ) )
351	58, 16, 93, 350, 65, 169, 141	isumsup2 12581	. . . . 5 |- ( ph -> T ~~> sup ( ran T , RR , < ) )
352		seqex 11280	. . . . . . 7 |- seq 1 ( + , ( ( abs o. - ) o. F ) ) e. _V
353	15, 352	eqeltri 2474	. . . . . 6 |- S e. _V
354	353	a1i 11	. . . . 5 |- ( ph -> S e. _V )
355		eqidd 2405	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( ( ( abs o. - ) o. H ) ` n ) )
356	58, 17, 93, 355, 82, 81, 182	isumsup2 12581	. . . . 5 |- ( ph -> U ~~> sup ( ran U , RR , < ) )
357	50	recnd 9070	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( T ` j ) e. CC )
358	165	recnd 9070	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( U ` j ) e. CC )
359	65	recnd 9070	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC )
360	60, 61, 359	syl2an 464	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC )
361	82	recnd 9070	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC )
362	60, 61, 361	syl2an 464	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC )
363	85	eqcomd 2409	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
364	60, 61, 363	syl2an 464	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
365	59, 360, 362, 364	seradd 11320	. . . . . 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 ) ) )
366	89, 175	oveq12i 6052	. . . . . 6 |- ( ( T ` j ) + ( U ` j ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) )
367	365, 90, 366	3eqtr4g 2461	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( S ` j ) = ( ( T ` j ) + ( U ` j ) ) )
368	58, 93, 351, 354, 356, 357, 358, 367	climadd 12380	. . . 4 |- ( ph -> S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) )
369		climuni 12301	. . . 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* , < ) )
370	368, 129, 369	syl2anc 643	. . 3 |- ( ph -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) )
371	349, 370	breqtrd 4196	. 2 |- ( ph -> ( ( vol * ` ( E i^i B ) ) + ( vol * ` ( E \ B ) ) ) <_ sup ( ran S , RR* , < ) )
372	11, 25, 27, 371, 20	letrd 9183	1 |- ( ph -> ( ( vol * ` ( E i^i B ) ) + ( vol * ` ( E \ B ) ) ) <_ ( ( vol * ` E ) + C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   \ cdif 3277   i^i cin 3279   C_ wss 3280   (/)c0 3588   ifcif 3699   <.cop 3777   U.cuni 3975   class class class wbr 4172   e. cmpt 4226   X. cxp 4835   dom cdm 4837   ran crn 4838   o. ccom 4841   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   1stc1st 6306   2ndc2nd 6307   supcsup 7403   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   +oocpnf 9073   RR*cxr 9075   < clt 9076   <_ cle 9077   - cmin 9247   NNcn 9956   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   (,)cioo 10872   [,)cico 10874   [,]cicc 10875   ...cfz 10999   seq cseq 11278   abscabs 11994   ~~> cli 12233   vol *covol 19312

This theorem is referenced by:  ioombl1  19409

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-ioo 10876  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-rlim 12238  df-sum 12435  df-ovol 19314