Theorem itg2gt0 22711

Description: If the function F is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)

Hypotheses

Ref	Expression
itg2gt0.1	|- ( ph -> A e. dom vol )
itg2gt0.2	|- ( ph -> 0 < ( vol ` A ) )
itg2gt0.3	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2gt0.4	|- ( ph -> F e. MblFn )
itg2gt0.5	|- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )

Assertion

Ref	Expression
itg2gt0	|- ( ph -> 0 < ( S.2 ` F ) )

Distinct variable groups:   x, A   x, F   ph, x

Proof of Theorem itg2gt0

Dummy variables k n z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itg2gt0.2	. 2 |- ( ph -> 0 < ( vol ` A ) )
2		itg2gt0.1	. . . . . . 7 |- ( ph -> A e. dom vol )
3		iccssxr 11714	. . . . . . . 8 |- ( 0 [,] +oo ) C_ RR*
4		volf 22476	. . . . . . . . 9 |- vol : dom vol --> ( 0 [,] +oo )
5	4	ffvelrni 6019	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
6	3, 5	sseldi 3429	. . . . . . 7 |- ( A e. dom vol -> ( vol ` A ) e. RR* )
7	2, 6	syl 17	. . . . . 6 |- ( ph -> ( vol ` A ) e. RR* )
8	7	adantr 467	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) e. RR* )
9		itg2gt0.3	. . . . . . . . . . . . . . . 16 |- ( ph -> F : RR --> ( 0 [,) +oo ) )
10		reex 9627	. . . . . . . . . . . . . . . 16 |- RR e. _V
11		fex 6136	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ RR e. _V ) -> F e. _V )
12	9, 10, 11	sylancl 667	. . . . . . . . . . . . . . 15 |- ( ph -> F e. _V )
13		cnvexg 6736	. . . . . . . . . . . . . . 15 |- ( F e. _V -> `' F e. _V )
14	12, 13	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> `' F e. _V )
15		imaexg 6727	. . . . . . . . . . . . . 14 |- ( `' F e. _V -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
16	14, 15	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
17	16	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
18		eqid 2450	. . . . . . . . . . . 12 |- ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) = ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) )
19	17, 18	fmptd 6044	. . . . . . . . . . 11 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V )
20		ffn 5726	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
21	19, 20	syl 17	. . . . . . . . . 10 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
22		fniunfv 6150	. . . . . . . . . 10 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
23	21, 22	syl 17	. . . . . . . . 9 |- ( ph -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
24		itg2gt0.4	. . . . . . . . . . . . . . 15 |- ( ph -> F e. MblFn )
25		rge0ssre 11737	. . . . . . . . . . . . . . . 16 |- ( 0 [,) +oo ) C_ RR
26		fss 5735	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
27	9, 25, 26	sylancl 667	. . . . . . . . . . . . . . 15 |- ( ph -> F : RR --> RR )
28		mbfima 22581	. . . . . . . . . . . . . . 15 |- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
29	24, 27, 28	syl2anc 666	. . . . . . . . . . . . . 14 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
30	29	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
31	30, 18	fmptd 6044	. . . . . . . . . . . 12 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol )
32	31	ffvelrnda 6020	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
33	32	ralrimiva 2801	. . . . . . . . . 10 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
34		iunmbl 22499	. . . . . . . . . 10 |- ( A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
35	33, 34	syl 17	. . . . . . . . 9 |- ( ph -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
36	23, 35	eqeltrrd 2529	. . . . . . . 8 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol )
37		mblss 22478	. . . . . . . 8 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
38	36, 37	syl 17	. . . . . . 7 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
39		ovolcl 22424	. . . . . . 7 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
40	38, 39	syl 17	. . . . . 6 |- ( ph -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
41	40	adantr 467	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
42		0xr 9684	. . . . . 6 |- 0 e. RR*
43	42	a1i 11	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> 0 e. RR* )
44		mblvol 22477	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
45	2, 44	syl 17	. . . . . . 7 |- ( ph -> ( vol ` A ) = ( vol* ` A ) )
46		mblss 22478	. . . . . . . . . . . . . . . 16 |- ( A e. dom vol -> A C_ RR )
47	2, 46	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ RR )
48	47	sselda 3431	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. RR )
49	9	ffvelrnda 6020	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
50		elrege0 11735	. . . . . . . . . . . . . . . 16 |- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
51	49, 50	sylib 200	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
52	51	simpld 461	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
53	48, 52	syldan 473	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
54		itg2gt0.5	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )
55		nnrecl 10864	. . . . . . . . . . . . 13 |- ( ( ( F ` x ) e. RR /\ 0 < ( F ` x ) ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
56	53, 54, 55	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
57		ffn 5726	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,) +oo ) -> F Fn RR )
58	9, 57	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> F Fn RR )
59	58	ad2antrr 731	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> F Fn RR )
60		elpreima 6000	. . . . . . . . . . . . . . . 16 |- ( F Fn RR -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
62	48	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> x e. RR )
63	62	biantrurd 511	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
64		nnrecre 10643	. . . . . . . . . . . . . . . . . . 19 |- ( k e. NN -> ( 1 / k ) e. RR )
65	64	adantl 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR )
66	65	rexrd 9687	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR* )
67	66	adantlr 720	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( 1 / k ) e. RR* )
68		elioopnf 11725	. . . . . . . . . . . . . . . 16 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
69	67, 68	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
70	61, 63, 69	3bitr2d 285	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
71		id 22	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. NN )
72		imaexg 6727	. . . . . . . . . . . . . . . . . 18 |- ( `' F e. _V -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
73	14, 72	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
74	73	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
75		oveq2 6296	. . . . . . . . . . . . . . . . . . 19 |- ( n = k -> ( 1 / n ) = ( 1 / k ) )
76	75	oveq1d 6303	. . . . . . . . . . . . . . . . . 18 |- ( n = k -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / k ) (,) +oo ) )
77	76	imaeq2d 5167	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
78	77, 18	fvmptg 5944	. . . . . . . . . . . . . . . 16 |- ( ( k e. NN /\ ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
79	71, 74, 78	syl2anr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
80	79	eleq2d 2513	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) <-> x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
81	53	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( F ` x ) e. RR )
82	81	biantrurd 511	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( 1 / k ) < ( F ` x ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
83	70, 80, 82	3bitr4rd 290	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( 1 / k ) < ( F ` x ) <-> x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
84	83	rexbidva 2897	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( E. k e. NN ( 1 / k ) < ( F ` x ) <-> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
85	56, 84	mpbid 214	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) )
86	85	ex 436	. . . . . . . . . 10 |- ( ph -> ( x e. A -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
87		eluni2 4201	. . . . . . . . . . 11 |- ( x e. U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) <-> E. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) x e. z )
88		eleq2 2517	. . . . . . . . . . . . 13 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( x e. z <-> x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
89	88	rexrn 6022	. . . . . . . . . . . 12 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN -> ( E. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) x e. z <-> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
90	21, 89	syl 17	. . . . . . . . . . 11 |- ( ph -> ( E. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) x e. z <-> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
91	87, 90	syl5bb 261	. . . . . . . . . 10 |- ( ph -> ( x e. U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) <-> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
92	86, 91	sylibrd 238	. . . . . . . . 9 |- ( ph -> ( x e. A -> x e. U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
93	92	ssrdv 3437	. . . . . . . 8 |- ( ph -> A C_ U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
94		ovolss 22431	. . . . . . . 8 |- ( ( A C_ U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) /\ U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR ) -> ( vol* ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
95	93, 38, 94	syl2anc 666	. . . . . . 7 |- ( ph -> ( vol* ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
96	45, 95	eqbrtrd 4422	. . . . . 6 |- ( ph -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
97	96	adantr 467	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
98		mblvol 22477	. . . . . . . . 9 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
99	36, 98	syl 17	. . . . . . . 8 |- ( ph -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
100		peano2nn 10618	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( k + 1 ) e. NN )
101	100	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
102		nnrecre 10643	. . . . . . . . . . . . . . 15 |- ( ( k + 1 ) e. NN -> ( 1 / ( k + 1 ) ) e. RR )
103	101, 102	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR )
104	103	rexrd 9687	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR* )
105		nnre 10613	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. RR )
106	105	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> k e. RR )
107	106	lep1d 10535	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> k <_ ( k + 1 ) )
108		nngt0 10635	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> 0 < k )
109	108	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < k )
110	101	nnred 10621	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
111	101	nngt0d 10650	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < ( k + 1 ) )
112		lerec 10486	. . . . . . . . . . . . . . 15 |- ( ( ( k e. RR /\ 0 < k ) /\ ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
113	106, 109, 110, 111, 112	syl22anc 1268	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
114	107, 113	mpbid 214	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) )
115		iooss1 11668	. . . . . . . . . . . . 13 |- ( ( ( 1 / ( k + 1 ) ) e. RR* /\ ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
116	104, 114, 115	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
117		imass2 5203	. . . . . . . . . . . 12 |- ( ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
118	116, 117	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
119	71, 73, 78	syl2anr 481	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
120		imaexg 6727	. . . . . . . . . . . . 13 |- ( `' F e. _V -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
121	14, 120	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
122		oveq2 6296	. . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( 1 / n ) = ( 1 / ( k + 1 ) ) )
123	122	oveq1d 6303	. . . . . . . . . . . . . 14 |- ( n = ( k + 1 ) -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / ( k + 1 ) ) (,) +oo ) )
124	123	imaeq2d 5167	. . . . . . . . . . . . 13 |- ( n = ( k + 1 ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
125	124, 18	fvmptg 5944	. . . . . . . . . . . 12 |- ( ( ( k + 1 ) e. NN /\ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
126	100, 121, 125	syl2anr 481	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
127	118, 119, 126	3sstr4d 3474	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) )
128	127	ralrimiva 2801	. . . . . . . . 9 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) )
129		volsup 22502	. . . . . . . . 9 |- ( ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol /\ A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) ) -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
130	31, 128, 129	syl2anc 666	. . . . . . . 8 |- ( ph -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
131	99, 130	eqtr3d 2486	. . . . . . 7 |- ( ph -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
132	131	adantr 467	. . . . . 6 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
133	73	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
134	71, 133, 78	syl2anr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
135	134	fveq2d 5867	. . . . . . . . . . 11 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) = ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
136	42	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 e. RR* )
137		nnrecgt0 10644	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. NN -> 0 < ( 1 / k ) )
138	137	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> 0 < ( 1 / k ) )
139		0re 9640	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. RR
140		ltle 9719	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 0 e. RR /\ ( 1 / k ) e. RR ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
141	139, 65, 140	sylancr 668	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
142	138, 141	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. NN ) -> 0 <_ ( 1 / k ) )
143		elxrge0 11738	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 / k ) e. ( 0 [,] +oo ) <-> ( ( 1 / k ) e. RR* /\ 0 <_ ( 1 / k ) ) )
144	66, 142, 143	sylanbrc 669	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,] +oo ) )
145		0e0iccpnf 11740	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. ( 0 [,] +oo )
146		ifcl 3922	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 1 / k ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
147	144, 145, 146	sylancl 667	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
148	147	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
149		eqid 2450	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) = ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) )
150	148, 149	fmptd 6044	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
151	150	adantrr 722	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
152		itg2cl 22683	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR* )
153	151, 152	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR* )
154		icossicc 11718	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
155		fss 5735	. . . . . . . . . . . . . . . . . . . 20 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
156	9, 154, 155	sylancl 667	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
157		itg2cl 22683	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S.2 ` F ) e. RR* )
159	158	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` F ) e. RR* )
160		0nrp 11331	. . . . . . . . . . . . . . . . . . 19 |- -. 0 e. RR+
161		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
162	119, 32	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
163	162	adantrr 722	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
164	163	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
165	161, 139	syl6eqelr 2537	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR )
166	65, 138	elrpd 11335	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR+ )
167	166	adantrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. RR+ )
168	167	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( 1 / k ) e. RR+ )
169		itg2const2 22692	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol /\ ( 1 / k ) e. RR+ ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR ) )
170	164, 168, 169	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR ) )
171	165, 170	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR )
172		elrege0 11735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. ( 0 [,) +oo ) <-> ( ( 1 / k ) e. RR /\ 0 <_ ( 1 / k ) ) )
173	65, 142, 172	sylanbrc 669	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
174	173	adantrr 722	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
175	174	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
176		itg2const 22691	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol /\ ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR /\ ( 1 / k ) e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) = ( ( 1 / k ) x. ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
177	164, 171, 175, 176	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) = ( ( 1 / k ) x. ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
178	161, 177	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> 0 = ( ( 1 / k ) x. ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
179		simplrr 770	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
180	171, 179	elrpd 11335	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR+ )
181	168, 180	rpmulcld 11354	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> ( ( 1 / k ) x. ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) e. RR+ )
182	178, 181	eqeltrd 2528	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) /\ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) -> 0 e. RR+ )
183	182	ex 436	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) -> 0 e. RR+ ) )
184	160, 183	mtoi 182	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> -. 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
185		itg2ge0 22686	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
186	151, 185	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
187		xrleloe 11440	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 e. RR* /\ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR* ) -> ( 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) <-> ( 0 < ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) \/ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) ) )
188	42, 153, 187	sylancr 668	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) <-> ( 0 < ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) \/ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) ) )
189	186, 188	mpbid 214	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 0 < ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) \/ 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) )
190	189	ord 379	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( -. 0 < ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) -> 0 = ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) ) )
191	184, 190	mt3d 129	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 < ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
192	156	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> F : RR --> ( 0 [,] +oo ) )
193	65	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR )
194	58	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. NN ) -> F Fn RR )
195	194, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
196	195	biimpa 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) )
197	196	simpld 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> x e. RR )
198	52	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
199	197, 198	syldan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. RR )
200	66	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR* )
201	196	simprd 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. ( ( 1 / k ) (,) +oo ) )
202		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) -> ( 1 / k ) < ( F ` x ) )
203	68, 202	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) -> ( 1 / k ) < ( F ` x ) ) )
204	200, 201, 203	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) < ( F ` x ) )
205	193, 199, 204	ltled 9780	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) <_ ( F ` x ) )
206	51	simprd 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
207	206	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
208	197, 207	syldan 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
209		breq1 4404	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 / k ) = if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) -> ( ( 1 / k ) <_ ( F ` x ) <-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) ) )
210		breq1 4404	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 = if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) -> ( 0 <_ ( F ` x ) <-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) ) )
211	209, 210	ifboth 3916	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 1 / k ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
212	205, 208, 211	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
213	212	adantlr 720	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
214		iffalse 3889	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
215	214	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
216	207	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
217	215, 216	eqbrtrd 4422	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
218	213, 217	pm2.61dan 799	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
219	218	ralrimiva 2801	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
220	219	adantrr 722	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
221	10	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> RR e. _V )
222		ovex 6316	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 / k ) e. _V
223		c0ex 9634	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. _V
224	222, 223	ifex 3948	. . . . . . . . . . . . . . . . . . . . . 22 |- if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. _V
225	224	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. _V )
226		fvex 5873	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F ` x ) e. _V
227	226	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. _V )
228		eqidd 2451	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) = ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) )
229	9	feqmptd 5916	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
230	221, 225, 227, 228, 229	ofrfval2 6546	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) oR <_ F <-> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) ) )
231	230	biimpar 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) oR <_ F )
232	220, 231	syldan 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) oR <_ F )
233		itg2le 22690	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ F : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) oR <_ F ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) <_ ( S.2 ` F ) )
234	151, 192, 232, 233	syl3anc 1267	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) <_ ( S.2 ` F ) )
235	136, 153, 159, 191, 234	xrltletrd 11455	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 < ( S.2 ` F ) )
236	235	expr 619	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 < ( S.2 ` F ) ) )
237	236	con3d 139	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
238	4	ffvelrni 6019	. . . . . . . . . . . . . . . . 17 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. ( 0 [,] +oo ) )
239	3, 238	sseldi 3429	. . . . . . . . . . . . . . . 16 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
240	162, 239	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
241		xrlenlt 9696	. . . . . . . . . . . . . . 15 |- ( ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
242	240, 42, 241	sylancl 667	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
243	237, 242	sylibrd 238	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 ) )
244	243	imp 431	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
245	244	an32s 812	. . . . . . . . . . 11 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
246	135, 245	eqbrtrd 4422	. . . . . . . . . 10 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
247	246	ralrimiva 2801	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
248		fveq2 5863	. . . . . . . . . . . . 13 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( vol ` z ) = ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
249	248	breq1d 4411	. . . . . . . . . . . 12 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( ( vol ` z ) <_ 0 <-> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
250	249	ralrn 6023	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 <-> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
251	19, 20, 250	3syl 18	. . . . . . . . . 10 |- ( ph -> ( A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 <-> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
252	251	adantr 467	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 <-> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
253	247, 252	mpbird 236	. . . . . . . 8 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 )
254		ffn 5726	. . . . . . . . . 10 |- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
255	4, 254	ax-mp 5	. . . . . . . . 9 |- vol Fn dom vol
256		frn 5733	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
257	31, 256	syl 17	. . . . . . . . . 10 |- ( ph -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
258	257	adantr 467	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
259		breq1 4404	. . . . . . . . . 10 |- ( x = ( vol ` z ) -> ( x <_ 0 <-> ( vol ` z ) <_ 0 ) )
260	259	ralima 6143	. . . . . . . . 9 |- ( ( vol Fn dom vol /\ ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol ) -> ( A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 <-> A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 ) )
261	255, 258, 260	sylancr 668	. . . . . . . 8 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 <-> A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 ) )
262	253, 261	mpbird 236	. . . . . . 7 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 )
263		imassrn 5178	. . . . . . . . 9 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ ran vol
264		frn 5733	. . . . . . . . . . 11 |- ( vol : dom vol --> ( 0 [,] +oo ) -> ran vol C_ ( 0 [,] +oo ) )
265	4, 264	ax-mp 5	. . . . . . . . . 10 |- ran vol C_ ( 0 [,] +oo )
266	265, 3	sstri 3440	. . . . . . . . 9 |- ran vol C_ RR*
267	263, 266	sstri 3440	. . . . . . . 8 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ RR*
268		supxrleub 11609	. . . . . . . 8 |- ( ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ RR* /\ 0 e. RR* ) -> ( sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 <-> A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 ) )
269	267, 42, 268	mp2an 677	. . . . . . 7 |- ( sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 <-> A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 )
270	262, 269	sylibr 216	. . . . . 6 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 )
271	132, 270	eqbrtrd 4422	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) <_ 0 )
272	8, 41, 43, 97, 271	xrletrd 11456	. . . 4 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ 0 )
273	272	ex 436	. . 3 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> ( vol ` A ) <_ 0 ) )
274		xrlenlt 9696	. . . 4 |- ( ( ( vol ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
275	7, 42, 274	sylancl 667	. . 3 |- ( ph -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
276	273, 275	sylibd 218	. 2 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` A ) ) )
277	1, 276	mt4d 144	1 |- ( ph -> 0 < ( S.2 ` F ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   = wceq 1443   e. wcel 1886   A.wral 2736   E.wrex 2737   _Vcvv 3044   C_ wss 3403   ifcif 3880   U.cuni 4197   U_ciun 4277   class class class wbr 4401   |-> cmpt 4460   `'ccnv 4832   dom cdm 4833   ran crn 4834   "cima 4836   Fn wfn 5576   -->wf 5577   ` cfv 5581  (class class class)co 6288   oRcofr 6527   supcsup 7951   RRcr 9535   0cc0 9536   1c1 9537   + caddc 9539   x. cmul 9541   +oocpnf 9669   RR*cxr 9671   < clt 9672   <_ cle 9673   / cdiv 10266   NNcn 10606   RR+crp 11299   (,)cioo 11632   [,)cico 11634   [,]cicc 11635   vol*covol 22406   volcvol 22408  MblFncmbf 22565   S.2citg2 22567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cc 8862  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614  ax-addf 9615

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-disj 4373  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-ofr 6529  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fi 7922  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-q 11262  df-rp 11300  df-xneg 11406  df-xadd 11407  df-xmul 11408  df-ioo 11636  df-ico 11638  df-icc 11639  df-fz 11782  df-fzo 11913  df-fl 12025  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-rlim 13546  df-sum 13746  df-rest 15314  df-topgen 15335  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-top 19914  df-bases 19915  df-topon 19916  df-cmp 20395  df-cncf 21903  df-ovol 22409  df-vol 22411  df-mbf 22570  df-itg1 22571  df-itg2 22572  df-0p 22621

This theorem is referenced by:  itggt0  22792