Theorem itg2addnclem 26155

Description: An alternate expression for the S.2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.)

Hypothesis

Ref	Expression
itg2addnclem.1	|- L = { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) }

Assertion

Ref	Expression
itg2addnclem	|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( L , RR* , < ) )

Distinct variable group:   x, y, z, g, F

Allowed substitution hints:   L( x, y, z, g)

Proof of Theorem itg2addnclem

Dummy variables s u f a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2404	. . 3 |- { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } = { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) }
2	1	itg2val 19573	. 2 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) )
3		itg2addnclem.1	. . . 4 |- L = { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) }
4	3	supeq1i 7410	. . 3 |- sup ( L , RR* , < ) = sup ( { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) } , RR* , < )
5		xrltso 10690	. . . . 5 |- < Or RR*
6	5	a1i 11	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> < Or RR* )
7		simprr 734	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f o R <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
8		itg1cl 19530	. . . . . . . . . 10 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
9	8	rexrd 9090	. . . . . . . . 9 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR* )
10	9	adantr 452	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f o R <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
11	7, 10	eqeltrd 2478	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( f o R <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
12	11	rexlimiva 2785	. . . . . 6 |- ( E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* )
13	12	abssi 3378	. . . . 5 |- { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
14		supxrcl 10849	. . . . 5 |- ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR* -> sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR* )
15	13, 14	mp1i 12	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR* )
16		fveq1 5686	. . . . . . . . . . . . . . . 16 |- ( g = f -> ( g ` z ) = ( f ` z ) )
17	16	eqeq1d 2412	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) = 0 <-> ( f ` z ) = 0 ) )
18	16	oveq1d 6055	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) + y ) = ( ( f ` z ) + y ) )
19	17, 18	ifbieq2d 3719	. . . . . . . . . . . . . 14 |- ( g = f -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
20	19	mpteq2dv 4256	. . . . . . . . . . . . 13 |- ( g = f -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) = ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) )
21	20	breq1d 4182	. . . . . . . . . . . 12 |- ( g = f -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F <-> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F ) )
22	21	rexbidv 2687	. . . . . . . . . . 11 |- ( g = f -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F <-> E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F ) )
23		fveq2 5687	. . . . . . . . . . . 12 |- ( g = f -> ( S.1 ` g ) = ( S.1 ` f ) )
24	23	eqeq2d 2415	. . . . . . . . . . 11 |- ( g = f -> ( x = ( S.1 ` g ) <-> x = ( S.1 ` f ) ) )
25	22, 24	anbi12d 692	. . . . . . . . . 10 |- ( g = f -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) <-> ( E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) ) )
26	25	cbvrexv 2893	. . . . . . . . 9 |- ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) <-> E. f e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) )
27		breq2 4176	. . . . . . . . . . . . . . . . 17 |- ( 0 = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) -> ( ( f ` z ) <_ 0 <-> ( f ` z ) <_ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) )
28		breq2 4176	. . . . . . . . . . . . . . . . 17 |- ( ( ( f ` z ) + y ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) -> ( ( f ` z ) <_ ( ( f ` z ) + y ) <-> ( f ` z ) <_ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) )
29		id 20	. . . . . . . . . . . . . . . . . . 19 |- ( ( f ` z ) = 0 -> ( f ` z ) = 0 )
30		0le0 10037	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 0
31	29, 30	syl6eqbr 4209	. . . . . . . . . . . . . . . . . 18 |- ( ( f ` z ) = 0 -> ( f ` z ) <_ 0 )
32	31	adantl 453	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( f ` z ) <_ 0 )
33		rpge0 10580	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. RR+ -> 0 <_ y )
34	33	ad2antlr 708	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ y )
35		i1ff 19521	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f e. dom S.1 -> f : RR --> RR )
36	35	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ z e. RR ) -> ( f ` z ) e. RR )
37	36	adantlr 696	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
38		rpre 10574	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. RR+ -> y e. RR )
39	38	ad2antlr 708	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
40	37, 39	addge01d 9570	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( 0 <_ y <-> ( f ` z ) <_ ( ( f ` z ) + y ) ) )
41	34, 40	mpbid 202	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) <_ ( ( f ` z ) + y ) )
42	41	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) /\ -. ( f ` z ) = 0 ) -> ( f ` z ) <_ ( ( f ` z ) + y ) )
43	27, 28, 32, 42	ifbothda 3729	. . . . . . . . . . . . . . . 16 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) <_ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
44	43	adantlll 699	. . . . . . . . . . . . . . 15 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) <_ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
45	35	ad2antlr 708	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> f : RR --> RR )
46	45	ffvelrnda 5829	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
47	46	rexrd 9090	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR* )
48		0re 9047	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
49	38	ad2antlr 708	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
50	46, 49	readdcld 9071	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( f ` z ) + y ) e. RR )
51		ifcl 3735	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. RR /\ ( ( f ` z ) + y ) e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR )
52	48, 50, 51	sylancr 645	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR )
53	52	rexrd 9090	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR* )
54		iccssxr 10949	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
55		fss 5558	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : RR --> RR* )
56	54, 55	mpan2 653	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> RR* )
57	56	ad2antrr 707	. . . . . . . . . . . . . . . . 17 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> F : RR --> RR* )
58	57	ffvelrnda 5829	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. RR* )
59		xrletr 10704	. . . . . . . . . . . . . . . 16 |- ( ( ( f ` z ) e. RR* /\ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR* /\ ( F ` z ) e. RR* ) -> ( ( ( f ` z ) <_ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) /\ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) <_ ( F ` z ) ) -> ( f ` z ) <_ ( F ` z ) ) )
60	47, 53, 58, 59	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( ( f ` z ) <_ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) /\ if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) <_ ( F ` z ) ) -> ( f ` z ) <_ ( F ` z ) ) )
61	44, 60	mpand 657	. . . . . . . . . . . . . 14 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) <_ ( F ` z ) -> ( f ` z ) <_ ( F ` z ) ) )
62	61	ralimdva 2744	. . . . . . . . . . . . 13 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( A. z e. RR if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) <_ ( F ` z ) -> A. z e. RR ( f ` z ) <_ ( F ` z ) ) )
63		reex 9037	. . . . . . . . . . . . . . 15 |- RR e. _V
64	63	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> RR e. _V )
65		eqidd 2405	. . . . . . . . . . . . . 14 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) = ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) )
66		id 20	. . . . . . . . . . . . . . . 16 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> ( 0 [,] +oo ) )
67	66	feqmptd 5738	. . . . . . . . . . . . . . 15 |- ( F : RR --> ( 0 [,] +oo ) -> F = ( z e. RR |-> ( F ` z ) ) )
68	67	ad2antrr 707	. . . . . . . . . . . . . 14 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> F = ( z e. RR |-> ( F ` z ) ) )
69	64, 52, 58, 65, 68	ofrfval2 6282	. . . . . . . . . . . . 13 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F <-> A. z e. RR if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) <_ ( F ` z ) ) )
70	35	feqmptd 5738	. . . . . . . . . . . . . . 15 |- ( f e. dom S.1 -> f = ( z e. RR |-> ( f ` z ) ) )
71	70	ad2antlr 708	. . . . . . . . . . . . . 14 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> f = ( z e. RR |-> ( f ` z ) ) )
72	64, 46, 58, 71, 68	ofrfval2 6282	. . . . . . . . . . . . 13 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( f o R <_ F <-> A. z e. RR ( f ` z ) <_ ( F ` z ) ) )
73	62, 69, 72	3imtr4d 260	. . . . . . . . . . . 12 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F -> f o R <_ F ) )
74	73	rexlimdva 2790	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F -> f o R <_ F ) )
75	74	anim1d 548	. . . . . . . . . 10 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) -> ( f o R <_ F /\ x = ( S.1 ` f ) ) ) )
76	75	reximdva 2778	. . . . . . . . 9 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. f e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` f ) ) -> E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) ) )
77	26, 76	syl5bi 209	. . . . . . . 8 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) -> E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) ) )
78	77	ss2abdv 3376	. . . . . . 7 |- ( F : RR --> ( 0 [,] +oo ) -> { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) } C_ { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } )
79	78	sseld 3307	. . . . . 6 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) } -> b e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } ) )
80		simp3r 986	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f o R <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
81	9	3ad2ant2 979	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f o R <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
82	80, 81	eqeltrd 2478	. . . . . . . . . 10 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f o R <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
83	82	rexlimdv3a 2792	. . . . . . . . 9 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* ) )
84	83	abssdv 3377	. . . . . . . 8 |- ( F : RR --> ( 0 [,] +oo ) -> { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR* )
85		xrsupss 10843	. . . . . . . 8 |- ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR* -> E. a e. RR* ( A. b e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } -. a < b /\ A. b e. RR* ( b < a -> E. s e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } b < s ) ) )
86	84, 85	syl 16	. . . . . . 7 |- ( F : RR --> ( 0 [,] +oo ) -> E. a e. RR* ( A. b e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } -. a < b /\ A. b e. RR* ( b < a -> E. s e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } b < s ) ) )
87	6, 86	supub 7420	. . . . . 6 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } -> -. sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b ) )
88	79, 87	syld 42	. . . . 5 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) } -> -. sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b ) )
89	88	imp 419	. . . 4 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ x = ( S.1 ` g ) ) } ) -> -. sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b )
90		supxrlub 10860	. . . . . . . 8 |- ( ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } C_ RR* /\ b e. RR* ) -> ( b < sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) <-> E. s e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } b < s ) )
91	13, 90	mpan 652	. . . . . . 7 |- ( b e. RR* -> ( b < sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) <-> E. s e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } b < s ) )
92	91	adantl 453	. . . . . 6 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> ( b < sup ( { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) <-> E. s e. { x | E. f e. dom S.1 ( f o R <_ F /\ x = ( S.1 ` f ) ) } b < s ) )
93		simprrr 742	. . . . . . . . . . . . . . 15 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) -> s = ( S.1 ` f ) )
94	93	breq2d 4184	. . . . . . . . . . . . . 14 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) -> ( b < s <-> b < ( S.1 ` f ) ) )
95		simplll 735	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> F : RR --> ( 0 [,] +oo ) )
96		i1f0 19532	. . . . . . . . . . . . . . . . . . 19 |- ( RR X. { 0 } ) e. dom S.1
97		2rp 10573	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR+
98		ne0i 3594	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 e. RR+ -> RR+ =/= (/) )
99	97, 98	ax-mp 8	. . . . . . . . . . . . . . . . . . . 20 |- RR+ =/= (/)
100		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( F ` z ) e. ( 0 [,] +oo ) )
101		elxrge0 10964	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F ` z ) e. ( 0 [,] +oo ) <-> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
102	100, 101	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
103	102	simprd 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 <_ ( F ` z ) )
104	103	ralrimiva 2749	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> A. z e. RR 0 <_ ( F ` z ) )
105	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> RR e. _V )
106		c0ex 9041	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. _V
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 e. _V )
108		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
109	105, 107, 100, 108, 67	ofrfval2 6282	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> ( ( z e. RR |-> 0 ) o R <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
110	104, 109	mpbird 224	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) o R <_ F )
111	110	ralrimivw 2750	. . . . . . . . . . . . . . . . . . . 20 |- ( F : RR --> ( 0 [,] +oo ) -> A. y e. RR+ ( z e. RR |-> 0 ) o R <_ F )
112		r19.2z 3677	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR+ =/= (/) /\ A. y e. RR+ ( z e. RR |-> 0 ) o R <_ F ) -> E. y e. RR+ ( z e. RR |-> 0 ) o R <_ F )
113	99, 111, 112	sylancr 645	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> E. y e. RR+ ( z e. RR |-> 0 ) o R <_ F )
114		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
115		itg10 19533	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
116	114, 115	syl6req 2453	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
117	116	biantrud 494	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = ( RR X. { 0 } ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F <-> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) ) )
118		fveq1 5686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
119	106	fvconst2 5906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
120	118, 119	sylan9eq 2456	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
121		iftrue 3705	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` z ) = 0 -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = 0 )
122	120, 121	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = 0 )
123	122	mpteq2dva 4255	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) = ( z e. RR |-> 0 ) )
124	123	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F <-> ( z e. RR |-> 0 ) o R <_ F ) )
125	124	rexbidv 2687	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = ( RR X. { 0 } ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F <-> E. y e. RR+ ( z e. RR |-> 0 ) o R <_ F ) )
126	117, 125	bitr3d 247	. . . . . . . . . . . . . . . . . . . 20 |- ( g = ( RR X. { 0 } ) -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) <-> E. y e. RR+ ( z e. RR |-> 0 ) o R <_ F ) )
127	126	rspcev 3012	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. y e. RR+ ( z e. RR |-> 0 ) o R <_ F ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) )
128	96, 113, 127	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) )
129		id 20	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> b = -oo )
130		mnflt 10678	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR -> -oo < 0 )
131	48, 130	mp1i 12	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> -oo < 0 )
132	129, 131	eqbrtrd 4192	. . . . . . . . . . . . . . . . . 18 |- ( b = -oo -> b < 0 )
133		eqeq1 2410	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( a = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
134	133	anbi2d 685	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 0 -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) <-> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) ) )
135	134	rexbidv 2687	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) <-> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) ) )
136		breq2 4176	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( b < a <-> b < 0 ) )
137	135, 136	anbi12d 692	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> ( ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) <-> ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) /\ b < 0 ) ) )
138	106, 137	spcev 3003	. . . . . . . . . . . . . . . . . 18 |- ( ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) /\ b < 0 ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
139	128, 132, 138	syl2an 464	. . . . . . . . . . . . . . . . 17 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b = -oo ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
140	95, 139	sylan 458	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b = -oo ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
141		simp-4r 744	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b e. RR* )
142	8	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
143	142	ad3antlr 712	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> ( S.1 ` f ) e. RR )
144		simpllr 736	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> b e. RR* )
145		ngtmnft 10711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b e. RR* -> ( b = -oo <-> -. -oo < b ) )
146	145	biimprd 215	. . . . . . . . . . . . . . . . . . . . 21 |- ( b e. RR* -> ( -. -oo < b -> b = -oo ) )
147	146	necon1ad 2634	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. RR* -> ( b =/= -oo -> -oo < b ) )
148	147	imp 419	. . . . . . . . . . . . . . . . . . 19 |- ( ( b e. RR* /\ b =/= -oo ) -> -oo < b )
149	144, 148	sylan 458	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> -oo < b )
150		simpr 448	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> b e. RR* )
151	9	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
152	150, 151	anim12i 550	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) -> ( b e. RR* /\ ( S.1 ` f ) e. RR* ) )
153		xrltle 10698	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) -> ( b < ( S.1 ` f ) -> b <_ ( S.1 ` f ) ) )
154	153	imp 419	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
155	152, 154	sylan 458	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
156	155	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b <_ ( S.1 ` f ) )
157		xrre 10713	. . . . . . . . . . . . . . . . . 18 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR ) /\ ( -oo < b /\ b <_ ( S.1 ` f ) ) ) -> b e. RR )
158	141, 143, 149, 156, 157	syl22anc 1185	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b e. RR )
159	128	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ 0 = ( S.1 ` g ) ) )
160		simplrl 737	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> b < ( S.1 ` f ) )
161		simplrl 737	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) -> f e. dom S.1 )
162		simpl 444	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> f e. dom S.1 )
163		cnvimass 5183	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( `' f " ( ran f \ { 0 } ) ) C_ dom f
164		fdm 5554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : RR --> RR -> dom f = RR )
165	35, 164	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f e. dom S.1 -> dom f = RR )
166	163, 165	syl5sseq 3356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
167	166	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
168		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 )
169	164	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> RR = dom f )
170		ffun 5552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f : RR --> RR -> Fun f )
171		difpreima 5817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( Fun f -> ( `' f " ( ran f \ { 0 } ) ) = ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) )
172	170, 171	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) )
173		cnvimarndm 5184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( `' f " ran f ) = dom f
174	173	difeq1i 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) )
175	172, 174	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) ) )
176	169, 175	difeq12d 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) )
177		cnvimass 5183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( `' f " { 0 } ) C_ dom f
178		dfss4 3535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' f " { 0 } ) C_ dom f <-> ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } ) )
179	177, 178	mpbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } )
180	176, 179	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( `' f " { 0 } ) )
181	180	eleq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) <-> z e. ( `' f " { 0 } ) ) )
182		ffn 5550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> f Fn RR )
183		fniniseg 5810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) <-> ( z e. RR /\ ( f ` z ) = 0 ) ) )
184		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( z e. RR /\ ( f ` z ) = 0 ) -> ( f ` z ) = 0 )
185	183, 184	syl6bi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) -> ( f ` z ) = 0 ) )
186	182, 185	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( `' f " { 0 } ) -> ( f ` z ) = 0 ) )
187	181, 186	sylbid 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) -> ( f ` z ) = 0 ) )
188	35, 187	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f e. dom S.1 -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) -> ( f ` z ) = 0 ) )
189	188	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. dom S.1 /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
190	189	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( f e. dom S.1 /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
191	162, 167, 168, 190	itg10a 19555	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. dom S.1 /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
192	161, 191	sylan 458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
193	160, 192	breqtrd 4196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> b < 0 )
194	159, 193, 138	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) o R <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
195		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) -> f e. dom S.1 )
196		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( b < ( S.1 ` f ) /\ b e. RR ) -> b e. RR )
197	195, 196	anim12i 550	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f o R <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) -> ( f e. dom S.1 /\ b e. RR ) )
198	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> RR e. _V )
199		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f ` u ) e. _V
200	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( f ` u ) e. _V )
201		ovex 6065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V
202	201, 106	ifex 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) e. _V
203	202	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) e. _V )
204	35	feqmptd 5738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f e. dom S.1 -> f = ( u e. RR |-> ( f ` u ) ) )
205	204	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f = ( u e. RR |-> ( f ` u ) ) )
206		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) )
207	198, 200, 203, 205, 206	offval2 6281	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f o F - ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) = ( u e. RR |-> ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) )
208		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) = ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) -> ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) = ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) )
209		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) = 0 -> ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) = ( ( f ` u ) - 0 ) )
210	208, 209	ifsb 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) = if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , ( ( f ` u ) - 0 ) )
211	173, 164	syl5eq 2448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( f : RR --> RR -> ( `' f " ran f ) = RR )
212	211	difeq1d 3424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f : RR --> RR -> ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
213	172, 212	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
214	213	eleq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f : RR --> RR -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
215	35, 214	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
216	215	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
217		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> u e. RR )
218	217	biantrurd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( -. u e. ( `' f " { 0 } ) <-> ( u e. RR /\ -. u e. ( `' f " { 0 } ) ) ) )
219		eldif 3290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u e. ( RR \ ( `' f " { 0 } ) ) <-> ( u e. RR /\ -. u e. ( `' f " { 0 } ) ) )
220	218, 219	syl6bbr 255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( -. u e. ( `' f " { 0 } ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
221	216, 220	bitr4d 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> -. u e. ( `' f " { 0 } ) ) )
222	221	con2bid 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( u e. ( `' f " { 0 } ) <-> -. u e. ( `' f " ( ran f \ { 0 } ) ) ) )
223		fniniseg 5810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( f Fn RR -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
224	35, 182, 223	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f e. dom S.1 -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
225	224	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
226	222, 225	bitr3d 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( -. u e. ( `' f " ( ran f \ { 0 } ) ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
227		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = ( 0 - 0 ) )
228		0cn 9040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 0 e. CC
229	228	subidi 9327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 0 - 0 ) = 0
230	227, 229	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = 0 )
231	230	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. RR /\ ( f ` u ) = 0 ) -> ( ( f ` u ) - 0 ) = 0 )
232	226, 231	syl6bi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( -. u e. ( `' f " ( ran f \ { 0 } ) ) -> ( ( f ` u ) - 0 ) = 0 ) )
233	232	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) /\ -. u e. ( `' f " ( ran f \ { 0 } ) ) ) -> ( ( f ` u ) - 0 ) = 0 )
234	233	ifeq2da 3725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , ( ( f ` u ) - 0 ) ) = if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) )
235	210, 234	syl5eq 2448	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) = if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) )
236	235	mpteq2dva 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) )
237	207, 236	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f o F - ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) )
238		simpll 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f e. dom S.1 )
239	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V )
240		1ex 9042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- 1 e. _V
241	240, 106	ifex 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) e. _V
242	241	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) e. _V )
243		fconstmpt 4880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( RR X. { ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) } ) = ( u e. RR |-> ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) )
244	243	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( RR X. { ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) } ) = ( u e. RR |-> ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) )
245		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) )
246	198, 239, 242, 244, 245	offval2 6281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( RR X. { ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) } ) o F x. ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) ) = ( u e. RR |-> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) ) )
247		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) = 1 -> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) = ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 1 ) )
248		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) = 0 -> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) = ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 0 ) )
249	247, 248	ifsb 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) = if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 1 ) , ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 0 ) )
250		resubcl 9321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( S.1 ` f ) e. RR /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
251	8, 250	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f e. dom S.1 /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
252	251	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( S.1 ` f ) - b ) e. RR )
253		2re 10025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 e. RR
254		i1fima 19523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) e. dom vol )
255		mblvol 19379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( `' f " ( ran f \ { 0 } ) ) e. dom vol -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) )
256	254, 255	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) )
257		neldifsn 3889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- -. 0 e. ( ran f \ { 0 } )
258		i1fima2 19524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f e. dom S.1 /\ -. 0 e. ( ran f \ { 0 } ) ) -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
259	257, 258	mpan2 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
260	256, 259	eqeltrrd 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f e. dom S.1 -> ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
261		remulcl 9031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( 2 e. RR /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR ) -> ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
262	253, 260, 261	sylancr 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
263	262	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
264		2cn 10026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 e. CC
265	264	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 e. CC )
266	260	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
267	266	recnd 9070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) e. CC )
268		2ne0 10039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 =/= 0
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 =/= 0 )
270		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 )
271	265, 267, 269, 270	mulne0d 9630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) =/= 0 )
272	252, 263, 271	redivcld 9798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. RR )
273	272	recnd 9070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. CC )
274	273	mulid1d 9061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 1 ) = ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) )
275	273	mul01d 9221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 0 ) = 0 )
276	274, 275	ifeq12d 3715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 1 ) , ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. 0 ) ) = if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) )
277	249, 276	syl5eq 2448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) = if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) )
278	277	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> ( ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) x. if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) )
279	246, 278	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( RR X. { ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) } ) o F x. ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) )
280		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) )
281	280	i1f1 19535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( `' f " ( ran f \ { 0 } ) ) e. dom vol /\ ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) e. dom S.1 )
282	254, 259, 281	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f e. dom S.1 -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) e. dom S.1 )
283	282	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) e. dom S.1 )
284	283, 272	i1fmulc 19548	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( RR X. { ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) } ) o F x. ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) ) e. dom S.1 )
285	279, 284	eqeltrrd 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) e. dom S.1 )
286		i1fsub 19553	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f e. dom S.1 /\ ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) e. dom S.1 ) -> ( f o F - ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) e. dom S.1 )
287	238, 285, 286	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f o F - ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) e. dom S.1 )
288	237, 287	eqeltrrd 2479	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) e. dom S.1 )
289		eleq1 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> z e. ( `' f " ( ran f \ { 0 } ) ) ) )
290		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u = z -> ( f ` u ) = ( f ` z ) )
291	290	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) = ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) )
292		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> 0 = 0 )
293	289, 291, 292	ifbieq12d 3721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( u = z -> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) = if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) )
294		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) )
295		ovex 6065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) e. _V
296	295, 106	ifex 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol * ` ( `' f " ( ran f \ { 0 } ) ) ) ) )