Theorem itg2addnclem 28592

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 2454	. . 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 21340	. 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 7809	. . 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 11230	. . . . 5 |- < Or RR*
6	5	a1i 11	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> < Or RR* )
7		simprr 756	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
8		itg1cl 21297	. . . . . . . . . 10 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
9	8	rexrd 9545	. . . . . . . . 9 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR* )
10	9	adantr 465	. . . . . . . 8 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
11	7, 10	eqeltrd 2542	. . . . . . 7 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
12	11	rexlimiva 2942	. . . . . 6 |- ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* )
13	12	abssi 3536	. . . . 5 |- { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR*
14		supxrcl 11389	. . . . 5 |- ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* -> sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR* )
15	13, 14	mp1i 12	. . . 4 |- ( F : RR --> ( 0 [,] +oo ) -> sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) e. RR* )
16		fveq1 5799	. . . . . . . . . . . . . . . 16 |- ( g = f -> ( g ` z ) = ( f ` z ) )
17	16	eqeq1d 2456	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) = 0 <-> ( f ` z ) = 0 ) )
18	16	oveq1d 6216	. . . . . . . . . . . . . . 15 |- ( g = f -> ( ( g ` z ) + y ) = ( ( f ` z ) + y ) )
19	17, 18	ifbieq2d 3923	. . . . . . . . . . . . . 14 |- ( g = f -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) )
20	19	mpteq2dv 4488	. . . . . . . . . . . . 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 2868	. . . . . . . . . . 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 5800	. . . . . . . . . . . 12 |- ( g = f -> ( S.1 ` g ) = ( S.1 ` f ) )
24	23	eqeq2d 2468	. . . . . . . . . . 11 |- ( g = f -> ( x = ( S.1 ` g ) <-> x = ( S.1 ` f ) ) )
25	22, 24	anbi12d 710	. . . . . . . . . 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 3054	. . . . . . . . 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 10523	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 0
31	29, 30	syl6eqbr 4438	. . . . . . . . . . . . . . . . . 18 |- ( ( f ` z ) = 0 -> ( f ` z ) <_ 0 )
32	31	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) /\ ( f ` z ) = 0 ) -> ( f ` z ) <_ 0 )
33		rpge0 11115	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. RR+ -> 0 <_ y )
34	33	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> 0 <_ y )
35		i1ff 21288	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f e. dom S.1 -> f : RR --> RR )
36	35	ffvelrnda 5953	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ z e. RR ) -> ( f ` z ) e. RR )
37	36	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
38		rpre 11109	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. RR+ -> y e. RR )
39	38	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f e. dom S.1 /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
40	37, 39	addge01d 10039	. . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 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 3933	. . . . . . . . . . . . . . . 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 717	. . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> f : RR --> RR )
46	45	ffvelrnda 5953	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR )
47	46	rexrd 9545	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( f ` z ) e. RR* )
48		0re 9498	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
49	38	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> y e. RR )
50	46, 49	readdcld 9525	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( ( f ` z ) + y ) e. RR )
51		ifcl 3940	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. RR /\ ( ( f ` z ) + y ) e. RR ) -> if ( ( f ` z ) = 0 , 0 , ( ( f ` z ) + y ) ) e. RR )
52	48, 50, 51	sylancr 663	. . . . . . . . . . . . . . . . 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 9545	. . . . . . . . . . . . . . . 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 11490	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
55		fss 5676	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : RR --> RR* )
56	54, 55	mpan2 671	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> F : RR --> RR* )
57	56	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) -> F : RR --> RR* )
58	57	ffvelrnda 5953	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 ) /\ y e. RR+ ) /\ z e. RR ) -> ( F ` z ) e. RR* )
59		xrletr 11244	. . . . . . . . . . . . . . . 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 1219	. . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . 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 2832	. . . . . . . . . . . . 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 9485	. . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . 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 5854	. . . . . . . . . . . . . . 15 |- ( F : RR --> ( 0 [,] +oo ) -> F = ( z e. RR |-> ( F ` z ) ) )
68	67	ad2antrr 725	. . . . . . . . . . . . . 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 6448	. . . . . . . . . . . . 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 5854	. . . . . . . . . . . . . . 15 |- ( f e. dom S.1 -> f = ( z e. RR |-> ( f ` z ) ) )
71	70	ad2antlr 726	. . . . . . . . . . . . . 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 6448	. . . . . . . . . . . . 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 2947	. . . . . . . . . . 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 564	. . . . . . . . . 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 2934	. . . . . . . . 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 3534	. . . . . . 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 3464	. . . . . 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 1017	. . . . . . . . . . 11 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x = ( S.1 ` f ) )
81	9	3ad2ant2 1010	. . . . . . . . . . 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 2542	. . . . . . . . . 10 |- ( ( F : RR --> ( 0 [,] +oo ) /\ f e. dom S.1 /\ ( f oR <_ F /\ x = ( S.1 ` f ) ) ) -> x e. RR* )
83	82	rexlimdv3a 2949	. . . . . . . . 9 |- ( F : RR --> ( 0 [,] +oo ) -> ( E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) -> x e. RR* ) )
84	83	abssdv 3535	. . . . . . . 8 |- ( F : RR --> ( 0 [,] +oo ) -> { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* )
85		xrsupss 11383	. . . . . . . 8 |- ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } C_ RR* -> E. a e. RR* ( A. b e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } -. a < b /\ A. b e. RR* ( b < a -> E. s e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } b < s ) ) )
86	84, 85	syl 16	. . . . . . 7 |- ( F : RR --> ( 0 [,] +oo ) -> E. a e. RR* ( A. b e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } -. a < b /\ A. b e. RR* ( b < a -> E. s e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } b < s ) ) )
87	6, 86	supub 7821	. . . . . 6 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } -> -. sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b ) )
88	79, 87	syld 44	. . . . 5 |- ( F : RR --> ( 0 [,] +oo ) -> ( b e. { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } -> -. sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b ) )
89	88	imp 429	. . . 4 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. { x | E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ x = ( S.1 ` g ) ) } ) -> -. sup ( { x | E. f e. dom S.1 ( f oR <_ F /\ x = ( S.1 ` f ) ) } , RR* , < ) < b )
90		supxrlub 11400	. . . . . . . 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 670	. . . . . . 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 466	. . . . . 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 764	. . . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . . . . 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 21299	. . . . . . . . . . . . . . . . . . 19 |- ( RR X. { 0 } ) e. dom S.1
97		2rp 11108	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR+
98		ne0i 3752	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 e. RR+ -> RR+ =/= (/) )
99	97, 98	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- RR+ =/= (/)
100		ffvelrn 5951	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( F ` z ) e. ( 0 [,] +oo ) )
101		elxrge0 11512	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F ` z ) e. ( 0 [,] +oo ) <-> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
102	100, 101	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> ( ( F ` z ) e. RR* /\ 0 <_ ( F ` z ) ) )
103	102	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 <_ ( F ` z ) )
104	103	ralrimiva 2830	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> A. z e. RR 0 <_ ( F ` z ) )
105	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> RR e. _V )
106		c0ex 9492	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. _V
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F : RR --> ( 0 [,] +oo ) /\ z e. RR ) -> 0 e. _V )
108		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) = ( z e. RR |-> 0 ) )
109	105, 107, 100, 108, 67	ofrfval2 6448	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F : RR --> ( 0 [,] +oo ) -> ( ( z e. RR |-> 0 ) oR <_ F <-> A. z e. RR 0 <_ ( F ` z ) ) )
110	104, 109	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : RR --> ( 0 [,] +oo ) -> ( z e. RR |-> 0 ) oR <_ F )
111	110	ralrimivw 2831	. . . . . . . . . . . . . . . . . . . 20 |- ( F : RR --> ( 0 [,] +oo ) -> A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
112		r19.2z 3878	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR+ =/= (/) /\ A. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
113	99, 111, 112	sylancr 663	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F )
114		fveq2 5800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( S.1 ` g ) = ( S.1 ` ( RR X. { 0 } ) ) )
115		itg10 21300	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S.1 ` ( RR X. { 0 } ) ) = 0
116	114, 115	syl6req 2512	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = ( RR X. { 0 } ) -> 0 = ( S.1 ` g ) )
117	116	biantrud 507	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = ( RR X. { 0 } ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) ) )
118		fveq1 5799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g = ( RR X. { 0 } ) -> ( g ` z ) = ( ( RR X. { 0 } ) ` z ) )
119	106	fvconst2 6043	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. RR -> ( ( RR X. { 0 } ) ` z ) = 0 )
120	118, 119	sylan9eq 2515	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> ( g ` z ) = 0 )
121		iftrue 3906	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` z ) = 0 -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = 0 )
122	120, 121	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g = ( RR X. { 0 } ) /\ z e. RR ) -> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) = 0 )
123	122	mpteq2dva 4487	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = ( RR X. { 0 } ) -> ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) = ( z e. RR |-> 0 ) )
124	123	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 ) )
125	124	rexbidv 2868	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = ( RR X. { 0 } ) -> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F <-> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) )
126	117, 125	bitr3d 255	. . . . . . . . . . . . . . . . . . . 20 |- ( g = ( RR X. { 0 } ) -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) <-> E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) )
127	126	rspcev 3179	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( RR X. { 0 } ) e. dom S.1 /\ E. y e. RR+ ( z e. RR |-> 0 ) oR <_ F ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) )
128	96, 113, 127	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,] +oo ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) )
129		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> b = -oo )
130		mnflt 11216	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR -> -oo < 0 )
131	48, 130	mp1i 12	. . . . . . . . . . . . . . . . . . 19 |- ( b = -oo -> -oo < 0 )
132	129, 131	eqbrtrd 4421	. . . . . . . . . . . . . . . . . 18 |- ( b = -oo -> b < 0 )
133		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( a = ( S.1 ` g ) <-> 0 = ( S.1 ` g ) ) )
134	133	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 0 -> ( ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) <-> ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) ) )
135	134	rexbidv 2868	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) <-> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) ) )
136		breq2 4405	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( b < a <-> b < 0 ) )
137	135, 136	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> ( ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) <-> ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) /\ b < 0 ) ) )
138	106, 137	spcev 3170	. . . . . . . . . . . . . . . . . 18 |- ( ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) /\ b < 0 ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
139	128, 132, 138	syl2an 477	. . . . . . . . . . . . . . . . 17 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b = -oo ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
140	95, 139	sylan 471	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b = -oo ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
141		simp-4r 766	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b e. RR* )
142	8	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR )
143	142	ad3antlr 730	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> ( S.1 ` f ) e. RR )
144		simpllr 758	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> b e. RR* )
145		ngtmnft 11251	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b e. RR* -> ( b = -oo <-> -. -oo < b ) )
146	145	biimprd 223	. . . . . . . . . . . . . . . . . . . . 21 |- ( b e. RR* -> ( -. -oo < b -> b = -oo ) )
147	146	necon1ad 2668	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. RR* -> ( b =/= -oo -> -oo < b ) )
148	147	imp 429	. . . . . . . . . . . . . . . . . . 19 |- ( ( b e. RR* /\ b =/= -oo ) -> -oo < b )
149	144, 148	sylan 471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> -oo < b )
150		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) -> b e. RR* )
151	9	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) -> ( S.1 ` f ) e. RR* )
152	150, 151	anim12i 566	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> ( b e. RR* /\ ( S.1 ` f ) e. RR* ) )
153		xrltle 11238	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) -> ( b < ( S.1 ` f ) -> b <_ ( S.1 ` f ) ) )
154	153	imp 429	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR* ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
155	152, 154	sylan 471	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) -> b <_ ( S.1 ` f ) )
156	155	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b <_ ( S.1 ` f ) )
157		xrre 11253	. . . . . . . . . . . . . . . . . 18 |- ( ( ( b e. RR* /\ ( S.1 ` f ) e. RR ) /\ ( -oo < b /\ b <_ ( S.1 ` f ) ) ) -> b e. RR )
158	141, 143, 149, 156, 157	syl22anc 1220	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ b e. RR* ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ b < ( S.1 ` f ) ) /\ b =/= -oo ) -> b e. RR )
159	128	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ 0 = ( S.1 ` g ) ) )
160		simplrl 759	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> b < ( S.1 ` f ) )
161		simplrl 759	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) -> f e. dom S.1 )
162		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> f e. dom S.1 )
163		cnvimass 5298	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( `' f " ( ran f \ { 0 } ) ) C_ dom f
164		fdm 5672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : RR --> RR -> dom f = RR )
165	35, 164	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f e. dom S.1 -> dom f = RR )
166	163, 165	syl5sseq 3513	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
167	166	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( `' f " ( ran f \ { 0 } ) ) C_ RR )
168		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 )
169	164	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> RR = dom f )
170		ffun 5670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f : RR --> RR -> Fun f )
171		difpreima 5941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( Fun f -> ( `' f " ( ran f \ { 0 } ) ) = ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) )
172	170, 171	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) )
173		cnvimarndm 5299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( `' f " ran f ) = dom f
174	173	difeq1i 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) )
175	172, 174	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( dom f \ ( `' f " { 0 } ) ) )
176	169, 175	difeq12d 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) )
177		cnvimass 5298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( `' f " { 0 } ) C_ dom f
178		dfss4 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' f " { 0 } ) C_ dom f <-> ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } ) )
179	177, 178	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( dom f \ ( dom f \ ( `' f " { 0 } ) ) ) = ( `' f " { 0 } )
180	176, 179	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) = ( `' f " { 0 } ) )
181	180	eleq2d 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) <-> z e. ( `' f " { 0 } ) ) )
182		ffn 5668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f : RR --> RR -> f Fn RR )
183		fniniseg 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) <-> ( z e. RR /\ ( f ` z ) = 0 ) ) )
184		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( z e. RR /\ ( f ` z ) = 0 ) -> ( f ` z ) = 0 )
185	183, 184	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f Fn RR -> ( z e. ( `' f " { 0 } ) -> ( f ` z ) = 0 ) )
186	182, 185	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f : RR --> RR -> ( z e. ( `' f " { 0 } ) -> ( f ` z ) = 0 ) )
187	181, 186	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : RR --> RR -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) -> ( f ` z ) = 0 ) )
188	35, 187	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f e. dom S.1 -> ( z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) -> ( f ` z ) = 0 ) )
189	188	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. dom S.1 /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
190	189	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) /\ z e. ( RR \ ( `' f " ( ran f \ { 0 } ) ) ) ) -> ( f ` z ) = 0 )
191	162, 167, 168, 190	itg10a 21322	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. dom S.1 /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
192	161, 191	sylan 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> ( S.1 ` f ) = 0 )
193	160, 192	breqtrd 4425	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> b < 0 )
194	159, 193, 138	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) = 0 ) -> E. a ( E. g e. dom S.1 ( E. y e. RR+ ( z e. RR |-> if ( ( g ` z ) = 0 , 0 , ( ( g ` z ) + y ) ) ) oR <_ F /\ a = ( S.1 ` g ) ) /\ b < a ) )
195		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) -> f e. dom S.1 )
196		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( b < ( S.1 ` f ) /\ b e. RR ) -> b e. RR )
197	195, 196	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( f e. dom S.1 /\ ( f oR <_ F /\ s = ( S.1 ` f ) ) ) ) /\ ( b < ( S.1 ` f ) /\ b e. RR ) ) -> ( f e. dom S.1 /\ b e. RR ) )
198	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> RR e. _V )
199		fvex 5810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f ` u ) e. _V
200	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( f ` u ) e. _V )
201		ovex 6226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V
202	201, 106	ifex 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) e. _V
203	202	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) e. _V )
204	35	feqmptd 5854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f e. dom S.1 -> f = ( u e. RR |-> ( f ` u ) ) )
205	204	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f = ( u e. RR |-> ( f ` u ) ) )
206		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) = ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) )
207	198, 200, 203, 205, 206	offval2 6447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( f oF - ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) = ( u e. RR |-> ( ( f ` u ) - if ( u e. ( `' f " ( ran f \ { 0 } ) ) , ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) , 0 ) ) ) )
208		ovif2 6279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
209	173, 164	syl5eq 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( f : RR --> RR -> ( `' f " ran f ) = RR )
210	209	difeq1d 3582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f : RR --> RR -> ( ( `' f " ran f ) \ ( `' f " { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
211	172, 210	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f : RR --> RR -> ( `' f " ( ran f \ { 0 } ) ) = ( RR \ ( `' f " { 0 } ) ) )
212	211	eleq2d 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f : RR --> RR -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
213	35, 212	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> u e. ( RR \ ( `' f " { 0 } ) ) ) )
214	213	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
215		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> u e. RR )
216	215	biantrurd 508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
217		eldif 3447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u e. ( RR \ ( `' f " { 0 } ) ) <-> ( u e. RR /\ -. u e. ( `' f " { 0 } ) ) )
218	216, 217	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 } ) ) ) )
219	214, 218	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 } ) ) )
220	219	con2bid 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( u e. ( `' f " { 0 } ) <-> -. u e. ( `' f " ( ran f \ { 0 } ) ) ) )
221		fniniseg 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( f Fn RR -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
222	35, 182, 221	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f e. dom S.1 -> ( u e. ( `' f " { 0 } ) <-> ( u e. RR /\ ( f ` u ) = 0 ) ) )
223	222	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224	220, 223	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 ) ) )
225		oveq1 6208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = ( 0 - 0 ) )
226		0m0e0 10543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 0 - 0 ) = 0
227	225, 226	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( f ` u ) = 0 -> ( ( f ` u ) - 0 ) = 0 )
228	227	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. RR /\ ( f ` u ) = 0 ) -> ( ( f ` u ) - 0 ) = 0 )
229	224, 228	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 ) )
230	229	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) /\ -. u e. ( `' f " ( ran f \ { 0 } ) ) ) -> ( ( f ` u ) - 0 ) = 0 )
231	230	ifeq2da 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
232	208, 231	syl5eq 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
233	232	mpteq2dva 4487	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
234	207, 233	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
235		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> f e. dom S.1 )
236	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) /\ u e. RR ) -> ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) e. _V )
237		1ex 9493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- 1 e. _V
238	237, 106	ifex 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) e. _V
239	238	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 )
240		fconstmpt 4991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
241	240	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 } ) ) ) ) ) ) )
242		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
243	198, 236, 239, 241, 242	offval2 6447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
244		ovif2 6279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
245		resubcl 9785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( S.1 ` f ) e. RR /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
246	8, 245	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f e. dom S.1 /\ b e. RR ) -> ( ( S.1 ` f ) - b ) e. RR )
247	246	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( ( S.1 ` f ) - b ) e. RR )
248		2re 10503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 e. RR
249		i1fima 21290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( f e. dom S.1 -> ( `' f " ( ran f \ { 0 } ) ) e. dom vol )
250		mblvol 21146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( `' f " ( ran f \ { 0 } ) ) e. dom vol -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) )
251	249, 250	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) = ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) )
252		neldifsn 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- -. 0 e. ( ran f \ { 0 } )
253		i1fima2 21291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f e. dom S.1 /\ -. 0 e. ( ran f \ { 0 } ) ) -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
254	252, 253	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( f e. dom S.1 -> ( vol ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
255	251, 254	eqeltrrd 2543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( f e. dom S.1 -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
256		remulcl 9479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( 2 e. RR /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
257	248, 255, 256	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( f e. dom S.1 -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
258	257	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) e. RR )
259		2cnd 10506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 e. CC )
260	255	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. RR )
261	260	recnd 9524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) e. CC )
262		2ne0 10526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- 2 =/= 0
263	262	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> 2 =/= 0 )
264		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 )
265	259, 261, 263, 264	mulne0d 10100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( f e. dom S.1 /\ b e. RR ) /\ ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) =/= 0 ) -> ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) =/= 0 )
266	247, 258, 265	redivcld 10271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
267	266	recnd 9524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
268	267	mulid1d 9515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
269	267	mul01d 9680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
270	268, 269	ifeq12d 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
271	244, 270	syl5eq 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
272	271	mpteq2dv 4488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
273	243, 272	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
274		eqid 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
275	274	i1f1 21302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
276	249, 254, 275	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f e. dom S.1 -> ( u e. RR |-> if ( u e. ( `' f " ( ran f \ { 0 } ) ) , 1 , 0 ) ) e. dom S.1 )
277	276	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
278	277, 266	i1fmulc 21315	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
279	273, 278	eqeltrrd 2543	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
280		i1fsub 21320	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
281	235, 279, 280	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
282	234, 281	eqeltrrd 2543	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
283		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u = z -> ( u e. ( `' f " ( ran f \ { 0 } ) ) <-> z e. ( `' f " ( ran f \ { 0 } ) ) ) )
284		fveq2 5800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u = z -> ( f ` u ) = ( f ` z ) )
285	284	oveq1d 6216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) ) )
286	283, 285	ifbieq1d 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
287		eqid 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
288		ovex 6226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) e. _V
289	288, 106	ifex 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( z e. ( `' f " ( ran f \ { 0 } ) ) , ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol* ` ( `' f " ( ran f \ { 0 } ) ) ) ) ) ) , 0 ) e. _V
290	286, 287, 289	fvmpt 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
291	290	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 ) ) )
292	291, 290	ifbieq1d 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
293		iftrue 3906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 0 <_ ( ( f ` z ) - ( ( ( S.1 ` f ) - b ) / ( 2 x. ( vol*