Theorem itg2addnclem 31986

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 2450	. . 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 22679	. 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 7958	. . 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 11437	. . . . 5 |- < Or RR*
6	5	a1i 11	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> < Or RR* )
7		simprr 765	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
8		itg1cl 22636	. . . . . . . . . 10 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
9	8	rexrd 9687	. . . . . . . . 9 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR* )
10	9	adantr 467	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
11	7, 10	eqeltrd 2528	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
12	11	rexlimiva 2874	. . . . . 6 |- ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* )
13	12	abssi 3503	. . . . 5 |- { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
14		supxrcl 11597	. . . . 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 13	. . . 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 5862	. . . . . . . . . . . . . . . 16 |- ( g = f -> ( g ` z ) = ( f ` z ) )
17	16	eqeq1d 2452	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) = 0 <-> ( f ` z ) = 0 ) )
18	16	oveq1d 6303	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) + y ) = ( ( f ` z ) + y ) )
19	17, 18	ifbieq2d 3905	. . . . . . . . . . . . . 14 |- ( g = f -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
20	19	mpteq2dv 4489	. . . . . . . . . . . . 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 4411	. . . . . . . . . . . 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 2900	. . . . . . . . . . 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 5863	. . . . . . . . . . . 12 |- ( g = f -> ( S.1 ` g ) = ( S.1 ` f ) )
24	23	eqeq2d 2460	. . . . . . . . . . 11 |- ( g = f -> ( x = ( S.1 ` g ) <-> x = ( S.1 ` f ) ) )
25	22, 24	anbi12d 716	. . . . . . . . . 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 3019	. . . . . . . . 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 4405	. . . . . . . . . . . . . . . . 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 4405	. . . . . . . . . . . . . . . . 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 10696	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 0
31	29, 30	syl6eqbr 4439	. . . . . . . . . . . . . . . . . 18 |- ( ( f ` z ) = 0 -> ( f ` z ) <_ 0 )
32	31	adantl 468	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( f ` z ) <_ 0 )
33		rpge0 11311	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. RR+ -> 0 <_ y )
34	33	ad2antlr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ y )
35		i1ff 22627	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f e. dom S.1 -> f : RR --> RR )
36	35	ffvelrnda 6020	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ z e. RR ) -> ( f ` z ) e. RR )
37	36	adantlr 720	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
38		rpre 11305	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. RR+ -> y e. RR )
39	38	ad2antlr 732	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
40	37, 39	addge01d 10198	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( 0 <_ y <-> ( f ` z ) <_ ( ( f ` z ) + y ) ) )
41	34, 40	mpbid 214	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) <_ ( ( f ` z ) + y ) )
42	41	adantr 467	. . . . . . . . . . . . . . . . 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 3915	. . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> f : RR --> RR )
46	45	ffvelrnda 6020	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
47	46	rexrd 9687	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR* )
48		0re 9640	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
49	38	ad2antlr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
50	46, 49	readdcld 9667	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( f ` z ) + y ) e. RR )
51		ifcl 3922	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. RR /\ ( ( f ` z ) + y ) e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR )
52	48, 50, 51	sylancr 668	. . . . . . . . . . . . . . . . 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 9687	. . . . . . . . . . . . . . . 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 11714	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
55		fss 5735	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : RR --> RR* )
56	54, 55	mpan2 676	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> RR* )
57	56	ad2antrr 731	. . . . . . . . . . . . . . . . 17 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> F : RR --> RR* )
58	57	ffvelrnda 6020	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. RR* )
59		xrletr 11452	. . . . . . . . . . . . . . . 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 1267	. . . . . . . . . . . . . . 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 680	. . . . . . . . . . . . . 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 2795	. . . . . . . . . . . . 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 9627	. . . . . . . . . . . . . . 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 2451	. . . . . . . . . . . . . 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 5916	. . . . . . . . . . . . . . 15 |- ( F : RR --> ( 0 [,] +oo ) -> F = ( z e. RR |-> ( F ` z ) ) )
68	67	ad2antrr 731	. . . . . . . . . . . . . 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 6546	. . . . . . . . . . . . 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 5916	. . . . . . . . . . . . . . 15 |- ( f e. dom S.1 -> f = ( z e. RR |-> ( f ` z ) ) )
71	70	ad2antlr 732	. . . . . . . . . . . . . 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 6546	. . . . . . . . . . . . 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 272	. . . . . . . . . . . 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 2878	. . . . . . . . . . 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 567	. . . . . . . . . 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 2861	. . . . . . . . 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 221	. . . . . . . 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 3501	. . . . . . 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 3430	. . . . . 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 1036	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
81	9	3ad2ant2 1029	. . . . . . . . . . 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 2528	. . . . . . . . . 10 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
83	82	rexlimdv3a 2880	. . . . . . . . 9 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* ) )
84	83	abssdv 3502	. . . . . . . 8 |- ( F : RR --> ( 0 [,] +oo ) -> { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* )
85		xrsupss 11591	. . . . . . . 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 17	. . . . . . 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 7970	. . . . . 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 45	. . . . 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 431	. . . 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 11608	. . . . . . . 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 675	. . . . . . 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 468	. . . . . 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 774	. . . . . . . . . . . . . . 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 4413	. . . . . . . . . . . . . 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 767	. . . . . . . . . . . . . . . . 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 22638	. . . . . . . . . . . . . . . . . . 19 |- ( RR X. { 0 } ) e. dom S.1
97		2rp 11304	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR+
98	97	ne0ii 3737	. . . . . . . . . . . . . . . . . . . 20 |- RR+ =/= (/)
99		ffvelrn 6018	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( F ` z ) e. ( 0 [,] +oo ) )
100		elxrge0 11738	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F ` z ) e. ( 0 [,] +oo ) <-> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
101	99, 100	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
102	101	simprd 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 <_ ( F ` z ) )
103	102	ralrimiva 2801	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> A. z e. RR 0 <_ ( F ` z ) )
104	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> RR e. _V )
105		c0ex 9634	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. _V
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 e. _V )
107		eqidd 2451	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
108	104, 106, 99, 107, 67	ofrfval2 6546	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
109	103, 108	mpbird 236	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) oR <_ F )
110	109	ralrimivw 2802	. . . . . . . . . . . . . . . . . . . 20 |- ( F : RR --> ( 0 [,] +oo ) -> A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
111		r19.2z 3857	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR+ =/= (/) /\ A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
112	98, 110, 111	sylancr 668	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
113		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
114		itg10 22639	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
115	113, 114	syl6req 2501	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
116	115	biantrud 510	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
117		fveq1 5862	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
118	105	fvconst2 6118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
119	117, 118	sylan9eq 2504	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
120		iftrue 3886	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` z ) = 0 -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = 0 )
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = 0 )
122	121	mpteq2dva 4488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) = ( z e. RR |-> 0 ) )
123	122	breq1d 4411	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> ( ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> ( z e. RR |-> 0 ) oR <_ F ) )
124	123	rexbidv 2900	. . . . . . . . . . . . . . . . . . . . 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 ) )
125	116, 124	bitr3d 259	. . . . . . . . . . . . . . . . . . . 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 ) )
126	125	rspcev 3149	. . . . . . . . . . . . . . . . . . 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 ) ) )
127	96, 112, 126	sylancr 668	. . . . . . . . . . . . . . . . . 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 ) ) )
128		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> b = -oo )
129		mnflt 11422	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR -> -oo < 0 )
130	48, 129	mp1i 13	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> -oo < 0 )
131	128, 130	eqbrtrd 4422	. . . . . . . . . . . . . . . . . 18 |- ( b = -oo -> b < 0 )
132		eqeq1 2454	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( a = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
133	132	anbi2d 709	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
134	133	rexbidv 2900	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
135		breq2 4405	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( b < a <-> b < 0 ) )
136	134, 135	anbi12d 716	. . . . . . . . . . . . . . . . . . 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 ) ) )
137	105, 136	spcev 3140	. . . . . . . . . . . . . . . . . 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 ) )
138	127, 131, 137	syl2an 480	. . . . . . . . . . . . . . . . 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 ) )
139	95, 138	sylan 474	. . . . . . . . . . . . . . . 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 ) )
140		simp-4r 776	. . . . . . . . . . . . . . . . . 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* )
141	8	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
142	141	ad3antlr 736	. . . . . . . . . . . . . . . . . 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 )
143		simpllr 768	. . . . . . . . . . . . . . . . . . 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* )
144		ngtmnft 11459	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b e. RR* -> ( b = -oo <-> -. -oo < b ) )
145	144	biimprd 227	. . . . . . . . . . . . . . . . . . . . 21 |- ( b e. RR* -> ( -. -oo < b -> b = -oo ) )
146	145	necon1ad 2640	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. RR* -> ( b =/= -oo -> -oo < b ) )
147	146	imp 431	. . . . . . . . . . . . . . . . . . 19 |- ( ( b e. RR* /\ b =/= -oo ) -> -oo < b )
148	143, 147	sylan 474	. . . . . . . . . . . . . . . . . 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 )
149		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> b e. RR* )
150	9	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
151	149, 150	anim12i 569	. . . . . . . . . . . . . . . . . . . 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* ) )
152		xrltle 11445	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) -> ( b < ( S.1 ` f ) -> b <_ ( S.1 ` f ) ) )
153	152	imp 431	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
154	151, 153	sylan 474	. . . . . . . . . . . . . . . . . . 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 ) )
155	154	adantr 467	. . . . . . . . . . . . . . . . . 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 ) )
156		xrre 11461	. . . . . . . . . . . . . . . . . 18 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR ) /\ ( -oo < b /\ b <_ ( S.1 ` f ) ) ) -> b e. RR )
157	140, 142, 148, 155, 156	syl22anc 1268	. . . . . . . . . . . . . . . . 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 )
158	127	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
159		simplrl 769	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
160		simplrl 769	. . . . . . . . . . . . . . . . . . . . . . . 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 )
161		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> f e. dom S.1 )
162		cnvimass 5187	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( `' f " ( ran f \ { 0 } ) ) C_ dom f
163		fdm 5731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : RR --> RR -> dom f = RR )
164	35, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f e. dom S.1 -> dom f = RR )
165	162, 164	syl5sseq 3479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
166	165	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
167		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 )
168	163	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> RR = dom f )
169		ffun 5729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f : RR --> RR -> Fun f )
170		difpreima 6006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( Fun f -> ( `' f " ( ran f \ { 0 } ) ) = ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) )
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) )
172		cnvimarndm 5188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( `' f " ran f ) = dom f
173	172	difeq1i 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) )
174	171, 173	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) ) )
175	168, 174	difeq12d 3551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) )
176		cnvimass 5187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( `' f " { 0 } ) C_ dom f
177		dfss4 3676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' f " { 0 } ) C_ dom f <-> ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } ) )
178	176, 177	mpbi 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } )
179	175, 178	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( `' f " { 0 } ) )
180	179	eleq2d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) <-> z e. ( `' f " { 0 } ) ) )
181		ffn 5726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> f Fn RR )
182		fniniseg 6001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) <-> ( z e. RR /\ ( f ` z ) = 0 ) ) )
183		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( z e. RR /\ ( f ` z ) = 0 ) -> ( f ` z ) = 0 )
184	182, 183	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) -> ( f ` z ) = 0 ) )
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( `' f " { 0 } ) -> ( f ` z ) = 0 ) )
186	180, 185	sylbid 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) -> ( f ` z ) = 0 ) )
187	35, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f e. dom S.1 -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) -> ( f ` z ) = 0 ) )
188	187	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. dom S.1 /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
189	188	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
190	161, 166, 167, 189	itg10a 22661	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
191	160, 190	sylan 474	. . . . . . . . . . . . . . . . . . . . . . 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 )
192	159, 191	breqtrd 4426	. . . . . . . . . . . . . . . . . . . . . 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 )
193	158, 192, 137	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 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 ) )
194		simprl 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> f e. dom S.1 )
195		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( b < ( S.1 ` f ) /\ b e. RR ) -> b e. RR )
196	194, 195	anim12i 569	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
197	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> RR e. _V )
198		fvex 5873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f ` u ) e. _V
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( f ` u ) e. _V )
200		ovex 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V
201	200, 105	ifex 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) e. _V
202	201	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 )
203	35	feqmptd 5916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f e. dom S.1 -> f = ( u e. RR |-> ( f ` u ) ) )
204	203	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f = ( u e. RR |-> ( f ` u ) ) )
205		eqidd 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
206	197, 199, 202, 204, 205	offval2 6545	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
207		ovif2 6371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
208	172, 163	syl5eq 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( f : RR --> RR -> ( `' f " ran f ) = RR )
209	208	difeq1d 3549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f : RR --> RR -> ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
210	171, 209	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
211	210	eleq2d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f : RR --> RR -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
212	35, 211	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
213	212	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
214		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> u e. RR )
215	214	biantrurd 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
216		eldif 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u e. ( RR \ ( `' f " { 0 } ) ) <-> ( u e. RR /\ -. u e. ( `' f " { 0 } ) ) )
217	215, 216	syl6bbr 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
218	213, 217	bitr4d 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
219	218	con2bid 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
220		fniniseg 6001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( f Fn RR -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
221	35, 181, 220	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f e. dom S.1 -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
222	221	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
223	219, 222	bitr3d 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224		oveq1 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = ( 0 - 0 ) )
225		0m0e0 10716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 0 - 0 ) = 0
226	224, 225	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = 0 )
227	226	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. RR /\ ( f ` u ) = 0 ) -> ( ( f ` u ) - 0 ) = 0 )
228	223, 227	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
229	228	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
230	229	ifeq2da 3911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
231	207, 230	syl5eq 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
232	231	mpteq2dva 4488	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
233	206, 232	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
234		simpll 759	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f e. dom S.1 )
235	200	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 )
236		1ex 9635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- 1 e. _V
237	236, 105	ifex 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) e. _V
238	237	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 )
239		fconstmpt 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
240	239	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 } ) ) ) ) ) ) )
241		eqidd 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
242	197, 235, 238, 240, 241	offval2 6545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
243		ovif2 6371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
244		resubcl 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( S.1 ` f ) e. RR /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
245	8, 244	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f e. dom S.1 /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
246	245	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( S.1 ` f ) - b ) e. RR )
247		2re 10676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 e. RR
248		i1fima 22629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) e. dom vol )
249		mblvol 22477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( `' f " ( ran f \ { 0 } ) ) e. dom vol -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) )
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) )
251		neldifsn 4098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- -. 0 e. ( ran f \ { 0 } )
252		i1fima2 22630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f e. dom S.1 /\ -. 0 e. ( ran f \ { 0 } ) ) -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
253	251, 252	mpan2 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
254	250, 253	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f e. dom S.1 -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
255		remulcl 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( 2 e. RR /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
256	247, 254, 255	sylancr 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
257	256	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
258		2cnd 10679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 e. CC )
259	254	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
260	259	recnd 9666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. CC )
261		2ne0 10699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 =/= 0
262	261	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 =/= 0 )
263		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 )
264	258, 260, 262, 263	mulne0d 10261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) =/= 0 )
265	246, 257, 264	redivcld 10432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
266	265	recnd 9666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
267	266	mulid1d 9657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
268	266	mul01d 9829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
269	267, 268	ifeq12d 3900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
270	243, 269	syl5eq 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
271	270	mpteq2dv 4489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
272	242, 271	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
273		eqid 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
274	273	i1f1 22641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
275	248, 253, 274	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f e. dom S.1 -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) e. dom S.1 )
276	275	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
277	276, 265	i1fmulc 22654	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
278	272, 277	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
279		i1fsub 22659	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
280	234, 278, 279	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
281	233, 280	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
282		eleq1 2516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> z e. ( `' f " ( ran f \ { 0 } ) ) ) )
283		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u = z -> ( f ` u ) = ( f ` z ) )
284	283	oveq1d 6303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) ) )
285	282, 284	ifbieq1d 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
286		eqid 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
287		ovex 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) e. _V
288	287, 105	ifex 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) e. _V
289	285, 286, 288	fvmpt 5946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( z e. RR -> ( ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) ` z ) = if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) )
290	289	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. RR -> ( 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 ) ) ` z ) <-> 0 <_ if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) )
291	290, 289	ifbieq1d 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z e. RR -> if ( 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 ) ) ` z ) , ( ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` u ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) ) ` z ) , 0 ) = if ( 0 <_ if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( 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 ) , 0 ) )
292		iftrue 3886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 0 <_ ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) )