Theorem itg2addnclem 28287

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 ) ) ) oR <_ 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 2433	. . 3 |- { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } = { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) }
2	1	itg2val 21048	. 2 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( { x | E. f e. dom S.1 ( f oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) }
4	3	supeq1i 7685	. . 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < )
5		xrltso 11106	. . . . 5 |- < Or RR*
6	5	a1i 11	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> < Or RR* )
7		simprr 749	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
8		itg1cl 21005	. . . . . . . . . 10 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
9	8	rexrd 9421	. . . . . . . . 9 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR* )
10	9	adantr 462	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
11	7, 10	eqeltrd 2507	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
12	11	rexlimiva 2826	. . . . . 6 |- ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* )
13	12	abssi 3415	. . . . 5 |- { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
14		supxrcl 11265	. . . . 5 |- ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* -> sup ( { x | E. f e. dom S.1 ( f oR <_ 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 oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR* )
16		fveq1 5678	. . . . . . . . . . . . . . . 16 |- ( g = f -> ( g ` z ) = ( f ` z ) )
17	16	eqeq1d 2441	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) = 0 <-> ( f ` z ) = 0 ) )
18	16	oveq1d 6095	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) + y ) = ( ( f ` z ) + y ) )
19	17, 18	ifbieq2d 3802	. . . . . . . . . . . . . 14 |- ( g = f -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
20	19	mpteq2dv 4367	. . . . . . . . . . . . 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 4290	. . . . . . . . . . . 12 |- ( g = f -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) oR <_ F ) )
22	21	rexbidv 2726	. . . . . . . . . . 11 |- ( g = f -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) oR <_ F ) )
23		fveq2 5679	. . . . . . . . . . . 12 |- ( g = f -> ( S.1 ` g ) = ( S.1 ` f ) )
24	23	eqeq2d 2444	. . . . . . . . . . 11 |- ( g = f -> ( x = ( S.1 ` g ) <-> x = ( S.1 ` f ) ) )
25	22, 24	anbi12d 703	. . . . . . . . . 10 |- ( g = f -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) <-> ( E. y e. RR+ ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) ) )
26	25	cbvrexv 2938	. . . . . . . . 9 |- ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) )
27		breq2 4284	. . . . . . . . . . . . . . . . 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 4284	. . . . . . . . . . . . . . . . 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 22	. . . . . . . . . . . . . . . . . . 19 |- ( ( f ` z ) = 0 -> ( f ` z ) = 0 )
30		0le0 10399	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 0
31	29, 30	syl6eqbr 4317	. . . . . . . . . . . . . . . . . 18 |- ( ( f ` z ) = 0 -> ( f ` z ) <_ 0 )
32	31	adantl 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( f ` z ) <_ 0 )
33		rpge0 10991	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. RR+ -> 0 <_ y )
34	33	ad2antlr 719	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ y )
35		i1ff 20996	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f e. dom S.1 -> f : RR --> RR )
36	35	ffvelrnda 5831	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ z e. RR ) -> ( f ` z ) e. RR )
37	36	adantlr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
38		rpre 10985	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. RR+ -> y e. RR )
39	38	ad2antlr 719	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
40	37, 39	addge01d 9915	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( 0 <_ y <-> ( f ` z ) <_ ( ( f ` z ) + y ) ) )
41	34, 40	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) <_ ( ( f ` z ) + y ) )
42	41	adantr 462	. . . . . . . . . . . . . . . . 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 3812	. . . . . . . . . . . . . . . 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 710	. . . . . . . . . . . . . . 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 719	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> f : RR --> RR )
46	45	ffvelrnda 5831	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
47	46	rexrd 9421	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR* )
48		0re 9374	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
49	38	ad2antlr 719	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
50	46, 49	readdcld 9401	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( f ` z ) + y ) e. RR )
51		ifcl 3819	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. RR /\ ( ( f ` z ) + y ) e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR )
52	48, 50, 51	sylancr 656	. . . . . . . . . . . . . . . . 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 9421	. . . . . . . . . . . . . . . 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 11366	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
55		fss 5555	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : RR --> RR* )
56	54, 55	mpan2 664	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> RR* )
57	56	ad2antrr 718	. . . . . . . . . . . . . . . . 17 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> F : RR --> RR* )
58	57	ffvelrnda 5831	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. RR* )
59		xrletr 11120	. . . . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . . . 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 668	. . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . 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 9361	. . . . . . . . . . . . . . 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 2434	. . . . . . . . . . . . . 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 22	. . . . . . . . . . . . . . . 16 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> ( 0 [,] +oo ) )
67	66	feqmptd 5732	. . . . . . . . . . . . . . 15 |- ( F : RR --> ( 0 [,] +oo ) -> F = ( z e. RR |-> ( F ` z ) ) )
68	67	ad2antrr 718	. . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . 13 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) oR <_ F <-> A. z e. RR if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) <_ ( F ` z ) ) )
70	35	feqmptd 5732	. . . . . . . . . . . . . . 15 |- ( f e. dom S.1 -> f = ( z e. RR |-> ( f ` z ) ) )
71	70	ad2antlr 719	. . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . 13 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( f oR <_ F <-> A. z e. RR ( f ` z ) <_ ( F ` z ) ) )
73	62, 69, 72	3imtr4d 268	. . . . . . . . . . . 12 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> ( ( z e. RR |-> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) ) oR <_ F -> f oR <_ F ) )
74	73	rexlimdva 2831	. . . . . . . . . . 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 ) ) ) oR <_ F -> f oR <_ F ) )
75	74	anim1d 559	. . . . . . . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) -> ( f oR <_ F /\ x = ( S.1 ` f ) ) ) )
76	75	reximdva 2818	. . . . . . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` f ) ) -> E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) ) )
77	26, 76	syl5bi 217	. . . . . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) -> E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) ) )
78	77	ss2abdv 3413	. . . . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } C_ { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } )
79	78	sseld 3343	. . . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } -> b e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } ) )
80		simp3r 1010	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
81	9	3ad2ant2 1003	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
82	80, 81	eqeltrd 2507	. . . . . . . . . 10 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
83	82	rexlimdv3a 2833	. . . . . . . . 9 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* ) )
84	83	abssdv 3414	. . . . . . . 8 |- ( F : RR --> ( 0 [,] +oo ) -> { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* )
85		xrsupss 11259	. . . . . . . 8 |- ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* -> E. a e. RR* ( A. b e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } -. a < b /\ A. b e. RR* ( b < a -> E. s e. { x | E. f e. dom S.1 ( f oR <_ 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 oR <_ F /\ x = ( S.1 ` f ) ) } -. a < b /\ A. b e. RR* ( b < a -> E. s e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } b < s ) ) )
87	6, 86	supub 7697	. . . . . 6 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } -> -. sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b ) )
88	79, 87	syld 44	. . . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } -> -. sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b ) )
89	88	imp 429	. . . 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 ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } ) -> -. sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b )
90		supxrlub 11276	. . . . . . . 8 |- ( ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* /\ b e. RR* ) -> ( b < sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) <-> E. s e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } b < s ) )
91	13, 90	mpan 663	. . . . . . 7 |- ( b e. RR* -> ( b < sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) <-> E. s e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } b < s ) )
92	91	adantl 463	. . . . . 6 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> ( b < sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) <-> E. s e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } b < s ) )
93		simprrr 757	. . . . . . . . . . . . . . 15 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> s = ( S.1 ` f ) )
94	93	breq2d 4292	. . . . . . . . . . . . . 14 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> ( b < s <-> b < ( S.1 ` f ) ) )
95		simplll 750	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> F : RR --> ( 0 [,] +oo ) )
96		i1f0 21007	. . . . . . . . . . . . . . . . . . 19 |- ( RR X. { 0 } ) e. dom S.1
97		2rp 10984	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR+
98		ne0i 3631	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 e. RR+ -> RR+ =/= (/) )
99	97, 98	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- RR+ =/= (/)
100		ffvelrn 5829	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( F ` z ) e. ( 0 [,] +oo ) )
101		elxrge0 11381	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F ` z ) e. ( 0 [,] +oo ) <-> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
102	100, 101	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
103	102	simprd 460	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 <_ ( F ` z ) )
104	103	ralrimiva 2789	. . . . . . . . . . . . . . . . . . . . . 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 9368	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. _V
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 e. _V )
108		eqidd 2434	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
109	105, 107, 100, 108, 67	ofrfval2 6326	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
110	104, 109	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) oR <_ F )
111	110	ralrimivw 2790	. . . . . . . . . . . . . . . . . . . 20 |- ( F : RR --> ( 0 [,] +oo ) -> A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
112		r19.2z 3757	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR+ =/= (/) /\ A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
113	99, 111, 112	sylancr 656	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
114		fveq2 5679	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
115		itg10 21008	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
116	114, 115	syl6req 2482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
117	116	biantrud 504	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = ( RR X. { 0 } ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) ) )
118		fveq1 5678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
119	106	fvconst2 5920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
120	118, 119	sylan9eq 2485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
121		iftrue 3785	. . . . . . . . . . . . . . . . . . . . . . . . 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 4366	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) = ( z e. RR |-> 0 ) )
124	123	breq1d 4290	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> ( z e. RR |-> 0 ) oR <_ F ) )
125	124	rexbidv 2726	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = ( RR X. { 0 } ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) )
126	117, 125	bitr3d 255	. . . . . . . . . . . . . . . . . . . 20 |- ( g = ( RR X. { 0 } ) -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) <-> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) )
127	126	rspcev 3062	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) )
128	96, 113, 127	sylancr 656	. . . . . . . . . . . . . . . . . 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 ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) )
129		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> b = -oo )
130		mnflt 11092	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR -> -oo < 0 )
131	48, 130	mp1i 12	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> -oo < 0 )
132	129, 131	eqbrtrd 4300	. . . . . . . . . . . . . . . . . 18 |- ( b = -oo -> b < 0 )
133		eqeq1 2439	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( a = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
134	133	anbi2d 696	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 0 -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) <-> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) ) )
135	134	rexbidv 2726	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ 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 ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) ) )
136		breq2 4284	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( b < a <-> b < 0 ) )
137	135, 136	anbi12d 703	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> ( ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ 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 ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) /\ b < 0 ) ) )
138	106, 137	spcev 3053	. . . . . . . . . . . . . . . . . 18 |- ( ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ 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 ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
139	128, 132, 138	syl2an 474	. . . . . . . . . . . . . . . . 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 ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
140	95, 139	sylan 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ 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 ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
141		simp-4r 759	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b e. RR* )
142	8	adantr 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
143	142	ad3antlr 723	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> ( S.1 ` f ) e. RR )
144		simpllr 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> b e. RR* )
145		ngtmnft 11127	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b e. RR* -> ( b = -oo <-> -. -oo < b ) )
146	145	biimprd 223	. . . . . . . . . . . . . . . . . . . . 21 |- ( b e. RR* -> ( -. -oo < b -> b = -oo ) )
147	146	necon1ad 2668	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. RR* -> ( b =/= -oo -> -oo < b ) )
148	147	imp 429	. . . . . . . . . . . . . . . . . . 19 |- ( ( b e. RR* /\ b =/= -oo ) -> -oo < b )
149	144, 148	sylan 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> -oo < b )
150		simpr 458	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> b e. RR* )
151	9	adantr 462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
152	150, 151	anim12i 561	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> ( b e. RR* /\ ( S.1 ` f ) e. RR* ) )
153		xrltle 11114	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) -> ( b < ( S.1 ` f ) -> b <_ ( S.1 ` f ) ) )
154	153	imp 429	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
155	152, 154	sylan 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
156	155	adantr 462	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b <_ ( S.1 ` f ) )
157		xrre 11129	. . . . . . . . . . . . . . . . . 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 1212	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b e. RR )
159	128	ad3antrrr 722	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ 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 ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) )
160		simplrl 752	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> b < ( S.1 ` f ) )
161		simplrl 752	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) -> f e. dom S.1 )
162		simpl 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> f e. dom S.1 )
163		cnvimass 5177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( `' f " ( ran f \ { 0 } ) ) C_ dom f
164		fdm 5551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3392	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
167	166	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
168		simpr 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 )
169	164	eqcomd 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> RR = dom f )
170		ffun 5549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f : RR --> RR -> Fun f )
171		difpreima 5819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( `' f " ran f ) = dom f
174	173	difeq1i 3458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) )
175	172, 174	syl6eq 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) ) )
176	169, 175	difeq12d 3463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) )
177		cnvimass 5177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( `' f " { 0 } ) C_ dom f
178		dfss4 3572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' f " { 0 } ) C_ dom f <-> ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } ) )
179	177, 178	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } )
180	176, 179	syl6eq 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( `' f " { 0 } ) )
181	180	eleq2d 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) <-> z e. ( `' f " { 0 } ) ) )
182		ffn 5547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> f Fn RR )
183		fniniseg 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) <-> ( z e. RR /\ ( f ` z ) = 0 ) ) )
184		simpr 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( z e. RR /\ ( f ` z ) = 0 ) -> ( f ` z ) = 0 )
185	183, 184	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. dom S.1 /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
190	189	adantlr 707	. . . . . . . . . . . . . . . . . . . . . . . . 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 21030	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
192	161, 191	sylan 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ 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 4304	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ 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 654	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ 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 ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
195		simprl 748	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> f e. dom S.1 )
196		simpr 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( b < ( S.1 ` f ) /\ b e. RR ) -> b e. RR )
197	195, 196	anim12i 561	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ 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 5689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V
202	201, 106	ifex 3846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f e. dom S.1 -> f = ( u e. RR |-> ( f ` u ) ) )
205	204	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f = ( u e. RR |-> ( f ` u ) ) )
206		eqidd 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f oF - ( 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 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( f : RR --> RR -> ( `' f " ran f ) = RR )
212	211	difeq1d 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f : RR --> RR -> ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
213	172, 212	eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
214	213	eleq2d 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> u e. RR )
218	217	biantrurd 505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u e. ( RR \ ( `' f " { 0 } ) ) <-> ( u e. RR /\ -. u e. ( `' f " { 0 } ) ) )
220	218, 219	syl6bbr 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( f Fn RR -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
224	35, 182, 223	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f e. dom S.1 -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
225	224	ad3antrrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = ( 0 - 0 ) )
228		0m0e0 10419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 0 - 0 ) = 0
229	227, 228	syl6eq 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = 0 )
230	229	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. RR /\ ( f ` u ) = 0 ) -> ( ( f ` u ) - 0 ) = 0 )
231	226, 230	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
232	231	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
233	232	ifeq2da 3808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
234	210, 233	syl5eq 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
235	234	mpteq2dva 4366	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
236	207, 235	eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f oF - ( 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 ) ) )
237		simpll 746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f e. dom S.1 )
238	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 )
239		1ex 9369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- 1 e. _V
240	239, 106	ifex 3846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) e. _V
241	240	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 )
242		fconstmpt 4869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
243	242	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 } ) ) ) ) ) ) )
244		eqidd 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
245	198, 238, 241, 243, 244	offval2 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) } ) oF 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 ) ) ) )
246		oveq2 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
247		oveq2 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
248	246, 247	ifsb 3790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
249		resubcl 9661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( S.1 ` f ) e. RR /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
250	8, 249	sylan 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f e. dom S.1 /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
251	250	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( S.1 ` f ) - b ) e. RR )
252		2re 10379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 e. RR
253		i1fima 20998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) e. dom vol )
254		mblvol 20855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( `' f " ( ran f \ { 0 } ) ) e. dom vol -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) )
255	253, 254	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) )
256		neldifsn 3990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- -. 0 e. ( ran f \ { 0 } )
257		i1fima2 20999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f e. dom S.1 /\ -. 0 e. ( ran f \ { 0 } ) ) -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
258	256, 257	mpan2 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
259	255, 258	eqeltrrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f e. dom S.1 -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
260		remulcl 9355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( 2 e. RR /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
261	252, 259, 260	sylancr 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
262	261	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
263		2cnd 10382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 e. CC )
264	259	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
265	264	recnd 9400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. CC )
266		2ne0 10402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 =/= 0
267	266	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 =/= 0 )
268		simpr 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 )
269	263, 265, 267, 268	mulne0d 9976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) =/= 0 )
270	251, 262, 269	redivcld 10147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
271	270	recnd 9400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
272	271	mulid1d 9391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
273	271	mul01d 9556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
274	272, 273	ifeq12d 3797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
275	248, 274	syl5eq 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
276	275	mpteq2dv 4367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
277	245, 276	eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) } ) oF 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 ) ) )
278		eqid 2433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
279	278	i1f1 21010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
280	253, 258, 279	syl2anc 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f e. dom S.1 -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) e. dom S.1 )
281	280	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
282	281, 270	i1fmulc 21023	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) } ) oF x. ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) ) e. dom S.1 )
283	277, 282	eqeltrrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
284		i1fsub 21028	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 oF - ( 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 )
285	237, 283, 284	syl2anc 654	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f oF - ( 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	236, 285	eqeltrrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
287		eleq1 2493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> z e. ( `' f " ( ran f \ { 0 } ) ) ) )
288		fveq2 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u = z -> ( f ` u ) = ( f ` z ) )
289	288	oveq1d 6095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) ) )
290		eqidd 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> 0 = 0 )
291	287, 289, 290	ifbieq12d 3804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
292		eqid 2433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
293		ovex 6105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) e. _V
294	293, 106	ifex 3846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) e. _V
295	291, 292, 294	fvmpt 5762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( z e. RR -> ( ( u e. RR |->