Theorem itg2addnclem 31420

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 2402	. . 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 22319	. 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 7860	. . 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 11318	. . . . 5 |- < Or RR*
6	5	a1i 11	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> < Or RR* )
7		simprr 758	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
8		itg1cl 22276	. . . . . . . . . 10 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
9	8	rexrd 9593	. . . . . . . . 9 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR* )
10	9	adantr 463	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
11	7, 10	eqeltrd 2490	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
12	11	rexlimiva 2891	. . . . . 6 |- ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* )
13	12	abssi 3513	. . . . 5 |- { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
14		supxrcl 11477	. . . . 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 5804	. . . . . . . . . . . . . . . 16 |- ( g = f -> ( g ` z ) = ( f ` z ) )
17	16	eqeq1d 2404	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) = 0 <-> ( f ` z ) = 0 ) )
18	16	oveq1d 6249	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) + y ) = ( ( f ` z ) + y ) )
19	17, 18	ifbieq2d 3909	. . . . . . . . . . . . . 14 |- ( g = f -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
20	19	mpteq2dv 4481	. . . . . . . . . . . . 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 4404	. . . . . . . . . . . 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 2917	. . . . . . . . . . 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 5805	. . . . . . . . . . . 12 |- ( g = f -> ( S.1 ` g ) = ( S.1 ` f ) )
24	23	eqeq2d 2416	. . . . . . . . . . 11 |- ( g = f -> ( x = ( S.1 ` g ) <-> x = ( S.1 ` f ) ) )
25	22, 24	anbi12d 709	. . . . . . . . . 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 3034	. . . . . . . . 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 4398	. . . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . 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 10586	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 0
31	29, 30	syl6eqbr 4431	. . . . . . . . . . . . . . . . . 18 |- ( ( f ` z ) = 0 -> ( f ` z ) <_ 0 )
32	31	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( f ` z ) <_ 0 )
33		rpge0 11195	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. RR+ -> 0 <_ y )
34	33	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ y )
35		i1ff 22267	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f e. dom S.1 -> f : RR --> RR )
36	35	ffvelrnda 5965	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ z e. RR ) -> ( f ` z ) e. RR )
37	36	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
38		rpre 11189	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. RR+ -> y e. RR )
39	38	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
40	37, 39	addge01d 10100	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . 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 3919	. . . . . . . . . . . . . . . 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 716	. . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> f : RR --> RR )
46	45	ffvelrnda 5965	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
47	46	rexrd 9593	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR* )
48		0re 9546	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
49	38	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
50	46, 49	readdcld 9573	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( f ` z ) + y ) e. RR )
51		ifcl 3926	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. RR /\ ( ( f ` z ) + y ) e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR )
52	48, 50, 51	sylancr 661	. . . . . . . . . . . . . . . . 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 9593	. . . . . . . . . . . . . . . 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 11578	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
55		fss 5678	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : RR --> RR* )
56	54, 55	mpan2 669	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> RR* )
57	56	ad2antrr 724	. . . . . . . . . . . . . . . . 17 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> F : RR --> RR* )
58	57	ffvelrnda 5965	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. RR* )
59		xrletr 11332	. . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . 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 2811	. . . . . . . . . . . . 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 9533	. . . . . . . . . . . . . . 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 2403	. . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . 15 |- ( F : RR --> ( 0 [,] +oo ) -> F = ( z e. RR |-> ( F ` z ) ) )
68	67	ad2antrr 724	. . . . . . . . . . . . . 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 6495	. . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . 15 |- ( f e. dom S.1 -> f = ( z e. RR |-> ( f ` z ) ) )
71	70	ad2antlr 725	. . . . . . . . . . . . . 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 6495	. . . . . . . . . . . . 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 2895	. . . . . . . . . . 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 562	. . . . . . . . . 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 2878	. . . . . . . . 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 3511	. . . . . . 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 3440	. . . . . 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 1026	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
81	9	3ad2ant2 1019	. . . . . . . . . . 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 2490	. . . . . . . . . 10 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
83	82	rexlimdv3a 2897	. . . . . . . . 9 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* ) )
84	83	abssdv 3512	. . . . . . . 8 |- ( F : RR --> ( 0 [,] +oo ) -> { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* )
85		xrsupss 11471	. . . . . . . 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 7872	. . . . . 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 42	. . . . 5 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) 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 427	. . . 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 11488	. . . . . . . 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 668	. . . . . . 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 464	. . . . . 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 767	. . . . . . . . . . . . . . 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 4406	. . . . . . . . . . . . . 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 760	. . . . . . . . . . . . . . . . 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 22278	. . . . . . . . . . . . . . . . . . 19 |- ( RR X. { 0 } ) e. dom S.1
97		2rp 11188	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR+
98	97	ne0ii 3744	. . . . . . . . . . . . . . . . . . . 20 |- RR+ =/= (/)
99		ffvelrn 5963	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( F ` z ) e. ( 0 [,] +oo ) )
100		elxrge0 11600	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F ` z ) e. ( 0 [,] +oo ) <-> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
101	99, 100	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
102	101	simprd 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 <_ ( F ` z ) )
103	102	ralrimiva 2817	. . . . . . . . . . . . . . . . . . . . . 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 9540	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. _V
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 e. _V )
107		eqidd 2403	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
108	104, 106, 99, 107, 67	ofrfval2 6495	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
109	103, 108	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) oR <_ F )
110	109	ralrimivw 2818	. . . . . . . . . . . . . . . . . . . 20 |- ( F : RR --> ( 0 [,] +oo ) -> A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
111		r19.2z 3861	. . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
113		fveq2 5805	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
114		itg10 22279	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
115	113, 114	syl6req 2460	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
116	115	biantrud 505	. . . . . . . . . . . . . . . . . . . . 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 5804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
118	105	fvconst2 6063	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
119	117, 118	sylan9eq 2463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
120		iftrue 3890	. . . . . . . . . . . . . . . . . . . . . . . . 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 4480	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) = ( z e. RR |-> 0 ) )
123	122	breq1d 4404	. . . . . . . . . . . . . . . . . . . . . 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 2917	. . . . . . . . . . . . . . . . . . . . 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 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 ) )
126	125	rspcev 3159	. . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . 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 11304	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR -> -oo < 0 )
130	48, 129	mp1i 13	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> -oo < 0 )
131	128, 130	eqbrtrd 4414	. . . . . . . . . . . . . . . . . 18 |- ( b = -oo -> b < 0 )
132		eqeq1 2406	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( a = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
133	132	anbi2d 702	. . . . . . . . . . . . . . . . . . . . 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 2917	. . . . . . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( b < a <-> b < 0 ) )
136	134, 135	anbi12d 709	. . . . . . . . . . . . . . . . . . 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 3150	. . . . . . . . . . . . . . . . . 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 475	. . . . . . . . . . . . . . . . 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 469	. . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
142	141	ad3antlr 729	. . . . . . . . . . . . . . . . . 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 761	. . . . . . . . . . . . . . . . . . 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 11339	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b e. RR* -> ( b = -oo <-> -. -oo < b ) )
145	144	biimprd 223	. . . . . . . . . . . . . . . . . . . . 21 |- ( b e. RR* -> ( -. -oo < b -> b = -oo ) )
146	145	necon1ad 2619	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. RR* -> ( b =/= -oo -> -oo < b ) )
147	146	imp 427	. . . . . . . . . . . . . . . . . . 19 |- ( ( b e. RR* /\ b =/= -oo ) -> -oo < b )
148	143, 147	sylan 469	. . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> b e. RR* )
150	9	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
151	149, 150	anim12i 564	. . . . . . . . . . . . . . . . . . . 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 11326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) -> ( b < ( S.1 ` f ) -> b <_ ( S.1 ` f ) ) )
153	152	imp 427	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
154	151, 153	sylan 469	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . 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 11341	. . . . . . . . . . . . . . . . . 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 1231	. . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . . . . 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 455	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> f e. dom S.1 )
162		cnvimass 5298	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( `' f " ( ran f \ { 0 } ) ) C_ dom f
163		fdm 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
166	165	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
167		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 )
168	163	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> RR = dom f )
169		ffun 5672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f : RR --> RR -> Fun f )
170		difpreima 5949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( `' f " ran f ) = dom f
173	172	difeq1i 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) )
174	171, 173	syl6eq 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) ) )
175	168, 174	difeq12d 3561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) )
176		cnvimass 5298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( `' f " { 0 } ) C_ dom f
177		dfss4 3683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' f " { 0 } ) C_ dom f <-> ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } ) )
178	176, 177	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } )
179	175, 178	syl6eq 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( `' f " { 0 } ) )
180	179	eleq2d 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) <-> z e. ( `' f " { 0 } ) ) )
181		ffn 5670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> f Fn RR )
182		fniniseg 5942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) <-> ( z e. RR /\ ( f ` z ) = 0 ) ) )
183		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( z e. RR /\ ( f ` z ) = 0 ) -> ( f ` z ) = 0 )
184	182, 183	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. dom S.1 /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
189	188	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . 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 22301	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
191	160, 190	sylan 469	. . . . . . . . . . . . . . . . . . . . . . 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 4418	. . . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> f e. dom S.1 )
195		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( b < ( S.1 ` f ) /\ b e. RR ) -> b e. RR )
196	194, 195	anim12i 564	. . . . . . . . . . . . . . . . . . . . . . . 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 5815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V
201	200, 105	ifex 3952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f e. dom S.1 -> f = ( u e. RR |-> ( f ` u ) ) )
204	203	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f = ( u e. RR |-> ( f ` u ) ) )
205		eqidd 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6494	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( f : RR --> RR -> ( `' f " ran f ) = RR )
209	208	difeq1d 3559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f : RR --> RR -> ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
210	171, 209	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
211	210	eleq2d 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> u e. RR )
215	214	biantrurd 506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u e. ( RR \ ( `' f " { 0 } ) ) <-> ( u e. RR /\ -. u e. ( `' f " { 0 } ) ) )
217	215, 216	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 } ) ) ) )
218	213, 217	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 } ) ) )
219	218	con2bid 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( f Fn RR -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
221	35, 181, 220	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f e. dom S.1 -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
222	221	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) )
224		oveq1 6241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = ( 0 - 0 ) )
225		0m0e0 10606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 0 - 0 ) = 0
226	224, 225	syl6eq 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = 0 )
227	226	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. RR /\ ( f ` u ) = 0 ) -> ( ( f ` u ) - 0 ) = 0 )
228	223, 227	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 ) )
229	228	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . . . . . . . . . . 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 752	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 9541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- 1 e. _V
237	236, 105	ifex 3952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( S.1 ` f ) e. RR /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
245	8, 244	sylan 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f e. dom S.1 /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
246	245	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( S.1 ` f ) - b ) e. RR )
247		2re 10566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 e. RR
248		i1fima 22269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) e. dom vol )
249		mblvol 22125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f e. dom S.1 /\ -. 0 e. ( ran f \ { 0 } ) ) -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
253	251, 252	mpan2 669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
254	250, 253	eqeltrrd 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f e. dom S.1 -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
255		remulcl 9527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
257	256	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 e. CC )
259	254	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. CC )
261		2ne0 10589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 22299	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2491	. . . . . . . . . . . . . . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> z e. ( `' f " ( ran f \ { 0 } ) ) ) )
283		fveq2 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u = z -> ( f ` u ) = ( f ` z ) )
284	283	oveq1d 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) e. _V
288	287, 105	ifex 3952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 0 <_ ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) )