Theorem itg2addnclem2

Description: Lemma for itg2addnc . The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017)

	Ref	Expression
Hypotheses	itg2addnc.f1	|- ( ph -> F e. MblFn )
	itg2addnc.f2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
Assertion	itg2addnclem2	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) e. dom S.1 )

Proof

Step	Hyp	Ref	Expression
1		itg2addnc.f1	|- ( ph -> F e. MblFn )
2		itg2addnc.f2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
3		rge0ssre	|- ( 0 [,) +oo ) C_ RR
4		fss	|- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
5	2 3 4	sylancl	|- ( ph -> F : RR --> RR )
6	5	ad2antrr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> F : RR --> RR )
7	6	ffvelrnda	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( F ` x ) e. RR )
8		rpre	|- ( v e. RR+ -> v e. RR )
9		3re	|- 3 e. RR
10		3ne0	|- 3 =/= 0
11	9 10	pm3.2i	|- ( 3 e. RR /\ 3 =/= 0 )
12		redivcl	|- ( ( v e. RR /\ 3 e. RR /\ 3 =/= 0 ) -> ( v / 3 ) e. RR )
13	12	3expb	|- ( ( v e. RR /\ ( 3 e. RR /\ 3 =/= 0 ) ) -> ( v / 3 ) e. RR )
14	8 11 13	sylancl	|- ( v e. RR+ -> ( v / 3 ) e. RR )
15	14	ad2antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( v / 3 ) e. RR )
16		rpcnne0	|- ( v e. RR+ -> ( v e. CC /\ v =/= 0 ) )
17		3cn	|- 3 e. CC
18	17 10	pm3.2i	|- ( 3 e. CC /\ 3 =/= 0 )
19		divne0	|- ( ( ( v e. CC /\ v =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( v / 3 ) =/= 0 )
20	16 18 19	sylancl	|- ( v e. RR+ -> ( v / 3 ) =/= 0 )
21	20	ad2antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( v / 3 ) =/= 0 )
22	7 15 21	redivcld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( F ` x ) / ( v / 3 ) ) e. RR )
23		reflcl	|- ( ( ( F ` x ) / ( v / 3 ) ) e. RR -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. RR )
24	22 23	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. RR )
25		peano2rem	|- ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. RR -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) e. RR )
26	24 25	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) e. RR )
27	26 15	remulcld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. RR )
28		i1ff	|- ( h e. dom S.1 -> h : RR --> RR )
29	28	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> h : RR --> RR )
30	29	ffvelrnda	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( h ` x ) e. RR )
31	27 30	ifcld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. RR )
32	31	fmpttd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) : RR --> RR )
33		fzfi	|- ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) e. Fin
34		ovex	|- ( ( t - 1 ) x. ( v / 3 ) ) e. _V
35		eqid	|- ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) = ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) )
36	34 35	fnmpti	|- ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) Fn ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) )
37		dffn4	|- ( ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) Fn ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) <-> ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) : ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) -onto-> ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) )
38	36 37	mpbi	|- ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) : ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) -onto-> ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) )
39		fofi	|- ( ( ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) e. Fin /\ ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) : ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) -onto-> ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) ) -> ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) e. Fin )
40	33 38 39	mp2an	|- ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) e. Fin
41		i1frn	|- ( h e. dom S.1 -> ran h e. Fin )
42	41	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ran h e. Fin )
43		unfi	|- ( ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) e. Fin /\ ran h e. Fin ) -> ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) e. Fin )
44	40 42 43	sylancr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) e. Fin )
45		0zd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> 0 e. ZZ )
46	28	frnd	|- ( h e. dom S.1 -> ran h C_ RR )
47		i1f0rn	|- ( h e. dom S.1 -> 0 e. ran h )
48		elex2	|- ( 0 e. ran h -> E. x x e. ran h )
49	47 48	syl	|- ( h e. dom S.1 -> E. x x e. ran h )
50		n0	|- ( ran h =/= (/) <-> E. x x e. ran h )
51	49 50	sylibr	|- ( h e. dom S.1 -> ran h =/= (/) )
52		fimaxre2	|- ( ( ran h C_ RR /\ ran h e. Fin ) -> E. x e. RR A. y e. ran h y <_ x )
53	46 41 52	syl2anc	|- ( h e. dom S.1 -> E. x e. RR A. y e. ran h y <_ x )
54		suprcl	|- ( ( ran h C_ RR /\ ran h =/= (/) /\ E. x e. RR A. y e. ran h y <_ x ) -> sup ( ran h , RR , < ) e. RR )
55	46 51 53 54	syl3anc	|- ( h e. dom S.1 -> sup ( ran h , RR , < ) e. RR )
56	55	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> sup ( ran h , RR , < ) e. RR )
57	56 15 21	redivcld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( sup ( ran h , RR , < ) / ( v / 3 ) ) e. RR )
58		peano2re	|- ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) e. RR -> ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) e. RR )
59	57 58	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) e. RR )
60		ceicl	|- ( ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) e. RR -> -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) e. ZZ )
61	59 60	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) e. ZZ )
62	61	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) e. ZZ )
63	22	flcld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. ZZ )
64	63	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. ZZ )
65		3nn	|- 3 e. NN
66		nnrp	|- ( 3 e. NN -> 3 e. RR+ )
67	65 66	ax-mp	|- 3 e. RR+
68		rpdivcl	|- ( ( v e. RR+ /\ 3 e. RR+ ) -> ( v / 3 ) e. RR+ )
69	67 68	mpan2	|- ( v e. RR+ -> ( v / 3 ) e. RR+ )
70	69	ad2antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( v / 3 ) e. RR+ )
71	2	ad2antrr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> F : RR --> ( 0 [,) +oo ) )
72	71	ffvelrnda	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
73		elrege0	|- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
74	72 73	sylib	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
75	74	simprd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
76	7 70 75	divge0d	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> 0 <_ ( ( F ` x ) / ( v / 3 ) ) )
77		flge0nn0	|- ( ( ( ( F ` x ) / ( v / 3 ) ) e. RR /\ 0 <_ ( ( F ` x ) / ( v / 3 ) ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. NN0 )
78	22 76 77	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. NN0 )
79	78	nn0ge0d	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> 0 <_ ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
80	79	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> 0 <_ ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
81	46 51 53	3jca	|- ( h e. dom S.1 -> ( ran h C_ RR /\ ran h =/= (/) /\ E. x e. RR A. y e. ran h y <_ x ) )
82	81	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ran h C_ RR /\ ran h =/= (/) /\ E. x e. RR A. y e. ran h y <_ x ) )
83		ffn	|- ( h : RR --> RR -> h Fn RR )
84	28 83	syl	|- ( h e. dom S.1 -> h Fn RR )
85		dffn3	|- ( h Fn RR <-> h : RR --> ran h )
86	84 85	sylib	|- ( h e. dom S.1 -> h : RR --> ran h )
87	86	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> h : RR --> ran h )
88	87	ffvelrnda	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( h ` x ) e. ran h )
89		suprub	|- ( ( ( ran h C_ RR /\ ran h =/= (/) /\ E. x e. RR A. y e. ran h y <_ x ) /\ ( h ` x ) e. ran h ) -> ( h ` x ) <_ sup ( ran h , RR , < ) )
90	82 88 89	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( h ` x ) <_ sup ( ran h , RR , < ) )
91		letr	|- ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. RR /\ ( h ` x ) e. RR /\ sup ( ran h , RR , < ) e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) <_ sup ( ran h , RR , < ) ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ sup ( ran h , RR , < ) ) )
92	27 30 56 91	syl3anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) <_ sup ( ran h , RR , < ) ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ sup ( ran h , RR , < ) ) )
93	26 56 70	lemuldivd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ sup ( ran h , RR , < ) <-> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) <_ ( sup ( ran h , RR , < ) / ( v / 3 ) ) ) )
94		1red	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> 1 e. RR )
95	24 94 57	lesubaddd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) <_ ( sup ( ran h , RR , < ) / ( v / 3 ) ) <-> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) )
96	93 95	bitrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ sup ( ran h , RR , < ) <-> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) )
97		ceige	|- ( ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) e. RR -> ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) )
98	59 97	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) )
99	61	zred	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) e. RR )
100		letr	|- ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. RR /\ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) e. RR /\ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) /\ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
101	24 59 99 100	syl3anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) /\ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
102	98 101	mpan2d	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
103	96 102	sylbid	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ sup ( ran h , RR , < ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
104	92 103	syld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) <_ sup ( ran h , RR , < ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
105	90 104	mpan2d	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
106	105	adantrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
107	106	imp	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) )
108	45 62 64 80 107	elfzd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) )
109		eqid	|- ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) )
110		oveq1	|- ( t = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) -> ( t - 1 ) = ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) )
111	110	oveq1d	|- ( t = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) -> ( ( t - 1 ) x. ( v / 3 ) ) = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) )
112	111	rspceeqv	|- ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) /\ ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) -> E. t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) = ( ( t - 1 ) x. ( v / 3 ) ) )
113	108 109 112	sylancl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> E. t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) = ( ( t - 1 ) x. ( v / 3 ) ) )
114		ovex	|- ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. _V
115	35	elrnmpt	|- ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. _V -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) <-> E. t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) = ( ( t - 1 ) x. ( v / 3 ) ) ) )
116	114 115	ax-mp	|- ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) <-> E. t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) = ( ( t - 1 ) x. ( v / 3 ) ) )
117	113 116	sylibr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) )
118		elun1	|- ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
119	117 118	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
120		elun2	|- ( ( h ` x ) e. ran h -> ( h ` x ) e. ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
121	88 120	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( h ` x ) e. ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
122	121	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) /\ -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) ) -> ( h ` x ) e. ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
123	119 122	ifclda	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
124	123	fmpttd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) : RR --> ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
125	124	frnd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) C_ ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) )
126		ssfi	|- ( ( ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) e. Fin /\ ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) C_ ( ran ( t e. ( 0 ... -u ( |_ ` -u ( ( sup ( ran h , RR , < ) / ( v / 3 ) ) + 1 ) ) ) |-> ( ( t - 1 ) x. ( v / 3 ) ) ) u. ran h ) ) -> ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) e. Fin )
127	44 125 126	syl2anc	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) e. Fin )
128		eqid	|- ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) = ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) )
129	128	mptpreima	|- ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) = { x e. RR | if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } }
130		unrab	|- ( { x e. RR | ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) } u. { x e. RR | ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) } ) = { x e. RR | ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) ) }
131		inrab	|- ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) = { x e. RR | ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) }
132	131	ineq1i	|- ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) = ( { x e. RR | ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) } i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } )
133		inrab	|- ( { x e. RR | ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) } i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) = { x e. RR | ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) }
134	132 133	eqtri	|- ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) = { x e. RR | ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) }
135		unrab	|- ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) = { x e. RR | ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) }
136	135	ineq1i	|- ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) = ( { x e. RR | ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) } i^i { x e. RR | t = ( h ` x ) } )
137		inrab	|- ( { x e. RR | ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) } i^i { x e. RR | t = ( h ` x ) } ) = { x e. RR | ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) }
138	136 137	eqtri	|- ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) = { x e. RR | ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) }
139	134 138	uneq12i	|- ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) u. ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) ) = ( { x e. RR | ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) } u. { x e. RR | ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) } )
140		eqcom	|- ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = t <-> t = if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) )
141		fvex	|- ( h ` x ) e. _V
142	114 141	ifex	|- if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. _V
143	142	elsn	|- ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } <-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = t )
144		ianor	|- ( -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) <-> ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ -. ( h ` x ) =/= 0 ) )
145		nne	|- ( -. ( h ` x ) =/= 0 <-> ( h ` x ) = 0 )
146	145	orbi2i	|- ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ -. ( h ` x ) =/= 0 ) <-> ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) )
147	144 146	bitr2i	|- ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) <-> -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) )
148	147	anbi1i	|- ( ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) <-> ( -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( h ` x ) ) )
149	148	orbi2i	|- ( ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) ) <-> ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( h ` x ) ) ) )
150		eqif	|- ( t = if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) <-> ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( h ` x ) ) ) )
151	149 150	bitr4i	|- ( ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) ) <-> t = if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) )
152	140 143 151	3bitr4i	|- ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } <-> ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) ) )
153	152	rabbii	|- { x e. RR | if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } } = { x e. RR | ( ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) /\ t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) \/ ( ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) \/ ( h ` x ) = 0 ) /\ t = ( h ` x ) ) ) }
154	130 139 153	3eqtr4ri	|- { x e. RR | if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } } = ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) u. ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) )
155	129 154	eqtri	|- ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) = ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) u. ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) )
156		eldifi	|- ( t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) -> t e. ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) )
157	32	frnd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) C_ RR )
158	157	sseld	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( t e. ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) -> t e. RR ) )
159	156 158	syl5	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) -> t e. RR ) )
160	159	imdistani	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) )
161		rabiun	|- { x e. U_ t e. ran h ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = U_ t e. ran h { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) }
162		cnvimarndm	|- ( `' h " ran h ) = dom h
163		iunid	|- U_ t e. ran h { t } = ran h
164	163	imaeq2i	|- ( `' h " U_ t e. ran h { t } ) = ( `' h " ran h )
165		imaiun	|- ( `' h " U_ t e. ran h { t } ) = U_ t e. ran h ( `' h " { t } )
166	164 165	eqtr3i	|- ( `' h " ran h ) = U_ t e. ran h ( `' h " { t } )
167	162 166	eqtr3i	|- dom h = U_ t e. ran h ( `' h " { t } )
168	28	fdmd	|- ( h e. dom S.1 -> dom h = RR )
169	167 168	eqtr3id	|- ( h e. dom S.1 -> U_ t e. ran h ( `' h " { t } ) = RR )
170	169	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> U_ t e. ran h ( `' h " { t } ) = RR )
171		rabeq	|- ( U_ t e. ran h ( `' h " { t } ) = RR -> { x e. U_ t e. ran h ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
172	170 171	syl	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> { x e. U_ t e. ran h ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
173	161 172	eqtr3id	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> U_ t e. ran h { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
174		fniniseg	|- ( h Fn RR -> ( x e. ( `' h " { t } ) <-> ( x e. RR /\ ( h ` x ) = t ) ) )
175	28 83 174	3syl	|- ( h e. dom S.1 -> ( x e. ( `' h " { t } ) <-> ( x e. RR /\ ( h ` x ) = t ) ) )
176	175	simplbda	|- ( ( h e. dom S.1 /\ x e. ( `' h " { t } ) ) -> ( h ` x ) = t )
177	176	breq2d	|- ( ( h e. dom S.1 /\ x e. ( `' h " { t } ) ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) <-> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t ) )
178	177	rabbidva	|- ( h e. dom S.1 -> { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
179		inrab2	|- ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) = { x e. ( RR i^i ( `' h " { t } ) ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t }
180		imassrn	|- ( `' h " { t } ) C_ ran `' h
181		dfdm4	|- dom h = ran `' h
182	181 168	eqtr3id	|- ( h e. dom S.1 -> ran `' h = RR )
183	180 182	sseqtrid	|- ( h e. dom S.1 -> ( `' h " { t } ) C_ RR )
184		sseqin2	|- ( ( `' h " { t } ) C_ RR <-> ( RR i^i ( `' h " { t } ) ) = ( `' h " { t } ) )
185	183 184	sylib	|- ( h e. dom S.1 -> ( RR i^i ( `' h " { t } ) ) = ( `' h " { t } ) )
186		rabeq	|- ( ( RR i^i ( `' h " { t } ) ) = ( `' h " { t } ) -> { x e. ( RR i^i ( `' h " { t } ) ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } = { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
187	185 186	syl	|- ( h e. dom S.1 -> { x e. ( RR i^i ( `' h " { t } ) ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } = { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
188	179 187	syl5eq	|- ( h e. dom S.1 -> ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) = { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
189	178 188	eqtr4d	|- ( h e. dom S.1 -> { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) )
190	189	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) )
191	26	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) e. RR )
192	46	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ran h C_ RR )
193	192	sselda	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> t e. RR )
194	193	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> t e. RR )
195	69	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( v / 3 ) e. RR+ )
196	191 194 195	lemuldivd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t <-> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) <_ ( t / ( v / 3 ) ) ) )
197	24	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. RR )
198		1red	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> 1 e. RR )
199	14	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( v / 3 ) e. RR )
200	20	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( v / 3 ) =/= 0 )
201	194 199 200	redivcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( t / ( v / 3 ) ) e. RR )
202	197 198 201	lesubaddd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) <_ ( t / ( v / 3 ) ) <-> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( t / ( v / 3 ) ) + 1 ) ) )
203	7	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( F ` x ) e. RR )
204		peano2re	|- ( ( t / ( v / 3 ) ) e. RR -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
205	201 204	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
206		reflcl	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. RR -> ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) e. RR )
207	205 206	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) e. RR )
208		peano2re	|- ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) e. RR -> ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) e. RR )
209	207 208	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) e. RR )
210	203 209 195	ltdivmuld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( ( F ` x ) / ( v / 3 ) ) < ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) <-> ( F ` x ) < ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) )
211	22	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( F ` x ) / ( v / 3 ) ) e. RR )
212		flflp1	|- ( ( ( ( F ` x ) / ( v / 3 ) ) e. RR /\ ( ( t / ( v / 3 ) ) + 1 ) e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( t / ( v / 3 ) ) + 1 ) <-> ( ( F ` x ) / ( v / 3 ) ) < ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) )
213	211 205 212	syl2anc	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( t / ( v / 3 ) ) + 1 ) <-> ( ( F ` x ) / ( v / 3 ) ) < ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) )
214	199 209	remulcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) e. RR )
215	214	rexrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) e. RR* )
216		elioomnf	|- ( ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) e. RR* -> ( ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
217	215 216	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
218	203	biantrurd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( F ` x ) < ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
219	217 218	bitr4d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) <-> ( F ` x ) < ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) )
220	210 213 219	3bitr4d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <_ ( ( t / ( v / 3 ) ) + 1 ) <-> ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
221	196 202 220	3bitrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t <-> ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
222	221	rabbidva	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } = { x e. RR | ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) } )
223	2	feqmptd	|- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
224	223	cnveqd	|- ( ph -> `' F = `' ( x e. RR |-> ( F ` x ) ) )
225	224	imaeq1d	|- ( ph -> ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) = ( `' ( x e. RR |-> ( F ` x ) ) " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
226		eqid	|- ( x e. RR |-> ( F ` x ) ) = ( x e. RR |-> ( F ` x ) )
227	226	mptpreima	|- ( `' ( x e. RR |-> ( F ` x ) ) " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) = { x e. RR | ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) }
228	225 227	eqtrdi	|- ( ph -> ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) = { x e. RR | ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) } )
229	228	ad3antrrr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) = { x e. RR | ( F ` x ) e. ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) } )
230	222 229	eqtr4d	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } = ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) )
231		mbfima	|- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) e. dom vol )
232	1 5 231	syl2anc	|- ( ph -> ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) e. dom vol )
233	232	ad3antrrr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> ( `' F " ( -oo (,) ( ( v / 3 ) x. ( ( |_ ` ( ( t / ( v / 3 ) ) + 1 ) ) + 1 ) ) ) ) e. dom vol )
234	230 233	eqeltrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } e. dom vol )
235	46	sseld	|- ( h e. dom S.1 -> ( t e. ran h -> t e. RR ) )
236	235	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( t e. ran h -> t e. RR ) )
237	236	imdistani	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) )
238		i1fmbf	|- ( h e. dom S.1 -> h e. MblFn )
239	238 28	jca	|- ( h e. dom S.1 -> ( h e. MblFn /\ h : RR --> RR ) )
240	239	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( h e. MblFn /\ h : RR --> RR ) )
241		mbfimasn	|- ( ( h e. MblFn /\ h : RR --> RR /\ t e. RR ) -> ( `' h " { t } ) e. dom vol )
242	241	3expa	|- ( ( ( h e. MblFn /\ h : RR --> RR ) /\ t e. RR ) -> ( `' h " { t } ) e. dom vol )
243	240 242	sylan	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( `' h " { t } ) e. dom vol )
244	237 243	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> ( `' h " { t } ) e. dom vol )
245		inmbl	|- ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } e. dom vol /\ ( `' h " { t } ) e. dom vol ) -> ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) e. dom vol )
246	234 244 245	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) e. dom vol )
247	190 246	eqeltrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
248	247	ralrimiva	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> A. t e. ran h { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
249		finiunmbl	|- ( ( ran h e. Fin /\ A. t e. ran h { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol ) -> U_ t e. ran h { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
250	42 248 249	syl2anc	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> U_ t e. ran h { x e. ( `' h " { t } ) | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
251	173 250	eqeltrrd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
252		unrab	|- ( { x e. RR | ( h ` x ) e. ( -oo (,) 0 ) } u. { x e. RR | ( h ` x ) e. ( 0 (,) +oo ) } ) = { x e. RR | ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) }
253	28	feqmptd	|- ( h e. dom S.1 -> h = ( x e. RR |-> ( h ` x ) ) )
254	253	cnveqd	|- ( h e. dom S.1 -> `' h = `' ( x e. RR |-> ( h ` x ) ) )
255	254	imaeq1d	|- ( h e. dom S.1 -> ( `' h " ( -oo (,) 0 ) ) = ( `' ( x e. RR |-> ( h ` x ) ) " ( -oo (,) 0 ) ) )
256		eqid	|- ( x e. RR |-> ( h ` x ) ) = ( x e. RR |-> ( h ` x ) )
257	256	mptpreima	|- ( `' ( x e. RR |-> ( h ` x ) ) " ( -oo (,) 0 ) ) = { x e. RR | ( h ` x ) e. ( -oo (,) 0 ) }
258	255 257	eqtrdi	|- ( h e. dom S.1 -> ( `' h " ( -oo (,) 0 ) ) = { x e. RR | ( h ` x ) e. ( -oo (,) 0 ) } )
259	254	imaeq1d	|- ( h e. dom S.1 -> ( `' h " ( 0 (,) +oo ) ) = ( `' ( x e. RR |-> ( h ` x ) ) " ( 0 (,) +oo ) ) )
260	256	mptpreima	|- ( `' ( x e. RR |-> ( h ` x ) ) " ( 0 (,) +oo ) ) = { x e. RR | ( h ` x ) e. ( 0 (,) +oo ) }
261	259 260	eqtrdi	|- ( h e. dom S.1 -> ( `' h " ( 0 (,) +oo ) ) = { x e. RR | ( h ` x ) e. ( 0 (,) +oo ) } )
262	258 261	uneq12d	|- ( h e. dom S.1 -> ( ( `' h " ( -oo (,) 0 ) ) u. ( `' h " ( 0 (,) +oo ) ) ) = ( { x e. RR | ( h ` x ) e. ( -oo (,) 0 ) } u. { x e. RR | ( h ` x ) e. ( 0 (,) +oo ) } ) )
263	28	ffvelrnda	|- ( ( h e. dom S.1 /\ x e. RR ) -> ( h ` x ) e. RR )
264		0re	|- 0 e. RR
265		lttri2	|- ( ( ( h ` x ) e. RR /\ 0 e. RR ) -> ( ( h ` x ) =/= 0 <-> ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) ) )
266	264 265	mpan2	|- ( ( h ` x ) e. RR -> ( ( h ` x ) =/= 0 <-> ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) ) )
267		ibar	|- ( ( h ` x ) e. RR -> ( ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) <-> ( ( h ` x ) e. RR /\ ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) ) ) )
268		andi	|- ( ( ( h ` x ) e. RR /\ ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) ) <-> ( ( ( h ` x ) e. RR /\ ( h ` x ) < 0 ) \/ ( ( h ` x ) e. RR /\ 0 < ( h ` x ) ) ) )
269		0xr	|- 0 e. RR*
270		elioomnf	|- ( 0 e. RR* -> ( ( h ` x ) e. ( -oo (,) 0 ) <-> ( ( h ` x ) e. RR /\ ( h ` x ) < 0 ) ) )
271		elioopnf	|- ( 0 e. RR* -> ( ( h ` x ) e. ( 0 (,) +oo ) <-> ( ( h ` x ) e. RR /\ 0 < ( h ` x ) ) ) )
272	270 271	orbi12d	|- ( 0 e. RR* -> ( ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) <-> ( ( ( h ` x ) e. RR /\ ( h ` x ) < 0 ) \/ ( ( h ` x ) e. RR /\ 0 < ( h ` x ) ) ) ) )
273	269 272	ax-mp	|- ( ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) <-> ( ( ( h ` x ) e. RR /\ ( h ` x ) < 0 ) \/ ( ( h ` x ) e. RR /\ 0 < ( h ` x ) ) ) )
274	268 273	bitr4i	|- ( ( ( h ` x ) e. RR /\ ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) ) <-> ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) )
275	267 274	bitrdi	|- ( ( h ` x ) e. RR -> ( ( ( h ` x ) < 0 \/ 0 < ( h ` x ) ) <-> ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) ) )
276	266 275	bitrd	|- ( ( h ` x ) e. RR -> ( ( h ` x ) =/= 0 <-> ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) ) )
277	263 276	syl	|- ( ( h e. dom S.1 /\ x e. RR ) -> ( ( h ` x ) =/= 0 <-> ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) ) )
278	277	rabbidva	|- ( h e. dom S.1 -> { x e. RR | ( h ` x ) =/= 0 } = { x e. RR | ( ( h ` x ) e. ( -oo (,) 0 ) \/ ( h ` x ) e. ( 0 (,) +oo ) ) } )
279	252 262 278	3eqtr4a	|- ( h e. dom S.1 -> ( ( `' h " ( -oo (,) 0 ) ) u. ( `' h " ( 0 (,) +oo ) ) ) = { x e. RR | ( h ` x ) =/= 0 } )
280		i1fima	|- ( h e. dom S.1 -> ( `' h " ( -oo (,) 0 ) ) e. dom vol )
281		i1fima	|- ( h e. dom S.1 -> ( `' h " ( 0 (,) +oo ) ) e. dom vol )
282		unmbl	|- ( ( ( `' h " ( -oo (,) 0 ) ) e. dom vol /\ ( `' h " ( 0 (,) +oo ) ) e. dom vol ) -> ( ( `' h " ( -oo (,) 0 ) ) u. ( `' h " ( 0 (,) +oo ) ) ) e. dom vol )
283	280 281 282	syl2anc	|- ( h e. dom S.1 -> ( ( `' h " ( -oo (,) 0 ) ) u. ( `' h " ( 0 (,) +oo ) ) ) e. dom vol )
284	279 283	eqeltrrd	|- ( h e. dom S.1 -> { x e. RR | ( h ` x ) =/= 0 } e. dom vol )
285	284	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> { x e. RR | ( h ` x ) =/= 0 } e. dom vol )
286		inmbl	|- ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol /\ { x e. RR | ( h ` x ) =/= 0 } e. dom vol ) -> ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) e. dom vol )
287	251 285 286	syl2anc	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) e. dom vol )
288	287	adantr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) e. dom vol )
289	24	recnd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. CC )
290	289	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. CC )
291		1cnd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> 1 e. CC )
292		simplr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> t e. RR )
293	14	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( v / 3 ) e. RR )
294	20	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( v / 3 ) =/= 0 )
295	292 293 294	redivcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( t / ( v / 3 ) ) e. RR )
296	295	recnd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( t / ( v / 3 ) ) e. CC )
297	290 291 296	subadd2d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) = ( t / ( v / 3 ) ) <-> ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) )
298		eqcom	|- ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) = ( t / ( v / 3 ) ) <-> ( t / ( v / 3 ) ) = ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) )
299		recn	|- ( t e. RR -> t e. CC )
300	299	ad2antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> t e. CC )
301	26	recnd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) e. CC )
302	301	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) e. CC )
303	14	recnd	|- ( v e. RR+ -> ( v / 3 ) e. CC )
304	303	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( v / 3 ) e. CC )
305	300 302 304 294	divmul3d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( t / ( v / 3 ) ) = ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) <-> t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) )
306	298 305	syl5bb	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) = ( t / ( v / 3 ) ) <-> t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) )
307	297 306	bitr3d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <-> t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) )
308	307	rabbidva	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } = { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } )
309		imaundi	|- ( `' F " ( { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } u. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) ) = ( ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
310	224	ad4antr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> `' F = `' ( x e. RR |-> ( F ` x ) ) )
311		zre	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. ZZ -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
312	311	adantl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
313	14	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( v / 3 ) e. RR )
314	312 313	remulcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) e. RR )
315	314	rexrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) e. RR* )
316		peano2z	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. ZZ -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. ZZ )
317	316	zred	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. ZZ -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR )
318	317	adantl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR )
319	313 318	remulcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR )
320	319	rexrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR* )
321		zcn	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. ZZ -> ( ( t / ( v / 3 ) ) + 1 ) e. CC )
322	321	adantl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( t / ( v / 3 ) ) + 1 ) e. CC )
323	303	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( v / 3 ) e. CC )
324	322 323	mulcomd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) = ( ( v / 3 ) x. ( ( t / ( v / 3 ) ) + 1 ) ) )
325	69	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( v / 3 ) e. RR+ )
326	311	ltp1d	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. ZZ -> ( ( t / ( v / 3 ) ) + 1 ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) )
327	326	adantl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( t / ( v / 3 ) ) + 1 ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) )
328	312 318 325 327	ltmul2dd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( v / 3 ) x. ( ( t / ( v / 3 ) ) + 1 ) ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) )
329	324 328	eqbrtrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) )
330		snunioo	|- ( ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) e. RR* /\ ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR* /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) -> ( { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } u. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) = ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
331	315 320 329 330	syl3anc	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } u. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) = ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
332	310 331	imaeq12d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( `' F " ( { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } u. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) ) = ( `' ( x e. RR |-> ( F ` x ) ) " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
333	309 332	eqtr3id	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) ) = ( `' ( x e. RR |-> ( F ` x ) ) " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
334	226	mptpreima	|- ( `' ( x e. RR |-> ( F ` x ) ) " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) = { x e. RR | ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) }
335	5	ad3antrrr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> F : RR --> RR )
336	335	ffvelrnda	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( F ` x ) e. RR )
337	336	3biant1d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
338	337	adantr	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
339	311	adantl	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
340	336	adantr	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( F ` x ) e. RR )
341	69	ad4antlr	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( v / 3 ) e. RR+ )
342	339 340 341	lemuldivd	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) <-> ( ( t / ( v / 3 ) ) + 1 ) <_ ( ( F ` x ) / ( v / 3 ) ) ) )
343	317	adantl	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR )
344	340 343 341	ltdivmuld	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) <-> ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
345	344	bicomd	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) <-> ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) )
346	342 345	anbi12d	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) <_ ( ( F ` x ) / ( v / 3 ) ) /\ ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
347	338 346	bitr3d	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( F ` x ) e. RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) <_ ( ( F ` x ) / ( v / 3 ) ) /\ ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
348		elico2	|- ( ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) e. RR /\ ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR* ) -> ( ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
349	314 320 348	syl2anc	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
350	349	adantlr	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( F ` x ) e. RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) <_ ( F ` x ) /\ ( F ` x ) < ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) )
351		eqcom	|- ( ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <-> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) = ( ( t / ( v / 3 ) ) + 1 ) )
352	22	adantlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( F ` x ) / ( v / 3 ) ) e. RR )
353		flbi	|- ( ( ( ( F ` x ) / ( v / 3 ) ) e. RR /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) = ( ( t / ( v / 3 ) ) + 1 ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) <_ ( ( F ` x ) / ( v / 3 ) ) /\ ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
354	352 353	sylan	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) = ( ( t / ( v / 3 ) ) + 1 ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) <_ ( ( F ` x ) / ( v / 3 ) ) /\ ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
355	351 354	syl5bb	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) <_ ( ( F ` x ) / ( v / 3 ) ) /\ ( ( F ` x ) / ( v / 3 ) ) < ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) )
356	347 350 355	3bitr4d	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) )
357	356	an32s	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) /\ x e. RR ) -> ( ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) <-> ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) )
358	357	rabbidva	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> { x e. RR | ( F ` x ) e. ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) } = { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } )
359	334 358	syl5eq	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( `' ( x e. RR |-> ( F ` x ) ) " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) [,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) = { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } )
360	333 359	eqtrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) ) = { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } )
361	1	ad4antr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> F e. MblFn )
362	5	ad4antr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> F : RR --> RR )
363		mbfimasn	|- ( ( F e. MblFn /\ F : RR --> RR /\ ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) e. RR ) -> ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) e. dom vol )
364	361 362 314 363	syl3anc	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) e. dom vol )
365		mbfima	|- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) e. dom vol )
366	1 5 365	syl2anc	|- ( ph -> ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) e. dom vol )
367	366	ad4antr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) e. dom vol )
368		unmbl	|- ( ( ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) e. dom vol /\ ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) e. dom vol ) -> ( ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) ) e. dom vol )
369	364 367 368	syl2anc	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> ( ( `' F " { ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( ( t / ( v / 3 ) ) + 1 ) x. ( v / 3 ) ) (,) ( ( v / 3 ) x. ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) ) ) ) e. dom vol )
370	360 369	eqeltrrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } e. dom vol )
371		simpr	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) -> ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
372	352	flcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. ZZ )
373	372	adantr	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. ZZ )
374	371 373	eqeltrd	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) -> ( ( t / ( v / 3 ) ) + 1 ) e. ZZ )
375	374	stoic1a	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) /\ -. ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> -. ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
376	375	an32s	|- ( ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ -. ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) /\ x e. RR ) -> -. ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
377	376	ralrimiva	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ -. ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> A. x e. RR -. ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
378		rabeq0	|- ( { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } = (/) <-> A. x e. RR -. ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) )
379	377 378	sylibr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ -. ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } = (/) )
380		0mbl	|- (/) e. dom vol
381	379 380	eqeltrdi	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ -. ( ( t / ( v / 3 ) ) + 1 ) e. ZZ ) -> { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } e. dom vol )
382	370 381	pm2.61dan	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> { x e. RR | ( ( t / ( v / 3 ) ) + 1 ) = ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) } e. dom vol )
383	308 382	eqeltrrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } e. dom vol )
384		inmbl	|- ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) e. dom vol /\ { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } e. dom vol ) -> ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) e. dom vol )
385	288 383 384	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) e. dom vol )
386		rabiun	|- { x e. U_ t e. ran h ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = U_ t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) }
387		rabeq	|- ( U_ t e. ran h ( `' h " { t } ) = RR -> { x e. U_ t e. ran h ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
388	169 387	syl	|- ( h e. dom S.1 -> { x e. U_ t e. ran h ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
389	386 388	eqtr3id	|- ( h e. dom S.1 -> U_ t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
390	389	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> U_ t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } )
391	177	notbid	|- ( ( h e. dom S.1 /\ x e. ( `' h " { t } ) ) -> ( -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) <-> -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t ) )
392	391	rabbidva	|- ( h e. dom S.1 -> { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
393		inrab2	|- ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) = { x e. ( RR i^i ( `' h " { t } ) ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t }
394		rabeq	|- ( ( RR i^i ( `' h " { t } ) ) = ( `' h " { t } ) -> { x e. ( RR i^i ( `' h " { t } ) ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } = { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
395	185 394	syl	|- ( h e. dom S.1 -> { x e. ( RR i^i ( `' h " { t } ) ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } = { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
396	393 395	syl5eq	|- ( h e. dom S.1 -> ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) = { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
397	392 396	eqtr4d	|- ( h e. dom S.1 -> { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) )
398	397	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } = ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) )
399		imaundi	|- ( `' F " ( { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } u. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) ) = ( ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) )
400	14 20	jca	|- ( v e. RR+ -> ( ( v / 3 ) e. RR /\ ( v / 3 ) =/= 0 ) )
401		redivcl	|- ( ( t e. RR /\ ( v / 3 ) e. RR /\ ( v / 3 ) =/= 0 ) -> ( t / ( v / 3 ) ) e. RR )
402	401	3expb	|- ( ( t e. RR /\ ( ( v / 3 ) e. RR /\ ( v / 3 ) =/= 0 ) ) -> ( t / ( v / 3 ) ) e. RR )
403	400 402	sylan2	|- ( ( t e. RR /\ v e. RR+ ) -> ( t / ( v / 3 ) ) e. RR )
404	403	ancoms	|- ( ( v e. RR+ /\ t e. RR ) -> ( t / ( v / 3 ) ) e. RR )
405	404	adantll	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( t / ( v / 3 ) ) e. RR )
406	405 204	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
407		peano2re	|- ( ( ( t / ( v / 3 ) ) + 1 ) e. RR -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR )
408		reflcl	|- ( ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR -> ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR )
409	406 407 408	3syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR )
410	14	ad2antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( v / 3 ) e. RR )
411	409 410	remulcld	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR )
412	411	rexrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR* )
413		pnfxr	|- +oo e. RR*
414	413	a1i	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> +oo e. RR* )
415		ltpnf	|- ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) < +oo )
416	411 415	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) < +oo )
417		snunioo	|- ( ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR* /\ +oo e. RR* /\ ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) < +oo ) -> ( { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } u. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) = ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) )
418	412 414 416 417	syl3anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } u. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) = ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) )
419	418	imaeq2d	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( `' F " ( { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } u. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) ) = ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) )
420	399 419	eqtr3id	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) ) = ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) )
421	224	imaeq1d	|- ( ph -> ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) = ( `' ( x e. RR |-> ( F ` x ) ) " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) )
422	226	mptpreima	|- ( `' ( x e. RR |-> ( F ` x ) ) " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) = { x e. RR | ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) }
423	421 422	eqtrdi	|- ( ph -> ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) = { x e. RR | ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) } )
424	423	ad3antrrr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) ) = { x e. RR | ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) } )
425	406 407	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR )
426	425	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR )
427		flflp1	|- ( ( ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) e. RR /\ ( ( F ` x ) / ( v / 3 ) ) e. RR ) -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) <_ ( ( F ` x ) / ( v / 3 ) ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) < ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) + 1 ) ) )
428	426 352 427	syl2anc	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) <_ ( ( F ` x ) / ( v / 3 ) ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) < ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) + 1 ) ) )
429	411	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR )
430		elicopnf	|- ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR -> ( ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) <-> ( ( F ` x ) e. RR /\ ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) <_ ( F ` x ) ) ) )
431	429 430	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) <-> ( ( F ` x ) e. RR /\ ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) <_ ( F ` x ) ) ) )
432	336	biantrurd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) <_ ( F ` x ) <-> ( ( F ` x ) e. RR /\ ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) <_ ( F ` x ) ) ) )
433	409	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) e. RR )
434	69	ad3antlr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( v / 3 ) e. RR+ )
435	433 336 434	lemuldivd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) <_ ( F ` x ) <-> ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) <_ ( ( F ` x ) / ( v / 3 ) ) ) )
436	431 432 435	3bitr2d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) <-> ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) <_ ( ( F ` x ) / ( v / 3 ) ) ) )
437	406	adantr	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( t / ( v / 3 ) ) + 1 ) e. RR )
438	352 23	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) e. RR )
439		1red	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> 1 e. RR )
440	437 438 439	ltadd1d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( t / ( v / 3 ) ) + 1 ) < ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <-> ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) < ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) + 1 ) ) )
441	428 436 440	3bitr4d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) <-> ( ( t / ( v / 3 ) ) + 1 ) < ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) ) )
442	295 439 438	ltaddsubd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( t / ( v / 3 ) ) + 1 ) < ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) <-> ( t / ( v / 3 ) ) < ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) ) )
443	441 442	bitrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) <-> ( t / ( v / 3 ) ) < ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) ) )
444	438 25	syl	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) e. RR )
445	292 444 434	ltdivmul2d	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( t / ( v / 3 ) ) < ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) <-> t < ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) ) )
446	444 293	remulcld	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) e. RR )
447	292 446	ltnled	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( t < ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <-> -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t ) )
448	443 445 447	3bitrd	|- ( ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) /\ x e. RR ) -> ( ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) <-> -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t ) )
449	448	rabbidva	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> { x e. RR | ( F ` x ) e. ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) [,) +oo ) } = { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
450	420 424 449	3eqtrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) ) = { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } )
451	1	ad3antrrr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> F e. MblFn )
452		mbfimasn	|- ( ( F e. MblFn /\ F : RR --> RR /\ ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) e. RR ) -> ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) e. dom vol )
453	451 335 411 452	syl3anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) e. dom vol )
454		mbfima	|- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) e. dom vol )
455	1 5 454	syl2anc	|- ( ph -> ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) e. dom vol )
456	455	ad3antrrr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) e. dom vol )
457		unmbl	|- ( ( ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) e. dom vol /\ ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) e. dom vol ) -> ( ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) ) e. dom vol )
458	453 456 457	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( `' F " { ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) } ) u. ( `' F " ( ( ( |_ ` ( ( ( t / ( v / 3 ) ) + 1 ) + 1 ) ) x. ( v / 3 ) ) (,) +oo ) ) ) e. dom vol )
459	450 458	eqeltrrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } e. dom vol )
460	237 459	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } e. dom vol )
461		inmbl	|- ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } e. dom vol /\ ( `' h " { t } ) e. dom vol ) -> ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) e. dom vol )
462	460 244 461	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ t } i^i ( `' h " { t } ) ) e. dom vol )
463	398 462	eqeltrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ran h ) -> { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
464	463	ralrimiva	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> A. t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
465		finiunmbl	|- ( ( ran h e. Fin /\ A. t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol ) -> U_ t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
466	42 464 465	syl2anc	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> U_ t e. ran h { x e. ( `' h " { t } ) | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
467	390 466	eqeltrrd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol )
468	254	imaeq1d	|- ( h e. dom S.1 -> ( `' h " { 0 } ) = ( `' ( x e. RR |-> ( h ` x ) ) " { 0 } ) )
469	256	mptpreima	|- ( `' ( x e. RR |-> ( h ` x ) ) " { 0 } ) = { x e. RR | ( h ` x ) e. { 0 } }
470	141	elsn	|- ( ( h ` x ) e. { 0 } <-> ( h ` x ) = 0 )
471	470	rabbii	|- { x e. RR | ( h ` x ) e. { 0 } } = { x e. RR | ( h ` x ) = 0 }
472	469 471	eqtri	|- ( `' ( x e. RR |-> ( h ` x ) ) " { 0 } ) = { x e. RR | ( h ` x ) = 0 }
473	468 472	eqtrdi	|- ( h e. dom S.1 -> ( `' h " { 0 } ) = { x e. RR | ( h ` x ) = 0 } )
474		i1fima	|- ( h e. dom S.1 -> ( `' h " { 0 } ) e. dom vol )
475	473 474	eqeltrrd	|- ( h e. dom S.1 -> { x e. RR | ( h ` x ) = 0 } e. dom vol )
476	475	ad2antlr	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> { x e. RR | ( h ` x ) = 0 } e. dom vol )
477		unmbl	|- ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } e. dom vol /\ { x e. RR | ( h ` x ) = 0 } e. dom vol ) -> ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) e. dom vol )
478	467 476 477	syl2anc	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) e. dom vol )
479	478	adantr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) e. dom vol )
480	254	imaeq1d	|- ( h e. dom S.1 -> ( `' h " { t } ) = ( `' ( x e. RR |-> ( h ` x ) ) " { t } ) )
481	256	mptpreima	|- ( `' ( x e. RR |-> ( h ` x ) ) " { t } ) = { x e. RR | ( h ` x ) e. { t } }
482	141	elsn	|- ( ( h ` x ) e. { t } <-> ( h ` x ) = t )
483		eqcom	|- ( ( h ` x ) = t <-> t = ( h ` x ) )
484	482 483	bitri	|- ( ( h ` x ) e. { t } <-> t = ( h ` x ) )
485	484	rabbii	|- { x e. RR | ( h ` x ) e. { t } } = { x e. RR | t = ( h ` x ) }
486	481 485	eqtri	|- ( `' ( x e. RR |-> ( h ` x ) ) " { t } ) = { x e. RR | t = ( h ` x ) }
487	480 486	eqtrdi	|- ( h e. dom S.1 -> ( `' h " { t } ) = { x e. RR | t = ( h ` x ) } )
488	487	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( `' h " { t } ) = { x e. RR | t = ( h ` x ) } )
489	488 243	eqeltrrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> { x e. RR | t = ( h ` x ) } e. dom vol )
490		inmbl	|- ( ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) e. dom vol /\ { x e. RR | t = ( h ` x ) } e. dom vol ) -> ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) e. dom vol )
491	479 489 490	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) e. dom vol )
492		unmbl	|- ( ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) e. dom vol /\ ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) e. dom vol ) -> ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) u. ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) ) e. dom vol )
493	385 491 492	syl2anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. RR ) -> ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) u. ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) ) e. dom vol )
494	160 493	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( ( ( { x e. RR | ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } i^i { x e. RR | ( h ` x ) =/= 0 } ) i^i { x e. RR | t = ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) } ) u. ( ( { x e. RR | -. ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) } u. { x e. RR | ( h ` x ) = 0 } ) i^i { x e. RR | t = ( h ` x ) } ) ) e. dom vol )
495	155 494	eqeltrid	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) e. dom vol )
496		mblvol	|- ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) e. dom vol -> ( vol ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) = ( vol* ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) )
497	495 496	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( vol ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) = ( vol* ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) )
498		eldifsn	|- ( t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) <-> ( t e. ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) /\ t =/= 0 ) )
499	158	anim1d	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( ( t e. ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) /\ t =/= 0 ) -> ( t e. RR /\ t =/= 0 ) ) )
500	498 499	syl5bi	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) -> ( t e. RR /\ t =/= 0 ) ) )
501	500	imdistani	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) )
502	129	a1i	|- ( h e. dom S.1 -> ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) = { x e. RR | if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } } )
503	468 469	eqtrdi	|- ( h e. dom S.1 -> ( `' h " { 0 } ) = { x e. RR | ( h ` x ) e. { 0 } } )
504	502 503	ineq12d	|- ( h e. dom S.1 -> ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) i^i ( `' h " { 0 } ) ) = ( { x e. RR | if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } } i^i { x e. RR | ( h ` x ) e. { 0 } } ) )
505		inrab	|- ( { x e. RR | if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } } i^i { x e. RR | ( h ` x ) e. { 0 } } ) = { x e. RR | ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) }
506	504 505	eqtrdi	|- ( h e. dom S.1 -> ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) i^i ( `' h " { 0 } ) ) = { x e. RR | ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) } )
507	506	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) i^i ( `' h " { 0 } ) ) = { x e. RR | ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) } )
508	145	biimpri	|- ( ( h ` x ) = 0 -> -. ( h ` x ) =/= 0 )
509	508	intnand	|- ( ( h ` x ) = 0 -> -. ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) )
510	509	iffalsed	|- ( ( h ` x ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = ( h ` x ) )
511		eqtr	|- ( ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = ( h ` x ) /\ ( h ` x ) = 0 ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = 0 )
512	510 511	mpancom	|- ( ( h ` x ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = 0 )
513	512	adantl	|- ( ( ( t =/= 0 /\ x e. RR ) /\ ( h ` x ) = 0 ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) = 0 )
514		simpll	|- ( ( ( t =/= 0 /\ x e. RR ) /\ ( h ` x ) = 0 ) -> t =/= 0 )
515	514	necomd	|- ( ( ( t =/= 0 /\ x e. RR ) /\ ( h ` x ) = 0 ) -> 0 =/= t )
516	513 515	eqnetrd	|- ( ( ( t =/= 0 /\ x e. RR ) /\ ( h ` x ) = 0 ) -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) =/= t )
517	516	ex	|- ( ( t =/= 0 /\ x e. RR ) -> ( ( h ` x ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) =/= t ) )
518		orcom	|- ( ( -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } \/ -. ( h ` x ) e. { 0 } ) <-> ( -. ( h ` x ) e. { 0 } \/ -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } ) )
519		ianor	|- ( -. ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) <-> ( -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } \/ -. ( h ` x ) e. { 0 } ) )
520		imor	|- ( ( ( h ` x ) e. { 0 } -> -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } ) <-> ( -. ( h ` x ) e. { 0 } \/ -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } ) )
521	518 519 520	3bitr4i	|- ( -. ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) <-> ( ( h ` x ) e. { 0 } -> -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } ) )
522	143	necon3bbii	|- ( -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } <-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) =/= t )
523	470 522	imbi12i	|- ( ( ( h ` x ) e. { 0 } -> -. if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } ) <-> ( ( h ` x ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) =/= t ) )
524	521 523	bitri	|- ( -. ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) <-> ( ( h ` x ) = 0 -> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) =/= t ) )
525	517 524	sylibr	|- ( ( t =/= 0 /\ x e. RR ) -> -. ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) )
526	525	ralrimiva	|- ( t =/= 0 -> A. x e. RR -. ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) )
527		rabeq0	|- ( { x e. RR | ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) } = (/) <-> A. x e. RR -. ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) )
528	526 527	sylibr	|- ( t =/= 0 -> { x e. RR | ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) } = (/) )
529	528	ad2antll	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> { x e. RR | ( if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) e. { t } /\ ( h ` x ) e. { 0 } ) } = (/) )
530	507 529	eqtrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) i^i ( `' h " { 0 } ) ) = (/) )
531		imassrn	|- ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ ran `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) )
532		dfdm4	|- dom ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) = ran `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) )
533	142 128	dmmpti	|- dom ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) = RR
534	532 533	eqtr3i	|- ran `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) = RR
535	531 534	sseqtri	|- ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ RR
536		reldisj	|- ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ RR -> ( ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) i^i ( `' h " { 0 } ) ) = (/) <-> ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ ( RR \ ( `' h " { 0 } ) ) ) )
537	535 536	ax-mp	|- ( ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) i^i ( `' h " { 0 } ) ) = (/) <-> ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ ( RR \ ( `' h " { 0 } ) ) )
538	530 537	sylib	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ ( RR \ ( `' h " { 0 } ) ) )
539		ffun	|- ( h : RR --> RR -> Fun h )
540		difpreima	|- ( Fun h -> ( `' h " ( ran h \ { 0 } ) ) = ( ( `' h " ran h ) \ ( `' h " { 0 } ) ) )
541	539 540	syl	|- ( h : RR --> RR -> ( `' h " ( ran h \ { 0 } ) ) = ( ( `' h " ran h ) \ ( `' h " { 0 } ) ) )
542		fdm	|- ( h : RR --> RR -> dom h = RR )
543	162 542	syl5eq	|- ( h : RR --> RR -> ( `' h " ran h ) = RR )
544	543	difeq1d	|- ( h : RR --> RR -> ( ( `' h " ran h ) \ ( `' h " { 0 } ) ) = ( RR \ ( `' h " { 0 } ) ) )
545	541 544	eqtrd	|- ( h : RR --> RR -> ( `' h " ( ran h \ { 0 } ) ) = ( RR \ ( `' h " { 0 } ) ) )
546	28 545	syl	|- ( h e. dom S.1 -> ( `' h " ( ran h \ { 0 } ) ) = ( RR \ ( `' h " { 0 } ) ) )
547	546	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( `' h " ( ran h \ { 0 } ) ) = ( RR \ ( `' h " { 0 } ) ) )
548	538 547	sseqtrrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ ( `' h " ( ran h \ { 0 } ) ) )
549		imassrn	|- ( `' h " ( ran h \ { 0 } ) ) C_ ran `' h
550	549 182	sseqtrid	|- ( h e. dom S.1 -> ( `' h " ( ran h \ { 0 } ) ) C_ RR )
551	550	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( `' h " ( ran h \ { 0 } ) ) C_ RR )
552		i1fima	|- ( h e. dom S.1 -> ( `' h " ( ran h \ { 0 } ) ) e. dom vol )
553		mblvol	|- ( ( `' h " ( ran h \ { 0 } ) ) e. dom vol -> ( vol ` ( `' h " ( ran h \ { 0 } ) ) ) = ( vol* ` ( `' h " ( ran h \ { 0 } ) ) ) )
554	552 553	syl	|- ( h e. dom S.1 -> ( vol ` ( `' h " ( ran h \ { 0 } ) ) ) = ( vol* ` ( `' h " ( ran h \ { 0 } ) ) ) )
555		neldifsn	|- -. 0 e. ( ran h \ { 0 } )
556		i1fima2	|- ( ( h e. dom S.1 /\ -. 0 e. ( ran h \ { 0 } ) ) -> ( vol ` ( `' h " ( ran h \ { 0 } ) ) ) e. RR )
557	555 556	mpan2	|- ( h e. dom S.1 -> ( vol ` ( `' h " ( ran h \ { 0 } ) ) ) e. RR )
558	554 557	eqeltrrd	|- ( h e. dom S.1 -> ( vol* ` ( `' h " ( ran h \ { 0 } ) ) ) e. RR )
559	558	ad3antlr	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( vol* ` ( `' h " ( ran h \ { 0 } ) ) ) e. RR )
560		ovolsscl	|- ( ( ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) C_ ( `' h " ( ran h \ { 0 } ) ) /\ ( `' h " ( ran h \ { 0 } ) ) C_ RR /\ ( vol* ` ( `' h " ( ran h \ { 0 } ) ) ) e. RR ) -> ( vol* ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) e. RR )
561	548 551 559 560	syl3anc	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ ( t e. RR /\ t =/= 0 ) ) -> ( vol* ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) e. RR )
562	501 561	syl	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( vol* ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) e. RR )
563	497 562	eqeltrd	|- ( ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) /\ t e. ( ran ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) \ { 0 } ) ) -> ( vol ` ( `' ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) " { t } ) ) e. RR )
564	32 127 495 563	i1fd	|- ( ( ( ph /\ h e. dom S.1 ) /\ v e. RR+ ) -> ( x e. RR |-> if ( ( ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) <_ ( h ` x ) /\ ( h ` x ) =/= 0 ) , ( ( ( |_ ` ( ( F ` x ) / ( v / 3 ) ) ) - 1 ) x. ( v / 3 ) ) , ( h ` x ) ) ) e. dom S.1 )