Theorem itg2gt0 22293

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 11632	. . . . . . . 8 |- ( 0 [,] +oo ) C_ RR*
4		volf 22066	. . . . . . . . 9 |- vol : dom vol --> ( 0 [,] +oo )
5	4	ffvelrni 6031	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
6	3, 5	sseldi 3497	. . . . . . 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 9600	. . . . . . . . . . . . . . . 16 |- RR e. _V
11		fex 6146	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ RR e. _V ) -> F e. _V )
12	9, 10, 11	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ph -> F e. _V )
13		cnvexg 6745	. . . . . . . . . . . . . . 15 |- ( F e. _V -> `' F e. _V )
14	12, 13	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> `' F e. _V )
15		imaexg 6736	. . . . . . . . . . . . . 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 2457	. . . . . . . . . . . 12 |- ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) = ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) )
19	17, 18	fmptd 6056	. . . . . . . . . . 11 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V )
20		ffn 5737	. . . . . . . . . . 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 6160	. . . . . . . . . 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		rge0ssre 11653	. . . . . . . . . . . . . . . 16 |- ( 0 [,) +oo ) C_ RR
26		fss 5745	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
27	9, 25, 26	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ph -> F : RR --> RR )
28		mbfima 22165	. . . . . . . . . . . . . . 15 |- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
29	24, 27, 28	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
30	29	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
31	30, 18	fmptd 6056	. . . . . . . . . . . 12 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol )
32	31	ffvelrnda 6032	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
33	32	ralrimiva 2871	. . . . . . . . . 10 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
34		iunmbl 22089	. . . . . . . . . 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 16	. . . . . . . . 9 |- ( ph -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
36	23, 35	eqeltrrd 2546	. . . . . . . 8 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol )
37		mblss 22068	. . . . . . . 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 16	. . . . . . 7 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
39		ovolcl 22015	. . . . . . 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 16	. . . . . 6 |- ( ph -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
41	40	adantr 465	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
42		0xr 9657	. . . . . 6 |- 0 e. RR*
43	42	a1i 11	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> 0 e. RR* )
44		mblvol 22067	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
45	2, 44	syl 16	. . . . . . 7 |- ( ph -> ( vol ` A ) = ( vol* ` A ) )
46		mblss 22068	. . . . . . . . . . . . . . . 16 |- ( A e. dom vol -> A C_ RR )
47	2, 46	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ RR )
48	47	sselda 3499	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. RR )
49	9	ffvelrnda 6032	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
50		elrege0 11652	. . . . . . . . . . . . . . . 16 |- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
51	49, 50	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
52	51	simpld 459	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
53	48, 52	syldan 470	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
54		itg2gt0.5	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )
55		nnrecl 10814	. . . . . . . . . . . . 13 |- ( ( ( F ` x ) e. RR /\ 0 < ( F ` x ) ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
56	53, 54, 55	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
57		ffn 5737	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,) +oo ) -> F Fn RR )
58	9, 57	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> F Fn RR )
59	58	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> F Fn RR )
60		elpreima 6008	. . . . . . . . . . . . . . . 16 |- ( F Fn RR -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
61	59, 60	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 ) ) ) )
62	48	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> x e. RR )
63	62	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 ) ) ) )
64		nnrecre 10593	. . . . . . . . . . . . . . . . . . 19 |- ( k e. NN -> ( 1 / k ) e. RR )
65	64	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR )
66	65	rexrd 9660	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR* )
67	66	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( 1 / k ) e. RR* )
68		elioopnf 11643	. . . . . . . . . . . . . . . 16 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
69	67, 68	syl 16	. . . . . . . . . . . . . . 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 281	. . . . . . . . . . . . . 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 6736	. . . . . . . . . . . . . . . . . 18 |- ( `' F e. _V -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
73	14, 72	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
74	73	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
75		oveq2 6304	. . . . . . . . . . . . . . . . . . 19 |- ( n = k -> ( 1 / n ) = ( 1 / k ) )
76	75	oveq1d 6311	. . . . . . . . . . . . . . . . . 18 |- ( n = k -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / k ) (,) +oo ) )
77	76	imaeq2d 5347	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
78	77, 18	fvmptg 5954	. . . . . . . . . . . . . . . 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 478	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
80	79	eleq2d 2527	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( F ` x ) e. RR )
82	81	biantrurd 508	. . . . . . . . . . . . . 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 286	. . . . . . . . . . . . 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 2965	. . . . . . . . . . . 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 210	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) )
86	85	ex 434	. . . . . . . . . 10 |- ( ph -> ( x e. A -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
87		eluni2 4255	. . . . . . . . . . 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 2530	. . . . . . . . . . . . 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 6034	. . . . . . . . . . . 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 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 ) ) )
91	87, 90	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 ) ) )
92	86, 91	sylibrd 234	. . . . . . . . 9 |- ( ph -> ( x e. A -> x e. U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
93	92	ssrdv 3505	. . . . . . . 8 |- ( ph -> A C_ U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
94		ovolss 22022	. . . . . . . 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 661	. . . . . . 7 |- ( ph -> ( vol* ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
96	45, 95	eqbrtrd 4476	. . . . . 6 |- ( ph -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
97	96	adantr 465	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
98		mblvol 22067	. . . . . . . . 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 16	. . . . . . . 8 |- ( ph -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
100		peano2nn 10568	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( k + 1 ) e. NN )
101	100	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
102		nnrecre 10593	. . . . . . . . . . . . . . 15 |- ( ( k + 1 ) e. NN -> ( 1 / ( k + 1 ) ) e. RR )
103	101, 102	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR )
104	103	rexrd 9660	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR* )
105		nnre 10563	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. RR )
106	105	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> k e. RR )
107	106	lep1d 10497	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> k <_ ( k + 1 ) )
108		nngt0 10585	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> 0 < k )
109	108	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < k )
110	101	nnred 10571	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
111	101	nngt0d 10600	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < ( k + 1 ) )
112		lerec 10447	. . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
114	107, 113	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) )
115		iooss1 11589	. . . . . . . . . . . . 13 |- ( ( ( 1 / ( k + 1 ) ) e. RR* /\ ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
116	104, 114, 115	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
117		imass2 5382	. . . . . . . . . . . 12 |- ( ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
118	116, 117	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
119	71, 73, 78	syl2anr 478	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
120		imaexg 6736	. . . . . . . . . . . . 13 |- ( `' F e. _V -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
121	14, 120	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
122		oveq2 6304	. . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( 1 / n ) = ( 1 / ( k + 1 ) ) )
123	122	oveq1d 6311	. . . . . . . . . . . . . 14 |- ( n = ( k + 1 ) -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / ( k + 1 ) ) (,) +oo ) )
124	123	imaeq2d 5347	. . . . . . . . . . . . 13 |- ( n = ( k + 1 ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
125	124, 18	fvmptg 5954	. . . . . . . . . . . 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 478	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
127	118, 119, 126	3sstr4d 3542	. . . . . . . . . 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 2871	. . . . . . . . 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 22092	. . . . . . . . 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 661	. . . . . . . 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 2500	. . . . . . 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 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* , < ) )
133	73	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
134	71, 133, 78	syl2anr 478	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
135	134	fveq2d 5876	. . . . . . . . . . 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 10594	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. NN -> 0 < ( 1 / k ) )
138	137	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> 0 < ( 1 / k ) )
139		0re 9613	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. RR
140		ltle 9690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 0 e. RR /\ ( 1 / k ) e. RR ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
141	139, 65, 140	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . 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 11654	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 / k ) e. ( 0 [,] +oo ) <-> ( ( 1 / k ) e. RR* /\ 0 <_ ( 1 / k ) ) )
144	66, 142, 143	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,] +oo ) )
145		0e0iccpnf 11656	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. ( 0 [,] +oo )
146		ifcl 3986	. . . . . . . . . . . . . . . . . . . . . 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 662	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
148	147	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
149		eqid 2457	. . . . . . . . . . . . . . . . . . . 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 6056	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
151	150	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 ) )
152		itg2cl 22265	. . . . . . . . . . . . . . . . . 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 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* )
154		icossicc 11636	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
155		fss 5745	. . . . . . . . . . . . . . . . . . . 20 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
156	9, 154, 155	sylancl 662	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
157		itg2cl 22265	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
158	156, 157	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S.2 ` F ) e. RR* )
159	158	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` F ) e. RR* )
160		0nrp 11275	. . . . . . . . . . . . . . . . . . 19 |- -. 0 e. RR+
161		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 ) ) ) )
162	119, 32	eqeltrrd 2546	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
163	162	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
164	163	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 )
165	161, 139	syl6eqelr 2554	. . . . . . . . . . . . . . . . . . . . . . . 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 11279	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR+ )
167	166	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. RR+ )
168	167	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+ )
169		itg2const2 22274	. . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) )
171	165, 170	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 )
172		elrege0 11652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. ( 0 [,) +oo ) <-> ( ( 1 / k ) e. RR /\ 0 <_ ( 1 / k ) ) )
173	65, 142, 172	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
174	173	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
175	174	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 ) )
176		itg2const 22273	. . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) ) )
178	161, 177	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . . . 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 11279	. . . . . . . . . . . . . . . . . . . . . 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 11297	. . . . . . . . . . . . . . . . . . . . 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 2545	. . . . . . . . . . . . . . . . . . . 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 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+ ) )
184	160, 183	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 ) ) ) )
185		itg2ge0 22268	. . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) )
187		xrleloe 11375	. . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) ) ) )
189	186, 188	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 ) ) ) ) )
190	189	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 ) ) ) ) )
191	184, 190	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 ) ) ) )
192	156	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> F : RR --> ( 0 [,] +oo ) )
193	65	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR )
194	58	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. NN ) -> F Fn RR )
195	194, 60	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
196	195	biimpa 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) )
197	196	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> x e. RR )
198	52	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
199	197, 198	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. RR )
200	66	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR* )
201	196	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. ( ( 1 / k ) (,) +oo ) )
202		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) -> ( 1 / k ) < ( F ` x ) )
203	68, 202	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) -> ( 1 / k ) < ( F ` x ) ) )
204	200, 201, 203	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) < ( F ` x ) )
205	193, 199, 204	ltled 9750	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) <_ ( F ` x ) )
206	51	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
207	206	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
208	197, 207	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
209		breq1 4459	. . . . . . . . . . . . . . . . . . . . . . . . 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 4459	. . . . . . . . . . . . . . . . . . . . . . . . 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 3980	. . . . . . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . . . . . 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 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 ) )
214		iffalse 3953	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
215	214	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 )
216	207	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
217	215, 216	eqbrtrd 4476	. . . . . . . . . . . . . . . . . . . . . 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 791	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
219	218	ralrimiva 2871	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
220	219	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 ) )
221	10	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> RR e. _V )
222		ovex 6324	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 / k ) e. _V
223		c0ex 9607	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. _V
224	222, 223	ifex 4013	. . . . . . . . . . . . . . . . . . . . . 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 5882	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F ` x ) e. _V
227	226	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. _V )
228		eqidd 2458	. . . . . . . . . . . . . . . . . . . . 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 5926	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
230	221, 225, 227, 228, 229	ofrfval2 6556	. . . . . . . . . . . . . . . . . . . 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 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 )
232	220, 231	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 )
233		itg2le 22272	. . . . . . . . . . . . . . . . . 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 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 ) )
235	136, 153, 159, 191, 234	xrltletrd 11389	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 < ( S.2 ` F ) )
236	235	expr 615	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 < ( S.2 ` F ) ) )
237	236	con3d 133	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
238	4	ffvelrni 6031	. . . . . . . . . . . . . . . . 17 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. ( 0 [,] +oo ) )
239	3, 238	sseldi 3497	. . . . . . . . . . . . . . . 16 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
240	162, 239	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
241		xrlenlt 9669	. . . . . . . . . . . . . . 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 662	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
243	237, 242	sylibrd 234	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 ) )
244	243	imp 429	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
245	244	an32s 804	. . . . . . . . . . 11 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
246	135, 245	eqbrtrd 4476	. . . . . . . . . 10 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
247	246	ralrimiva 2871	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
248		fveq2 5872	. . . . . . . . . . . . 13 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( vol ` z ) = ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
249	248	breq1d 4466	. . . . . . . . . . . 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 6035	. . . . . . . . . . 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 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 ) )
252	251	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 ) )
253	247, 252	mpbird 232	. . . . . . . 8 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 )
254		ffn 5737	. . . . . . . . . 10 |- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
255	4, 254	ax-mp 5	. . . . . . . . 9 |- vol Fn dom vol
256		frn 5743	. . . . . . . . . . 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 16	. . . . . . . . . 10 |- ( ph -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
258	257	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
259		breq1 4459	. . . . . . . . . 10 |- ( x = ( vol ` z ) -> ( x <_ 0 <-> ( vol ` z ) <_ 0 ) )
260	259	ralima 6153	. . . . . . . . 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 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 ) )
262	253, 261	mpbird 232	. . . . . . 7 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 )
263		imassrn 5358	. . . . . . . . 9 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ ran vol
264		frn 5743	. . . . . . . . . . 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 3508	. . . . . . . . 9 |- ran vol C_ RR*
267	263, 266	sstri 3508	. . . . . . . 8 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ RR*
268		supxrleub 11543	. . . . . . . 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 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 )
270	262, 269	sylibr 212	. . . . . 6 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 )
271	132, 270	eqbrtrd 4476	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) <_ 0 )
272	8, 41, 43, 97, 271	xrletrd 11390	. . . 4 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ 0 )
273	272	ex 434	. . 3 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> ( vol ` A ) <_ 0 ) )
274		xrlenlt 9669	. . . 4 |- ( ( ( vol ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
275	7, 42, 274	sylancl 662	. . 3 |- ( ph -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
276	273, 275	sylibd 214	. 2 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` A ) ) )
277	1, 276	mt4d 138	1 |- ( ph -> 0 < ( S.2 ` F ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1395   e. wcel 1819   A.wral 2807   E.wrex 2808   _Vcvv 3109   C_ wss 3471   ifcif 3944   U.cuni 4251   U_ciun 4332   class class class wbr 4456   |-> cmpt 4515   `'ccnv 5007   dom cdm 5008   ran crn 5009   "cima 5011   Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6296   oRcofr 6538   supcsup 7918   RRcr 9508   0cc0 9509   1c1 9510   + caddc 9512   x. cmul 9514   +oocpnf 9642   RR*cxr 9644   < clt 9645   <_ cle 9646   / cdiv 10227   NNcn 10556   RR+crp 11245   (,)cioo 11554   [,)cico 11556   [,]cicc 11557   vol*covol 22000   volcvol 22001  MblFncmbf 22149   S.2citg2 22151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cc 8832  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587  ax-addf 9588

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-disj 4428  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-ofr 6540  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fi 7889  df-sup 7919  df-oi 7953  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-n0 10817  df-z 10886  df-uz 11107  df-q 11208  df-rp 11246  df-xneg 11343  df-xadd 11344  df-xmul 11345  df-ioo 11558  df-ico 11560  df-icc 11561  df-fz 11698  df-fzo 11822  df-fl 11932  df-seq 12111  df-exp 12170  df-hash 12409  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-clim 13323  df-rlim 13324  df-sum 13521  df-rest 14840  df-topgen 14861  df-psmet 18538  df-xmet 18539  df-met 18540  df-bl 18541  df-mopn 18542  df-top 19526  df-bases 19528  df-topon 19529  df-cmp 20014  df-cncf 21508  df-ovol 22002  df-vol 22003  df-mbf 22154  df-itg1 22155  df-itg2 22156  df-0p 22203

This theorem is referenced by:  itggt0  22374