Theorem itg2gt0 21930

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 11607	. . . . . . . 8 |- ( 0 [,] +oo ) C_ RR*
4		volf 21703	. . . . . . . . 9 |- vol : dom vol --> ( 0 [,] +oo )
5	4	ffvelrni 6020	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
6	3, 5	sseldi 3502	. . . . . . 7 |- ( A e. dom vol -> ( vol ` A ) e. RR* )
7	2, 6	syl 16	. . . . . 6 |- ( ph -> ( vol ` A ) e. RR* )
8	7	adantr 465	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) e. RR* )
9		itg2gt0.3	. . . . . . . . . . . . . . . 16 |- ( ph -> F : RR --> ( 0 [,) +oo ) )
10		reex 9583	. . . . . . . . . . . . . . . 16 |- RR e. _V
11		fex 6133	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ RR e. _V ) -> F e. _V )
12	9, 10, 11	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ph -> F e. _V )
13		cnvexg 6730	. . . . . . . . . . . . . . 15 |- ( F e. _V -> `' F e. _V )
14	12, 13	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> `' F e. _V )
15		imaexg 6721	. . . . . . . . . . . . . 14 |- ( `' F e. _V -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
16	14, 15	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
17	16	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
18		eqid 2467	. . . . . . . . . . . 12 |- ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) = ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) )
19	17, 18	fmptd 6045	. . . . . . . . . . 11 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V )
20		ffn 5731	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
21	19, 20	syl 16	. . . . . . . . . 10 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
22		fniunfv 6147	. . . . . . . . . 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 16	. . . . . . . . 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		0re 9596	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
26		pnfxr 11321	. . . . . . . . . . . . . . . . 17 |- +oo e. RR*
27		icossre 11605	. . . . . . . . . . . . . . . . 17 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
28	25, 26, 27	mp2an 672	. . . . . . . . . . . . . . . 16 |- ( 0 [,) +oo ) C_ RR
29		fss 5739	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
30	9, 28, 29	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ph -> F : RR --> RR )
31		mbfima 21802	. . . . . . . . . . . . . . 15 |- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
32	24, 30, 31	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
33	32	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
34	33, 18	fmptd 6045	. . . . . . . . . . . 12 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol )
35	34	ffvelrnda 6021	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
36	35	ralrimiva 2878	. . . . . . . . . 10 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
37		iunmbl 21726	. . . . . . . . . 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 )
38	36, 37	syl 16	. . . . . . . . 9 |- ( ph -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
39	23, 38	eqeltrrd 2556	. . . . . . . 8 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol )
40		mblss 21705	. . . . . . . 8 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
41	39, 40	syl 16	. . . . . . 7 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
42		ovolcl 21652	. . . . . . 7 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
43	41, 42	syl 16	. . . . . 6 |- ( ph -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
44	43	adantr 465	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
45		0xr 9640	. . . . . 6 |- 0 e. RR*
46	45	a1i 11	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> 0 e. RR* )
47		mblvol 21704	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
48	2, 47	syl 16	. . . . . . 7 |- ( ph -> ( vol ` A ) = ( vol* ` A ) )
49		mblss 21705	. . . . . . . . . . . . . . . 16 |- ( A e. dom vol -> A C_ RR )
50	2, 49	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ RR )
51	50	sselda 3504	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. RR )
52	9	ffvelrnda 6021	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
53		elrege0 11627	. . . . . . . . . . . . . . . 16 |- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
54	52, 53	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
55	54	simpld 459	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
56	51, 55	syldan 470	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
57		itg2gt0.5	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )
58		nnrecl 10793	. . . . . . . . . . . . 13 |- ( ( ( F ` x ) e. RR /\ 0 < ( F ` x ) ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
59	56, 57, 58	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
60		ffn 5731	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,) +oo ) -> F Fn RR )
61	9, 60	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> F Fn RR )
62	61	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> F Fn RR )
63		elpreima 6001	. . . . . . . . . . . . . . . 16 |- ( F Fn RR -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
64	62, 63	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
65	51	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> x e. RR )
66	65	biantrurd 508	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
67		nnrecre 10572	. . . . . . . . . . . . . . . . . . 19 |- ( k e. NN -> ( 1 / k ) e. RR )
68	67	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR )
69	68	rexrd 9643	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR* )
70	69	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( 1 / k ) e. RR* )
71		elioopnf 11618	. . . . . . . . . . . . . . . 16 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
72	70, 71	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
73	64, 66, 72	3bitr2d 281	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
74		id 22	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. NN )
75		imaexg 6721	. . . . . . . . . . . . . . . . . 18 |- ( `' F e. _V -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
76	14, 75	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
77	76	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
78		oveq2 6292	. . . . . . . . . . . . . . . . . . 19 |- ( n = k -> ( 1 / n ) = ( 1 / k ) )
79	78	oveq1d 6299	. . . . . . . . . . . . . . . . . 18 |- ( n = k -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / k ) (,) +oo ) )
80	79	imaeq2d 5337	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
81	80, 18	fvmptg 5948	. . . . . . . . . . . . . . . 16 |- ( ( k e. NN /\ ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
82	74, 77, 81	syl2anr 478	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
83	82	eleq2d 2537	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) <-> x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
84	56	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( F ` x ) e. RR )
85	84	biantrurd 508	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( 1 / k ) < ( F ` x ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
86	73, 83, 85	3bitr4rd 286	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( 1 / k ) < ( F ` x ) <-> x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
87	86	rexbidva 2970	. . . . . . . . . . . 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 ) ) )
88	59, 87	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) )
89	88	ex 434	. . . . . . . . . 10 |- ( ph -> ( x e. A -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
90		eluni2 4249	. . . . . . . . . . 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 )
91		eleq2 2540	. . . . . . . . . . . . 13 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( x e. z <-> x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
92	91	rexrn 6023	. . . . . . . . . . . 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 ) ) )
93	21, 92	syl 16	. . . . . . . . . . 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 ) ) )
94	90, 93	syl5bb 257	. . . . . . . . . 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 ) ) )
95	89, 94	sylibrd 234	. . . . . . . . 9 |- ( ph -> ( x e. A -> x e. U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
96	95	ssrdv 3510	. . . . . . . 8 |- ( ph -> A C_ U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
97		ovolss 21659	. . . . . . . 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 ) ) ) ) )
98	96, 41, 97	syl2anc 661	. . . . . . 7 |- ( ph -> ( vol* ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
99	48, 98	eqbrtrd 4467	. . . . . 6 |- ( ph -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
100	99	adantr 465	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
101		mblvol 21704	. . . . . . . . 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 ) ) ) ) )
102	39, 101	syl 16	. . . . . . . 8 |- ( ph -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
103		peano2nn 10548	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( k + 1 ) e. NN )
104	103	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
105		nnrecre 10572	. . . . . . . . . . . . . . 15 |- ( ( k + 1 ) e. NN -> ( 1 / ( k + 1 ) ) e. RR )
106	104, 105	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR )
107	106	rexrd 9643	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR* )
108		nnre 10543	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. RR )
109	108	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> k e. RR )
110	109	lep1d 10477	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> k <_ ( k + 1 ) )
111		nngt0 10565	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> 0 < k )
112	111	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < k )
113	104	nnred 10551	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
114	104	nngt0d 10579	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < ( k + 1 ) )
115		lerec 10427	. . . . . . . . . . . . . . 15 |- ( ( ( k e. RR /\ 0 < k ) /\ ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
116	109, 112, 113, 114, 115	syl22anc 1229	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
117	110, 116	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) )
118		iooss1 11564	. . . . . . . . . . . . 13 |- ( ( ( 1 / ( k + 1 ) ) e. RR* /\ ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
119	107, 117, 118	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
120		imass2 5372	. . . . . . . . . . . 12 |- ( ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
121	119, 120	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
122	74, 76, 81	syl2anr 478	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
123		imaexg 6721	. . . . . . . . . . . . 13 |- ( `' F e. _V -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
124	14, 123	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
125		oveq2 6292	. . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( 1 / n ) = ( 1 / ( k + 1 ) ) )
126	125	oveq1d 6299	. . . . . . . . . . . . . 14 |- ( n = ( k + 1 ) -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / ( k + 1 ) ) (,) +oo ) )
127	126	imaeq2d 5337	. . . . . . . . . . . . 13 |- ( n = ( k + 1 ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
128	127, 18	fvmptg 5948	. . . . . . . . . . . 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 ) ) )
129	103, 124, 128	syl2anr 478	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
130	121, 122, 129	3sstr4d 3547	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) )
131	130	ralrimiva 2878	. . . . . . . . 9 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) )
132		volsup 21729	. . . . . . . . 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* , < ) )
133	34, 131, 132	syl2anc 661	. . . . . . . 8 |- ( ph -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
134	102, 133	eqtr3d 2510	. . . . . . 7 |- ( ph -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
135	134	adantr 465	. . . . . 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* , < ) )
136	76	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
137	74, 136, 81	syl2anr 478	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
138	137	fveq2d 5870	. . . . . . . . . . 11 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) = ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
139	45	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 e. RR* )
140		nnrecgt0 10573	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. NN -> 0 < ( 1 / k ) )
141	140	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> 0 < ( 1 / k ) )
142		ltle 9673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 0 e. RR /\ ( 1 / k ) e. RR ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
143	25, 68, 142	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
144	141, 143	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. NN ) -> 0 <_ ( 1 / k ) )
145		elxrge0 11629	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 / k ) e. ( 0 [,] +oo ) <-> ( ( 1 / k ) e. RR* /\ 0 <_ ( 1 / k ) ) )
146	69, 144, 145	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,] +oo ) )
147		0e0iccpnf 11631	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. ( 0 [,] +oo )
148		ifcl 3981	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 1 / k ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
149	146, 147, 148	sylancl 662	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
150	149	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
151		eqid 2467	. . . . . . . . . . . . . . . . . . . 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 ) )
152	150, 151	fmptd 6045	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
153	152	adantrr 716	. . . . . . . . . . . . . . . . . 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 ) )
154		itg2cl 21902	. . . . . . . . . . . . . . . . . 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* )
155	153, 154	syl 16	. . . . . . . . . . . . . . . . 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* )
156		rexr 9639	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. RR -> x e. RR* )
157	156	anim1i 568	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. RR /\ 0 <_ x ) -> ( x e. RR* /\ 0 <_ x ) )
158		elrege0 11627	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
159		elxrge0 11629	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
160	157, 158, 159	3imtr4i 266	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( 0 [,) +oo ) -> x e. ( 0 [,] +oo ) )
161	160	ssriv 3508	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
162		fss 5739	. . . . . . . . . . . . . . . . . . . 20 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
163	9, 161, 162	sylancl 662	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
164		itg2cl 21902	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
165	163, 164	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S.2 ` F ) e. RR* )
166	165	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` F ) e. RR* )
167		0nrp 11250	. . . . . . . . . . . . . . . . . . 19 |- -. 0 e. RR+
168		simpr 461	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
169	122, 35	eqeltrrd 2556	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
170	169	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
171	170	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 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 )
172	168, 25	syl6eqelr 2564	. . . . . . . . . . . . . . . . . . . . . . . 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 )
173	68, 141	elrpd 11254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR+ )
174	173	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. RR+ )
175	174	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 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+ )
176		itg2const2 21911	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
177	171, 175, 176	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
178	172, 177	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . 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 )
179		elrege0 11627	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. ( 0 [,) +oo ) <-> ( ( 1 / k ) e. RR /\ 0 <_ ( 1 / k ) ) )
180	68, 144, 179	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
181	180	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
182	181	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
183		itg2const 21910	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
184	171, 178, 182, 183	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
185	168, 184	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
186		simplrr 760	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
187	178, 186	elrpd 11254	. . . . . . . . . . . . . . . . . . . . . 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+ )
188	175, 187	rpmulcld 11272	. . . . . . . . . . . . . . . . . . . . 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+ )
189	185, 188	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . 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+ )
190	189	ex 434	. . . . . . . . . . . . . . . . . . 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+ ) )
191	167, 190	mtoi 178	. . . . . . . . . . . . . . . . . 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 ) ) ) )
192		itg2ge0 21905	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
193	153, 192	syl 16	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
194		xrleloe 11350	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
195	45, 155, 194	sylancr 663	. . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
196	193, 195	mpbid 210	. . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
197	196	ord 377	. . . . . . . . . . . . . . . . . 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 ) ) ) ) )
198	191, 197	mt3d 125	. . . . . . . . . . . . . . . . 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 ) ) ) )
199	163	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> F : RR --> ( 0 [,] +oo ) )
200	68	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR )
201	61	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. NN ) -> F Fn RR )
202	201, 63	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
203	202	biimpa 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) )
204	203	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> x e. RR )
205	55	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
206	204, 205	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. RR )
207	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR* )
208	203	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. ( ( 1 / k ) (,) +oo ) )
209		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) -> ( 1 / k ) < ( F ` x ) )
210	71, 209	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) -> ( 1 / k ) < ( F ` x ) ) )
211	207, 208, 210	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) < ( F ` x ) )
212	200, 206, 211	ltled 9732	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) <_ ( F ` x ) )
213	54	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
214	213	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
215	204, 214	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
216		breq1 4450	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
217		breq1 4450	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
218	216, 217	ifboth 3975	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 1 / k ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
219	212, 215, 218	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
220	219	adantlr 714	. . . . . . . . . . . . . . . . . . . . . 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 ) )
221		iffalse 3948	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
222	221	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 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 )
223	214	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
224	222, 223	eqbrtrd 4467	. . . . . . . . . . . . . . . . . . . . . 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 ) )
225	220, 224	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
226	225	ralrimiva 2878	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
227	226	adantrr 716	. . . . . . . . . . . . . . . . . . 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 ) )
228	10	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> RR e. _V )
229		ovex 6309	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 / k ) e. _V
230		c0ex 9590	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. _V
231	229, 230	ifex 4008	. . . . . . . . . . . . . . . . . . . . . 22 |- if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. _V
232	231	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. _V )
233		fvex 5876	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F ` x ) e. _V
234	233	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. _V )
235		eqidd 2468	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
236	9	feqmptd 5920	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
237	228, 232, 234, 235, 236	ofrfval2 6541	. . . . . . . . . . . . . . . . . . . 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 ) ) )
238	237	biimpar 485	. . . . . . . . . . . . . . . . . . 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 )
239	227, 238	syldan 470	. . . . . . . . . . . . . . . . . 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 )
240		itg2le 21909	. . . . . . . . . . . . . . . . . 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 ) )
241	153, 199, 239, 240	syl3anc 1228	. . . . . . . . . . . . . . . . 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 ) )
242	139, 155, 166, 198, 241	xrltletrd 11364	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 < ( S.2 ` F ) )
243	242	expr 615	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 < ( S.2 ` F ) ) )
244	243	con3d 133	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
245	4	ffvelrni 6020	. . . . . . . . . . . . . . . . 17 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. ( 0 [,] +oo ) )
246	3, 245	sseldi 3502	. . . . . . . . . . . . . . . 16 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
247	169, 246	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
248		xrlenlt 9652	. . . . . . . . . . . . . . 15 |- ( ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
249	247, 45, 248	sylancl 662	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
250	244, 249	sylibrd 234	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 ) )
251	250	imp 429	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
252	251	an32s 802	. . . . . . . . . . 11 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
253	138, 252	eqbrtrd 4467	. . . . . . . . . 10 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
254	253	ralrimiva 2878	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
255		fveq2 5866	. . . . . . . . . . . . 13 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( vol ` z ) = ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
256	255	breq1d 4457	. . . . . . . . . . . 12 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( ( vol ` z ) <_ 0 <-> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
257	256	ralrn 6024	. . . . . . . . . . 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 ) )
258	19, 20, 257	3syl 20	. . . . . . . . . 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 ) )
259	258	adantr 465	. . . . . . . . 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 ) )
260	254, 259	mpbird 232	. . . . . . . 8 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 )
261		ffn 5731	. . . . . . . . . 10 |- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
262	4, 261	ax-mp 5	. . . . . . . . 9 |- vol Fn dom vol
263		frn 5737	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
264	34, 263	syl 16	. . . . . . . . . 10 |- ( ph -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
265	264	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
266		breq1 4450	. . . . . . . . . 10 |- ( x = ( vol ` z ) -> ( x <_ 0 <-> ( vol ` z ) <_ 0 ) )
267	266	ralima 6140	. . . . . . . . 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 ) )
268	262, 265, 267	sylancr 663	. . . . . . . 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 ) )
269	260, 268	mpbird 232	. . . . . . 7 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 )
270		imassrn 5348	. . . . . . . . 9 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ ran vol
271		frn 5737	. . . . . . . . . . 11 |- ( vol : dom vol --> ( 0 [,] +oo ) -> ran vol C_ ( 0 [,] +oo ) )
272	4, 271	ax-mp 5	. . . . . . . . . 10 |- ran vol C_ ( 0 [,] +oo )
273	272, 3	sstri 3513	. . . . . . . . 9 |- ran vol C_ RR*
274	270, 273	sstri 3513	. . . . . . . 8 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ RR*
275		supxrleub 11518	. . . . . . . 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 ) )
276	274, 45, 275	mp2an 672	. . . . . . 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 )
277	269, 276	sylibr 212	. . . . . 6 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 )
278	135, 277	eqbrtrd 4467	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) <_ 0 )
279	8, 44, 46, 100, 278	xrletrd 11365	. . . 4 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ 0 )
280	279	ex 434	. . 3 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> ( vol ` A ) <_ 0 ) )
281		xrlenlt 9652	. . . 4 |- ( ( ( vol ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
282	7, 45, 281	sylancl 662	. . 3 |- ( ph -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
283	280, 282	sylibd 214	. 2 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` A ) ) )
284	1, 283	mt4d 138	1 |- ( ph -> 0 < ( S.2 ` F ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1379   e. wcel 1767   A.wral 2814   E.wrex 2815   _Vcvv 3113   C_ wss 3476   ifcif 3939   U.cuni 4245   U_ciun 4325   class class class wbr 4447   |-> cmpt 4505   `'ccnv 4998   dom cdm 4999   ran crn 5000   "cima 5002   Fn wfn 5583   -->wf 5584   ` cfv 5588  (class class class)co 6284   oRcofr 6523   supcsup 7900   RRcr 9491   0cc0 9492   1c1 9493   + caddc 9495   x. cmul 9497   +oocpnf 9625   RR*cxr 9627   < clt 9628   <_ cle 9629   / cdiv 10206   NNcn 10536   RR+crp 11220   (,)cioo 11529   [,)cico 11531   [,]cicc 11532   vol*covol 21637   volcvol 21638  MblFncmbf 21786   S.2citg2 21788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-cc 8815  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570  ax-addf 9571

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-disj 4418  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-of 6524  df-ofr 6525  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fi 7871  df-sup 7901  df-oi 7935  df-card 8320  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-n0 10796  df-z 10865  df-uz 11083  df-q 11183  df-rp 11221  df-xneg 11318  df-xadd 11319  df-xmul 11320  df-ioo 11533  df-ico 11535  df-icc 11536  df-fz 11673  df-fzo 11793  df-fl 11897  df-seq 12076  df-exp 12135  df-hash 12374  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-clim 13274  df-rlim 13275  df-sum 13472  df-rest 14678  df-topgen 14699  df-psmet 18210  df-xmet 18211  df-met 18212  df-bl 18213  df-mopn 18214  df-top 19194  df-bases 19196  df-topon 19197  df-cmp 19681  df-cncf 21145  df-ovol 21639  df-vol 21640  df-mbf 21791  df-itg1 21792  df-itg2 21793  df-0p 21840

This theorem is referenced by:  itggt0  22011