Theorem ovolunlem1a 23264

Description: Lemma for ovolun 23267. (Contributed by Mario Carneiro, 7-May-2015.)

Hypotheses

Ref	Expression
ovolun.a	|- ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
ovolun.b	|- ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
ovolun.c	|- ( ph -> C e. RR+ )
ovolun.s	|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolun.t	|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ovolun.u	|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ovolun.f1	|- ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovolun.f2	|- ( ph -> A C_ U. ran ( (,) o. F ) )
ovolun.f3	|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
ovolun.g1	|- ( ph -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovolun.g2	|- ( ph -> B C_ U. ran ( (,) o. G ) )
ovolun.g3	|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
ovolun.h	|- H = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) )

Assertion

Ref	Expression
ovolunlem1a	|- ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )

Distinct variable groups:   k, n, C   k, F, n   k, H   A, k, n   B, k, n   S, k   T, k   k, G, n   ph, k, n   U, k

Allowed substitution hints:   S( n)   T( n)   U( n)   H( n)

Proof of Theorem ovolunlem1a

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

Step	Hyp	Ref	Expression
1		ovolun.g1	. . . . . . . . . 10 |- ( ph -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
2		reex 10027	. . . . . . . . . . . . 13 |- RR e. _V
3	2, 2	xpex 6962	. . . . . . . . . . . 12 |- ( RR X. RR ) e. _V
4	3	inex2 4800	. . . . . . . . . . 11 |- ( <_ i^i ( RR X. RR ) ) e. _V
5		nnex 11026	. . . . . . . . . . 11 |- NN e. _V
6	4, 5	elmap 7886	. . . . . . . . . 10 |- ( G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> G : NN --> ( <_ i^i ( RR X. RR ) ) )
7	1, 6	sylib 208	. . . . . . . . 9 |- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8	7	adantr 481	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
9	8	ffvelrnda 6359	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ ( n / 2 ) e. NN ) -> ( G ` ( n / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
10		nneo 11461	. . . . . . . . . . 11 |- ( n e. NN -> ( ( n / 2 ) e. NN <-> -. ( ( n + 1 ) / 2 ) e. NN ) )
11	10	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( ( n / 2 ) e. NN <-> -. ( ( n + 1 ) / 2 ) e. NN ) )
12	11	con2bid 344	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( ( n + 1 ) / 2 ) e. NN <-> -. ( n / 2 ) e. NN ) )
13	12	biimpar 502	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ -. ( n / 2 ) e. NN ) -> ( ( n + 1 ) / 2 ) e. NN )
14		ovolun.f1	. . . . . . . . . . 11 |- ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
15	4, 5	elmap 7886	. . . . . . . . . . 11 |- ( F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( <_ i^i ( RR X. RR ) ) )
16	14, 15	sylib 208	. . . . . . . . . 10 |- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
17	16	adantr 481	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
18	17	ffvelrnda 6359	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ ( ( n + 1 ) / 2 ) e. NN ) -> ( F ` ( ( n + 1 ) / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
19	13, 18	syldan 487	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ -. ( n / 2 ) e. NN ) -> ( F ` ( ( n + 1 ) / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
20	9, 19	ifclda 4120	. . . . . 6 |- ( ( ph /\ n e. NN ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
21		ovolun.h	. . . . . 6 |- H = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) )
22	20, 21	fmptd 6385	. . . . 5 |- ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
23		eqid 2622	. . . . . 6 |- ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
24		ovolun.u	. . . . . 6 |- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
25	23, 24	ovolsf 23241	. . . . 5 |- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
26	22, 25	syl 17	. . . 4 |- ( ph -> U : NN --> ( 0 [,) +oo ) )
27		rge0ssre 12280	. . . 4 |- ( 0 [,) +oo ) C_ RR
28		fss 6056	. . . 4 |- ( ( U : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> U : NN --> RR )
29	26, 27, 28	sylancl 694	. . 3 |- ( ph -> U : NN --> RR )
30	29	ffvelrnda 6359	. 2 |- ( ( ph /\ k e. NN ) -> ( U ` k ) e. RR )
31		2nn 11185	. . . 4 |- 2 e. NN
32		peano2nn 11032	. . . . . . . . 9 |- ( k e. NN -> ( k + 1 ) e. NN )
33	32	adantl 482	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
34	33	nnred 11035	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
35	34	rehalfcld 11279	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( ( k + 1 ) / 2 ) e. RR )
36	35	flcld 12599	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( |_ ` ( ( k + 1 ) / 2 ) ) e. ZZ )
37		ax-1cn 9994	. . . . . . . . 9 |- 1 e. CC
38	37	2timesi 11147	. . . . . . . 8 |- ( 2 x. 1 ) = ( 1 + 1 )
39		nnge1 11046	. . . . . . . . . 10 |- ( k e. NN -> 1 <_ k )
40	39	adantl 482	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> 1 <_ k )
41		nnre 11027	. . . . . . . . . . 11 |- ( k e. NN -> k e. RR )
42	41	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> k e. RR )
43		1re 10039	. . . . . . . . . . 11 |- 1 e. RR
44		leadd1 10496	. . . . . . . . . . 11 |- ( ( 1 e. RR /\ k e. RR /\ 1 e. RR ) -> ( 1 <_ k <-> ( 1 + 1 ) <_ ( k + 1 ) ) )
45	43, 43, 44	mp3an13 1415	. . . . . . . . . 10 |- ( k e. RR -> ( 1 <_ k <-> ( 1 + 1 ) <_ ( k + 1 ) ) )
46	42, 45	syl 17	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> ( 1 <_ k <-> ( 1 + 1 ) <_ ( k + 1 ) ) )
47	40, 46	mpbid 222	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( 1 + 1 ) <_ ( k + 1 ) )
48	38, 47	syl5eqbr 4688	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( 2 x. 1 ) <_ ( k + 1 ) )
49		2re 11090	. . . . . . . . . 10 |- 2 e. RR
50		2pos 11112	. . . . . . . . . 10 |- 0 < 2
51	49, 50	pm3.2i 471	. . . . . . . . 9 |- ( 2 e. RR /\ 0 < 2 )
52		lemuldiv2 10904	. . . . . . . . 9 |- ( ( 1 e. RR /\ ( k + 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. 1 ) <_ ( k + 1 ) <-> 1 <_ ( ( k + 1 ) / 2 ) ) )
53	43, 51, 52	mp3an13 1415	. . . . . . . 8 |- ( ( k + 1 ) e. RR -> ( ( 2 x. 1 ) <_ ( k + 1 ) <-> 1 <_ ( ( k + 1 ) / 2 ) ) )
54	34, 53	syl 17	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. 1 ) <_ ( k + 1 ) <-> 1 <_ ( ( k + 1 ) / 2 ) ) )
55	48, 54	mpbid 222	. . . . . 6 |- ( ( ph /\ k e. NN ) -> 1 <_ ( ( k + 1 ) / 2 ) )
56		1z 11407	. . . . . . 7 |- 1 e. ZZ
57		flge 12606	. . . . . . 7 |- ( ( ( ( k + 1 ) / 2 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( ( k + 1 ) / 2 ) <-> 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
58	35, 56, 57	sylancl 694	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( 1 <_ ( ( k + 1 ) / 2 ) <-> 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
59	55, 58	mpbid 222	. . . . 5 |- ( ( ph /\ k e. NN ) -> 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) )
60		elnnz1 11403	. . . . 5 |- ( ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN <-> ( ( |_ ` ( ( k + 1 ) / 2 ) ) e. ZZ /\ 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
61	36, 59, 60	sylanbrc 698	. . . 4 |- ( ( ph /\ k e. NN ) -> ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN )
62		nnmulcl 11043	. . . 4 |- ( ( 2 e. NN /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN )
63	31, 61, 62	sylancr 695	. . 3 |- ( ( ph /\ k e. NN ) -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN )
64	29	ffvelrnda 6359	. . 3 |- ( ( ph /\ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) e. RR )
65	63, 64	syldan 487	. 2 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) e. RR )
66		ovolun.a	. . . . . 6 |- ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
67	66	simprd 479	. . . . 5 |- ( ph -> ( vol* ` A ) e. RR )
68		ovolun.b	. . . . . 6 |- ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
69	68	simprd 479	. . . . 5 |- ( ph -> ( vol* ` B ) e. RR )
70	67, 69	readdcld 10069	. . . 4 |- ( ph -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
71		ovolun.c	. . . . 5 |- ( ph -> C e. RR+ )
72	71	rpred 11872	. . . 4 |- ( ph -> C e. RR )
73	70, 72	readdcld 10069	. . 3 |- ( ph -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR )
74	73	adantr 481	. 2 |- ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR )
75		simpr 477	. . . . 5 |- ( ( ph /\ k e. NN ) -> k e. NN )
76		nnuz 11723	. . . . 5 |- NN = ( ZZ>= ` 1 )
77	75, 76	syl6eleq 2711	. . . 4 |- ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
78		nnz 11399	. . . . . . 7 |- ( k e. NN -> k e. ZZ )
79	78	adantl 482	. . . . . 6 |- ( ( ph /\ k e. NN ) -> k e. ZZ )
80		flhalf 12631	. . . . . 6 |- ( k e. ZZ -> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
81	79, 80	syl 17	. . . . 5 |- ( ( ph /\ k e. NN ) -> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
82		nnz 11399	. . . . . . 7 |- ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ZZ )
83		eluz 11701	. . . . . . 7 |- ( ( k e. ZZ /\ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ZZ ) -> ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) <-> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
84	78, 82, 83	syl2an 494	. . . . . 6 |- ( ( k e. NN /\ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN ) -> ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) <-> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
85	75, 63, 84	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) <-> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
86	81, 85	mpbird 247	. . . 4 |- ( ( ph /\ k e. NN ) -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) )
87		elfznn 12370	. . . . 5 |- ( j e. ( 1 ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) -> j e. NN )
88	23	ovolfsf 23240	. . . . . . . . . 10 |- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
89	22, 88	syl 17	. . . . . . . . 9 |- ( ph -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
90	89	adantr 481	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
91	90	ffvelrnda 6359	. . . . . . 7 |- ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> ( ( ( abs o. - ) o. H ) ` j ) e. ( 0 [,) +oo ) )
92		elrege0 12278	. . . . . . 7 |- ( ( ( ( abs o. - ) o. H ) ` j ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. H ) ` j ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` j ) ) )
93	91, 92	sylib 208	. . . . . 6 |- ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> ( ( ( ( abs o. - ) o. H ) ` j ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` j ) ) )
94	93	simpld 475	. . . . 5 |- ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> ( ( ( abs o. - ) o. H ) ` j ) e. RR )
95	87, 94	sylan2 491	. . . 4 |- ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) -> ( ( ( abs o. - ) o. H ) ` j ) e. RR )
96		elfzuz 12338	. . . . . 6 |- ( j e. ( ( k + 1 ) ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) -> j e. ( ZZ>= ` ( k + 1 ) ) )
97		eluznn 11758	. . . . . 6 |- ( ( ( k + 1 ) e. NN /\ j e. ( ZZ>= ` ( k + 1 ) ) ) -> j e. NN )
98	33, 96, 97	syl2an 494	. . . . 5 |- ( ( ( ph /\ k e. NN ) /\ j e. ( ( k + 1 ) ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) -> j e. NN )
99	93	simprd 479	. . . . 5 |- ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` j ) )
100	98, 99	syldan 487	. . . 4 |- ( ( ( ph /\ k e. NN ) /\ j e. ( ( k + 1 ) ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` j ) )
101	77, 86, 95, 100	sermono 12833	. . 3 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` k ) <_ ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
102	24	fveq1i 6192	. . 3 |- ( U ` k ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` k )
103	24	fveq1i 6192	. . 3 |- ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
104	101, 102, 103	3brtr4g 4687	. 2 |- ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
105		eqid 2622	. . . . . . . . . 10 |- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
106		ovolun.s	. . . . . . . . . 10 |- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
107	105, 106	ovolsf 23241	. . . . . . . . 9 |- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
108	16, 107	syl 17	. . . . . . . 8 |- ( ph -> S : NN --> ( 0 [,) +oo ) )
109		frn 6053	. . . . . . . 8 |- ( S : NN --> ( 0 [,) +oo ) -> ran S C_ ( 0 [,) +oo ) )
110	108, 109	syl 17	. . . . . . 7 |- ( ph -> ran S C_ ( 0 [,) +oo ) )
111	110, 27	syl6ss 3615	. . . . . 6 |- ( ph -> ran S C_ RR )
112	111	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN ) -> ran S C_ RR )
113		ffn 6045	. . . . . . . 8 |- ( S : NN --> ( 0 [,) +oo ) -> S Fn NN )
114	108, 113	syl 17	. . . . . . 7 |- ( ph -> S Fn NN )
115	114	adantr 481	. . . . . 6 |- ( ( ph /\ k e. NN ) -> S Fn NN )
116		fnfvelrn 6356	. . . . . 6 |- ( ( S Fn NN /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran S )
117	115, 61, 116	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran S )
118	112, 117	sseldd 3604	. . . 4 |- ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. RR )
119		eqid 2622	. . . . . . . . . 10 |- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
120		ovolun.t	. . . . . . . . . 10 |- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
121	119, 120	ovolsf 23241	. . . . . . . . 9 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
122	7, 121	syl 17	. . . . . . . 8 |- ( ph -> T : NN --> ( 0 [,) +oo ) )
123		frn 6053	. . . . . . . 8 |- ( T : NN --> ( 0 [,) +oo ) -> ran T C_ ( 0 [,) +oo ) )
124	122, 123	syl 17	. . . . . . 7 |- ( ph -> ran T C_ ( 0 [,) +oo ) )
125	124, 27	syl6ss 3615	. . . . . 6 |- ( ph -> ran T C_ RR )
126	125	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN ) -> ran T C_ RR )
127		ffn 6045	. . . . . . . 8 |- ( T : NN --> ( 0 [,) +oo ) -> T Fn NN )
128	122, 127	syl 17	. . . . . . 7 |- ( ph -> T Fn NN )
129	128	adantr 481	. . . . . 6 |- ( ( ph /\ k e. NN ) -> T Fn NN )
130		fnfvelrn 6356	. . . . . 6 |- ( ( T Fn NN /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran T )
131	129, 61, 130	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran T )
132	126, 131	sseldd 3604	. . . 4 |- ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. RR )
133	72	rehalfcld 11279	. . . . . 6 |- ( ph -> ( C / 2 ) e. RR )
134	67, 133	readdcld 10069	. . . . 5 |- ( ph -> ( ( vol* ` A ) + ( C / 2 ) ) e. RR )
135	134	adantr 481	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( vol* ` A ) + ( C / 2 ) ) e. RR )
136	69, 133	readdcld 10069	. . . . 5 |- ( ph -> ( ( vol* ` B ) + ( C / 2 ) ) e. RR )
137	136	adantr 481	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( vol* ` B ) + ( C / 2 ) ) e. RR )
138		ressxr 10083	. . . . . . . . 9 |- RR C_ RR*
139	111, 138	syl6ss 3615	. . . . . . . 8 |- ( ph -> ran S C_ RR* )
140		supxrcl 12145	. . . . . . . 8 |- ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
141	139, 140	syl 17	. . . . . . 7 |- ( ph -> sup ( ran S , RR* , < ) e. RR* )
142		1nn 11031	. . . . . . . . . . 11 |- 1 e. NN
143		fdm 6051	. . . . . . . . . . . 12 |- ( S : NN --> ( 0 [,) +oo ) -> dom S = NN )
144	108, 143	syl 17	. . . . . . . . . . 11 |- ( ph -> dom S = NN )
145	142, 144	syl5eleqr 2708	. . . . . . . . . 10 |- ( ph -> 1 e. dom S )
146		ne0i 3921	. . . . . . . . . 10 |- ( 1 e. dom S -> dom S =/= (/) )
147	145, 146	syl 17	. . . . . . . . 9 |- ( ph -> dom S =/= (/) )
148		dm0rn0 5342	. . . . . . . . . 10 |- ( dom S = (/) <-> ran S = (/) )
149	148	necon3bii 2846	. . . . . . . . 9 |- ( dom S =/= (/) <-> ran S =/= (/) )
150	147, 149	sylib 208	. . . . . . . 8 |- ( ph -> ran S =/= (/) )
151		supxrgtmnf 12159	. . . . . . . 8 |- ( ( ran S C_ RR /\ ran S =/= (/) ) -> -oo < sup ( ran S , RR* , < ) )
152	111, 150, 151	syl2anc 693	. . . . . . 7 |- ( ph -> -oo < sup ( ran S , RR* , < ) )
153		ovolun.f3	. . . . . . 7 |- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
154		xrre 12000	. . . . . . 7 |- ( ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` A ) + ( C / 2 ) ) e. RR ) /\ ( -oo < sup ( ran S , RR* , < ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) ) -> sup ( ran S , RR* , < ) e. RR )
155	141, 134, 152, 153, 154	syl22anc 1327	. . . . . 6 |- ( ph -> sup ( ran S , RR* , < ) e. RR )
156	155	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN ) -> sup ( ran S , RR* , < ) e. RR )
157	139	adantr 481	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ran S C_ RR* )
158		supxrub 12154	. . . . . 6 |- ( ( ran S C_ RR* /\ ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran S ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran S , RR* , < ) )
159	157, 117, 158	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran S , RR* , < ) )
160	153	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
161	118, 156, 135, 159, 160	letrd 10194	. . . 4 |- ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
162	125, 138	syl6ss 3615	. . . . . . . 8 |- ( ph -> ran T C_ RR* )
163		supxrcl 12145	. . . . . . . 8 |- ( ran T C_ RR* -> sup ( ran T , RR* , < ) e. RR* )
164	162, 163	syl 17	. . . . . . 7 |- ( ph -> sup ( ran T , RR* , < ) e. RR* )
165		fdm 6051	. . . . . . . . . . . 12 |- ( T : NN --> ( 0 [,) +oo ) -> dom T = NN )
166	122, 165	syl 17	. . . . . . . . . . 11 |- ( ph -> dom T = NN )
167	142, 166	syl5eleqr 2708	. . . . . . . . . 10 |- ( ph -> 1 e. dom T )
168		ne0i 3921	. . . . . . . . . 10 |- ( 1 e. dom T -> dom T =/= (/) )
169	167, 168	syl 17	. . . . . . . . 9 |- ( ph -> dom T =/= (/) )
170		dm0rn0 5342	. . . . . . . . . 10 |- ( dom T = (/) <-> ran T = (/) )
171	170	necon3bii 2846	. . . . . . . . 9 |- ( dom T =/= (/) <-> ran T =/= (/) )
172	169, 171	sylib 208	. . . . . . . 8 |- ( ph -> ran T =/= (/) )
173		supxrgtmnf 12159	. . . . . . . 8 |- ( ( ran T C_ RR /\ ran T =/= (/) ) -> -oo < sup ( ran T , RR* , < ) )
174	125, 172, 173	syl2anc 693	. . . . . . 7 |- ( ph -> -oo < sup ( ran T , RR* , < ) )
175		ovolun.g3	. . . . . . 7 |- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
176		xrre 12000	. . . . . . 7 |- ( ( ( sup ( ran T , RR* , < ) e. RR* /\ ( ( vol* ` B ) + ( C / 2 ) ) e. RR ) /\ ( -oo < sup ( ran T , RR* , < ) /\ sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) -> sup ( ran T , RR* , < ) e. RR )
177	164, 136, 174, 175, 176	syl22anc 1327	. . . . . 6 |- ( ph -> sup ( ran T , RR* , < ) e. RR )
178	177	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN ) -> sup ( ran T , RR* , < ) e. RR )
179	162	adantr 481	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ran T C_ RR* )
180		supxrub 12154	. . . . . 6 |- ( ( ran T C_ RR* /\ ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran T ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran T , RR* , < ) )
181	179, 131, 180	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran T , RR* , < ) )
182	175	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN ) -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
183	132, 178, 137, 181, 182	letrd 10194	. . . 4 |- ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
184	118, 132, 135, 137, 161, 183	le2addd 10646	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) <_ ( ( ( vol* ` A ) + ( C / 2 ) ) + ( ( vol* ` B ) + ( C / 2 ) ) ) )
185		oveq2 6658	. . . . . . . . 9 |- ( z = 1 -> ( 2 x. z ) = ( 2 x. 1 ) )
186	185	fveq2d 6195	. . . . . . . 8 |- ( z = 1 -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. 1 ) ) )
187		fveq2 6191	. . . . . . . . 9 |- ( z = 1 -> ( S ` z ) = ( S ` 1 ) )
188		fveq2 6191	. . . . . . . . 9 |- ( z = 1 -> ( T ` z ) = ( T ` 1 ) )
189	187, 188	oveq12d 6668	. . . . . . . 8 |- ( z = 1 -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) )
190	186, 189	eqeq12d 2637	. . . . . . 7 |- ( z = 1 -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. 1 ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) ) )
191	190	imbi2d 330	. . . . . 6 |- ( z = 1 -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. 1 ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) ) ) )
192		oveq2 6658	. . . . . . . . 9 |- ( z = k -> ( 2 x. z ) = ( 2 x. k ) )
193	192	fveq2d 6195	. . . . . . . 8 |- ( z = k -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. k ) ) )
194		fveq2 6191	. . . . . . . . 9 |- ( z = k -> ( S ` z ) = ( S ` k ) )
195		fveq2 6191	. . . . . . . . 9 |- ( z = k -> ( T ` z ) = ( T ` k ) )
196	194, 195	oveq12d 6668	. . . . . . . 8 |- ( z = k -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` k ) + ( T ` k ) ) )
197	193, 196	eqeq12d 2637	. . . . . . 7 |- ( z = k -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) ) )
198	197	imbi2d 330	. . . . . 6 |- ( z = k -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) ) ) )
199		oveq2 6658	. . . . . . . . 9 |- ( z = ( k + 1 ) -> ( 2 x. z ) = ( 2 x. ( k + 1 ) ) )
200	199	fveq2d 6195	. . . . . . . 8 |- ( z = ( k + 1 ) -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. ( k + 1 ) ) ) )
201		fveq2 6191	. . . . . . . . 9 |- ( z = ( k + 1 ) -> ( S ` z ) = ( S ` ( k + 1 ) ) )
202		fveq2 6191	. . . . . . . . 9 |- ( z = ( k + 1 ) -> ( T ` z ) = ( T ` ( k + 1 ) ) )
203	201, 202	oveq12d 6668	. . . . . . . 8 |- ( z = ( k + 1 ) -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) )
204	200, 203	eqeq12d 2637	. . . . . . 7 |- ( z = ( k + 1 ) -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) )
205	204	imbi2d 330	. . . . . 6 |- ( z = ( k + 1 ) -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) ) )
206		oveq2 6658	. . . . . . . . 9 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( 2 x. z ) = ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
207	206	fveq2d 6195	. . . . . . . 8 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
208		fveq2 6191	. . . . . . . . 9 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( S ` z ) = ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
209		fveq2 6191	. . . . . . . . 9 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( T ` z ) = ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
210	208, 209	oveq12d 6668	. . . . . . . 8 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
211	207, 210	eqeq12d 2637	. . . . . . 7 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) )
212	211	imbi2d 330	. . . . . 6 |- ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) ) )
213	24	fveq1i 6192	. . . . . . . 8 |- ( U ` ( 2 x. 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. 1 ) )
214	23	ovolfsval 23239	. . . . . . . . . . . 12 |- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. H ) ` 1 ) = ( ( 2nd ` ( H ` 1 ) ) - ( 1st ` ( H ` 1 ) ) ) )
215	22, 142, 214	sylancl 694	. . . . . . . . . . 11 |- ( ph -> ( ( ( abs o. - ) o. H ) ` 1 ) = ( ( 2nd ` ( H ` 1 ) ) - ( 1st ` ( H ` 1 ) ) ) )
216		halfnz 11455	. . . . . . . . . . . . . . . . . 18 |- -. ( 1 / 2 ) e. ZZ
217		nnz 11399	. . . . . . . . . . . . . . . . . . 19 |- ( ( n / 2 ) e. NN -> ( n / 2 ) e. ZZ )
218		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n / 2 ) = ( 1 / 2 ) )
219	218	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( ( n / 2 ) e. ZZ <-> ( 1 / 2 ) e. ZZ ) )
220	217, 219	syl5ib 234	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( ( n / 2 ) e. NN -> ( 1 / 2 ) e. ZZ ) )
221	216, 220	mtoi 190	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> -. ( n / 2 ) e. NN )
222	221	iffalsed 4097	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( F ` ( ( n + 1 ) / 2 ) ) )
223		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n + 1 ) = ( 1 + 1 ) )
224		df-2 11079	. . . . . . . . . . . . . . . . . . . 20 |- 2 = ( 1 + 1 )
225	223, 224	syl6eqr 2674	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n + 1 ) = 2 )
226	225	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( ( n + 1 ) / 2 ) = ( 2 / 2 ) )
227		2div2e1 11150	. . . . . . . . . . . . . . . . . 18 |- ( 2 / 2 ) = 1
228	226, 227	syl6eq 2672	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( ( n + 1 ) / 2 ) = 1 )
229	228	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` 1 ) )
230	222, 229	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( n = 1 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( F ` 1 ) )
231		fvex 6201	. . . . . . . . . . . . . . 15 |- ( F ` 1 ) e. _V
232	230, 21, 231	fvmpt 6282	. . . . . . . . . . . . . 14 |- ( 1 e. NN -> ( H ` 1 ) = ( F ` 1 ) )
233	142, 232	ax-mp 5	. . . . . . . . . . . . 13 |- ( H ` 1 ) = ( F ` 1 )
234	233	fveq2i 6194	. . . . . . . . . . . 12 |- ( 2nd ` ( H ` 1 ) ) = ( 2nd ` ( F ` 1 ) )
235	233	fveq2i 6194	. . . . . . . . . . . 12 |- ( 1st ` ( H ` 1 ) ) = ( 1st ` ( F ` 1 ) )
236	234, 235	oveq12i 6662	. . . . . . . . . . 11 |- ( ( 2nd ` ( H ` 1 ) ) - ( 1st ` ( H ` 1 ) ) ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) )
237	215, 236	syl6eq 2672	. . . . . . . . . 10 |- ( ph -> ( ( ( abs o. - ) o. H ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
238	56, 237	seq1i 12815	. . . . . . . . 9 |- ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
239		2t1e2 11176	. . . . . . . . . . 11 |- ( 2 x. 1 ) = 2
240	239	fveq2i 6194	. . . . . . . . . 10 |- ( ( ( abs o. - ) o. H ) ` ( 2 x. 1 ) ) = ( ( ( abs o. - ) o. H ) ` 2 )
241	23	ovolfsval 23239	. . . . . . . . . . . 12 |- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ 2 e. NN ) -> ( ( ( abs o. - ) o. H ) ` 2 ) = ( ( 2nd ` ( H ` 2 ) ) - ( 1st ` ( H ` 2 ) ) ) )
242	22, 31, 241	sylancl 694	. . . . . . . . . . 11 |- ( ph -> ( ( ( abs o. - ) o. H ) ` 2 ) = ( ( 2nd ` ( H ` 2 ) ) - ( 1st ` ( H ` 2 ) ) ) )
243		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 |- ( n = 2 -> ( n / 2 ) = ( 2 / 2 ) )
244	243, 227	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( n = 2 -> ( n / 2 ) = 1 )
245	244, 142	syl6eqel 2709	. . . . . . . . . . . . . . . . 17 |- ( n = 2 -> ( n / 2 ) e. NN )
246	245	iftrued 4094	. . . . . . . . . . . . . . . 16 |- ( n = 2 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( G ` ( n / 2 ) ) )
247	244	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( n = 2 -> ( G ` ( n / 2 ) ) = ( G ` 1 ) )
248	246, 247	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( n = 2 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( G ` 1 ) )
249		fvex 6201	. . . . . . . . . . . . . . 15 |- ( G ` 1 ) e. _V
250	248, 21, 249	fvmpt 6282	. . . . . . . . . . . . . 14 |- ( 2 e. NN -> ( H ` 2 ) = ( G ` 1 ) )
251	31, 250	ax-mp 5	. . . . . . . . . . . . 13 |- ( H ` 2 ) = ( G ` 1 )
252	251	fveq2i 6194	. . . . . . . . . . . 12 |- ( 2nd ` ( H ` 2 ) ) = ( 2nd ` ( G ` 1 ) )
253	251	fveq2i 6194	. . . . . . . . . . . 12 |- ( 1st ` ( H ` 2 ) ) = ( 1st ` ( G ` 1 ) )
254	252, 253	oveq12i 6662	. . . . . . . . . . 11 |- ( ( 2nd ` ( H ` 2 ) ) - ( 1st ` ( H ` 2 ) ) ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) )
255	242, 254	syl6eq 2672	. . . . . . . . . 10 |- ( ph -> ( ( ( abs o. - ) o. H ) ` 2 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
256	240, 255	syl5eq 2668	. . . . . . . . 9 |- ( ph -> ( ( ( abs o. - ) o. H ) ` ( 2 x. 1 ) ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
257	76, 142, 38, 238, 256	seqp1i 12817	. . . . . . . 8 |- ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. 1 ) ) = ( ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) + ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) ) )
258	213, 257	syl5eq 2668	. . . . . . 7 |- ( ph -> ( U ` ( 2 x. 1 ) ) = ( ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) + ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) ) )
259	106	fveq1i 6192	. . . . . . . . 9 |- ( S ` 1 ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` 1 )
260	105	ovolfsval 23239	. . . . . . . . . . 11 |- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. F ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
261	16, 142, 260	sylancl 694	. . . . . . . . . 10 |- ( ph -> ( ( ( abs o. - ) o. F ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
262	56, 261	seq1i 12815	. . . . . . . . 9 |- ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
263	259, 262	syl5eq 2668	. . . . . . . 8 |- ( ph -> ( S ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
264	120	fveq1i 6192	. . . . . . . . 9 |- ( T ` 1 ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 )
265	119	ovolfsval 23239	. . . . . . . . . . 11 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
266	7, 142, 265	sylancl 694	. . . . . . . . . 10 |- ( ph -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
267	56, 266	seq1i 12815	. . . . . . . . 9 |- ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
268	264, 267	syl5eq 2668	. . . . . . . 8 |- ( ph -> ( T ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
269	263, 268	oveq12d 6668	. . . . . . 7 |- ( ph -> ( ( S ` 1 ) + ( T ` 1 ) ) = ( ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) + ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) ) )
270	258, 269	eqtr4d 2659	. . . . . 6 |- ( ph -> ( U ` ( 2 x. 1 ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) )
271		oveq1 6657	. . . . . . . . 9 |- ( ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) -> ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
272	38	oveq2i 6661	. . . . . . . . . . . . 13 |- ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( ( 2 x. k ) + ( 1 + 1 ) )
273		2cnd 11093	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> 2 e. CC )
274	42	recnd 10068	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> k e. CC )
275		1cnd 10056	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> 1 e. CC )
276	273, 274, 275	adddid 10064	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
277		nnmulcl 11043	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. NN /\ k e. NN ) -> ( 2 x. k ) e. NN )
278	31, 277	mpan 706	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( 2 x. k ) e. NN )
279	278	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( 2 x. k ) e. NN )
280	279	nncnd 11036	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( 2 x. k ) e. CC )
281	280, 275, 275	addassd 10062	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( ( ( 2 x. k ) + 1 ) + 1 ) = ( ( 2 x. k ) + ( 1 + 1 ) ) )
282	272, 276, 281	3eqtr4a 2682	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) = ( ( ( 2 x. k ) + 1 ) + 1 ) )
283	282	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( U ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) )
284	24	fveq1i 6192	. . . . . . . . . . . 12 |- ( U ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) )
285	279	peano2nnd 11037	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. NN )
286	285, 76	syl6eleq 2711	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 1 ) )
287		seqp1 12816	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) + ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) )
288	286, 287	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) + ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) )
289	279, 76	syl6eleq 2711	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( 2 x. k ) e. ( ZZ>= ` 1 ) )
290		seqp1 12816	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. k ) e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) ) )
291	289, 290	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) ) )
292	24	fveq1i 6192	. . . . . . . . . . . . . . . . 17 |- ( U ` ( 2 x. k ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) )
293	292	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) )
294		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( ( 2 x. k ) + 1 ) -> ( n / 2 ) = ( ( ( 2 x. k ) + 1 ) / 2 ) )
295	294	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = ( ( 2 x. k ) + 1 ) -> ( ( n / 2 ) e. NN <-> ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN ) )
296	294	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = ( ( 2 x. k ) + 1 ) -> ( G ` ( n / 2 ) ) = ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) )
297		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = ( ( 2 x. k ) + 1 ) -> ( n + 1 ) = ( ( ( 2 x. k ) + 1 ) + 1 ) )
298	297	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( ( 2 x. k ) + 1 ) -> ( ( n + 1 ) / 2 ) = ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) )
299	298	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = ( ( 2 x. k ) + 1 ) -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) )
300	295, 296, 299	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( ( 2 x. k ) + 1 ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) )
301		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) e. _V
302		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) e. _V
303	301, 302	ifex 4156	. . . . . . . . . . . . . . . . . . . . . 22 |- if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) e. _V
304	300, 21, 303	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2 x. k ) + 1 ) e. NN -> ( H ` ( ( 2 x. k ) + 1 ) ) = if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) )
305	285, 304	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> ( H ` ( ( 2 x. k ) + 1 ) ) = if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) )
306		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 =/= 0
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> 2 =/= 0 )
308	274, 273, 307	divcan3d 10806	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) / 2 ) = k )
309	308, 75	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) / 2 ) e. NN )
310		nneo 11461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 x. k ) e. NN -> ( ( ( 2 x. k ) / 2 ) e. NN <-> -. ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN ) )
311	279, 310	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( ( ( 2 x. k ) / 2 ) e. NN <-> -. ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN ) )
312	309, 311	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> -. ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN )
313	312	iffalsed 4097	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) = ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) )
314	282	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) )
315	33	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. CC )
316		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 e. CC
317		divcan3 10711	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( k + 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( k + 1 ) )
318	316, 306, 317	mp3an23 1416	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k + 1 ) e. CC -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( k + 1 ) )
319	315, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( k + 1 ) )
320	314, 319	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) = ( k + 1 ) )
321	320	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) = ( F ` ( k + 1 ) ) )
322	305, 313, 321	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( H ` ( ( 2 x. k ) + 1 ) ) = ( F ` ( k + 1 ) ) )
323	322	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) = ( 2nd ` ( F ` ( k + 1 ) ) ) )
324	322	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) = ( 1st ` ( F ` ( k + 1 ) ) ) )
325	323, 324	oveq12d 6668	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) - ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) ) = ( ( 2nd ` ( F ` ( k + 1 ) ) ) - ( 1st ` ( F ` ( k + 1 ) ) ) ) )
326	22	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
327	23	ovolfsval 23239	. . . . . . . . . . . . . . . . . 18 |- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( ( 2 x. k ) + 1 ) e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) - ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) ) )
328	326, 285, 327	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) - ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) ) )
329	105	ovolfsval 23239	. . . . . . . . . . . . . . . . . 18 |- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) = ( ( 2nd ` ( F ` ( k + 1 ) ) ) - ( 1st ` ( F ` ( k + 1 ) ) ) ) )
330	16, 32, 329	syl2an 494	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) = ( ( 2nd ` ( F ` ( k + 1 ) ) ) - ( 1st ` ( F ` ( k + 1 ) ) ) ) )
331	325, 328, 330	3eqtr4rd 2667	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) = ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) )
332	293, 331	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) ) )
333	291, 332	eqtr4d 2659	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) = ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
334	282	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( H ` ( 2 x. ( k + 1 ) ) ) = ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) )
335	285	peano2nnd 11037	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> ( ( ( 2 x. k ) + 1 ) + 1 ) e. NN )
336	282, 335	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) e. NN )
337		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = ( 2 x. ( k + 1 ) ) -> ( n / 2 ) = ( ( 2 x. ( k + 1 ) ) / 2 ) )
338	337	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( 2 x. ( k + 1 ) ) -> ( ( n / 2 ) e. NN <-> ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN ) )
339	337	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( 2 x. ( k + 1 ) ) -> ( G ` ( n / 2 ) ) = ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) )
340		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( 2 x. ( k + 1 ) ) -> ( n + 1 ) = ( ( 2 x. ( k + 1 ) ) + 1 ) )
341	340	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = ( 2 x. ( k + 1 ) ) -> ( ( n + 1 ) / 2 ) = ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) )
342	341	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( 2 x. ( k + 1 ) ) -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) )
343	338, 339, 342	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = ( 2 x. ( k + 1 ) ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) )
344		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) e. _V
345		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) e. _V
346	344, 345	ifex 4156	. . . . . . . . . . . . . . . . . . . . 21 |- if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) e. _V
347	343, 21, 346	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. ( k + 1 ) ) e. NN -> ( H ` ( 2 x. ( k + 1 ) ) ) = if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) )
348	336, 347	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( H ` ( 2 x. ( k + 1 ) ) ) = if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) )
349	319, 33	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN )
350	349	iftrued 4094	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) = ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) )
351	319	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) = ( G ` ( k + 1 ) ) )
352	348, 350, 351	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( H ` ( 2 x. ( k + 1 ) ) ) = ( G ` ( k + 1 ) ) )
353	334, 352	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( G ` ( k + 1 ) ) )
354	353	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) = ( 2nd ` ( G ` ( k + 1 ) ) ) )
355	353	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) = ( 1st ` ( G ` ( k + 1 ) ) ) )
356	354, 355	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) - ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) ) = ( ( 2nd ` ( G ` ( k + 1 ) ) ) - ( 1st ` ( G ` ( k + 1 ) ) ) ) )
357	23	ovolfsval 23239	. . . . . . . . . . . . . . . 16 |- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( ( ( 2 x. k ) + 1 ) + 1 ) e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) - ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) ) )
358	326, 335, 357	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) - ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) ) )
359	119	ovolfsval 23239	. . . . . . . . . . . . . . . 16 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) = ( ( 2nd ` ( G ` ( k + 1 ) ) ) - ( 1st ` ( G ` ( k + 1 ) ) ) ) )
360	7, 32, 359	syl2an 494	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) = ( ( 2nd ` ( G ` ( k + 1 ) ) ) - ( 1st ` ( G ` ( k + 1 ) ) ) ) )
361	356, 358, 360	3eqtr4d 2666	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) )
362	333, 361	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) + ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) = ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
363	288, 362	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
364	284, 363	syl5eq 2668	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( U ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
365		ffvelrn 6357	. . . . . . . . . . . . . . 15 |- ( ( U : NN --> ( 0 [,) +oo ) /\ ( 2 x. k ) e. NN ) -> ( U ` ( 2 x. k ) ) e. ( 0 [,) +oo ) )
366	26, 278, 365	syl2an 494	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) e. ( 0 [,) +oo ) )
367	27, 366	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) e. RR )
368	367	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) e. CC )
369	105	ovolfsf 23240	. . . . . . . . . . . . . . . 16 |- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
370	16, 369	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
371		ffvelrn 6357	. . . . . . . . . . . . . . 15 |- ( ( ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
372	370, 32, 371	syl2an 494	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
373	27, 372	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. RR )
374	373	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. CC )
375	119	ovolfsf 23240	. . . . . . . . . . . . . . . 16 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
376	7, 375	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
377		ffvelrn 6357	. . . . . . . . . . . . . . 15 |- ( ( ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
378	376, 32, 377	syl2an 494	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
379	27, 378	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. RR )
380	379	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. CC )
381	368, 374, 380	addassd 10062	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) = ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
382	283, 364, 381	3eqtrd 2660	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
383		seqp1 12816	. . . . . . . . . . . . . 14 |- ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
384	77, 383	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
385	106	fveq1i 6192	. . . . . . . . . . . . 13 |- ( S ` ( k + 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` ( k + 1 ) )
386	106	fveq1i 6192	. . . . . . . . . . . . . 14 |- ( S ` k ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k )
387	386	oveq1i 6660	. . . . . . . . . . . . 13 |- ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) )
388	384, 385, 387	3eqtr4g 2681	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( S ` ( k + 1 ) ) = ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
389		seqp1 12816	. . . . . . . . . . . . . 14 |- ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
390	77, 389	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
391	120	fveq1i 6192	. . . . . . . . . . . . 13 |- ( T ` ( k + 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( k + 1 ) )
392	120	fveq1i 6192	. . . . . . . . . . . . . 14 |- ( T ` k ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k )
393	392	oveq1i 6660	. . . . . . . . . . . . 13 |- ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) )
394	390, 391, 393	3eqtr4g 2681	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( T ` ( k + 1 ) ) = ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
395	388, 394	oveq12d 6668	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) = ( ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
396	108	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( S ` k ) e. ( 0 [,) +oo ) )
397	27, 396	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( S ` k ) e. RR )
398	397	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( S ` k ) e. CC )
399	122	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( T ` k ) e. ( 0 [,) +oo ) )
400	27, 399	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( T ` k ) e. RR )
401	400	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( T ` k ) e. CC )
402	398, 374, 401, 380	add4d 10264	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
403	395, 402	eqtrd 2656	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
404	382, 403	eqeq12d 2637	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> ( ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) <-> ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) ) )
405	271, 404	syl5ibr 236	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) )
406	405	expcom 451	. . . . . . 7 |- ( k e. NN -> ( ph -> ( ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) ) )
407	406	a2d 29	. . . . . 6 |- ( k e. NN -> ( ( ph -> ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) ) -> ( ph -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) ) )
408	191, 198, 205, 212, 270, 407	nnind 11038	. . . . 5 |- ( ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN -> ( ph -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) )
409	408	impcom 446	. . . 4 |- ( ( ph /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
410	61, 409	syldan 487	. . 3 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
411	67	adantr 481	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( vol* ` A ) e. RR )
412	411	recnd 10068	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( vol* ` A ) e. CC )
413	72	adantr 481	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> C e. RR )
414	413	rehalfcld 11279	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( C / 2 ) e. RR )
415	414	recnd 10068	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( C / 2 ) e. CC )
416	69	adantr 481	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( vol* ` B ) e. RR )
417	416	recnd 10068	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( vol* ` B ) e. CC )
418	412, 415, 417, 415	add4d 10264	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( C / 2 ) ) + ( ( vol* ` B ) + ( C / 2 ) ) ) = ( ( ( vol* ` A ) + ( vol* ` B ) ) + ( ( C / 2 ) + ( C / 2 ) ) ) )
419	413	recnd 10068	. . . . . 6 |- ( ( ph /\ k e. NN ) -> C e. CC )
420	419	2halvesd 11278	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( ( C / 2 ) + ( C / 2 ) ) = C )
421	420	oveq2d 6666	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + ( ( C / 2 ) + ( C / 2 ) ) ) = ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
422	418, 421	eqtr2d 2657	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) = ( ( ( vol* ` A ) + ( C / 2 ) ) + ( ( vol* ` B ) + ( C / 2 ) ) ) )
423	184, 410, 422	3brtr4d 4685	. 2 |- ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
424	30, 65, 74, 104, 423	letrd 10194	1 |- ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   U.cuni 4436   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   o. ccom 5118   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   2c2 11070   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   (,)cioo 12175   [,)cico 12177   ...cfz 12326   |_cfl 12591   seqcseq 12801   abscabs 13974   vol*covol 23231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fl 12593  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976

This theorem is referenced by:  ovolunlem1  23265