Theorem itg2gt0 22704

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 11717	. . . . . . . 8 |- ( 0 [,] +oo ) C_ RR*
4		volf 22469	. . . . . . . . 9 |- vol : dom vol --> ( 0 [,] +oo )
5	4	ffvelrni 6032	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
6	3, 5	sseldi 3462	. . . . . . 7 |- ( A e. dom vol -> ( vol ` A ) e. RR* )
7	2, 6	syl 17	. . . . . 6 |- ( ph -> ( vol ` A ) e. RR* )
8	7	adantr 466	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) e. RR* )
9		itg2gt0.3	. . . . . . . . . . . . . . . 16 |- ( ph -> F : RR --> ( 0 [,) +oo ) )
10		reex 9630	. . . . . . . . . . . . . . . 16 |- RR e. _V
11		fex 6149	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ RR e. _V ) -> F e. _V )
12	9, 10, 11	sylancl 666	. . . . . . . . . . . . . . 15 |- ( ph -> F e. _V )
13		cnvexg 6749	. . . . . . . . . . . . . . 15 |- ( F e. _V -> `' F e. _V )
14	12, 13	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> `' F e. _V )
15		imaexg 6740	. . . . . . . . . . . . . 14 |- ( `' F e. _V -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
16	14, 15	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
17	16	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
18		eqid 2422	. . . . . . . . . . . 12 |- ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) = ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) )
19	17, 18	fmptd 6057	. . . . . . . . . . 11 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V )
20		ffn 5742	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
21	19, 20	syl 17	. . . . . . . . . 10 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
22		fniunfv 6163	. . . . . . . . . 10 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
23	21, 22	syl 17	. . . . . . . . 9 |- ( ph -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
24		itg2gt0.4	. . . . . . . . . . . . . . 15 |- ( ph -> F e. MblFn )
25		rge0ssre 11740	. . . . . . . . . . . . . . . 16 |- ( 0 [,) +oo ) C_ RR
26		fss 5750	. . . . . . . . . . . . . . . 16 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
27	9, 25, 26	sylancl 666	. . . . . . . . . . . . . . 15 |- ( ph -> F : RR --> RR )
28		mbfima 22574	. . . . . . . . . . . . . . 15 |- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
29	24, 27, 28	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
30	29	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
31	30, 18	fmptd 6057	. . . . . . . . . . . 12 |- ( ph -> ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol )
32	31	ffvelrnda 6033	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
33	32	ralrimiva 2839	. . . . . . . . . 10 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
34		iunmbl 22492	. . . . . . . . . 10 |- ( A. k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
35	33, 34	syl 17	. . . . . . . . 9 |- ( ph -> U_ k e. NN ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
36	23, 35	eqeltrrd 2511	. . . . . . . 8 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol )
37		mblss 22471	. . . . . . . 8 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
38	36, 37	syl 17	. . . . . . 7 |- ( ph -> U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
39		ovolcl 22417	. . . . . . 7 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
40	38, 39	syl 17	. . . . . 6 |- ( ph -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
41	40	adantr 466	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
42		0xr 9687	. . . . . 6 |- 0 e. RR*
43	42	a1i 11	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> 0 e. RR* )
44		mblvol 22470	. . . . . . . 8 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
45	2, 44	syl 17	. . . . . . 7 |- ( ph -> ( vol ` A ) = ( vol* ` A ) )
46		mblss 22471	. . . . . . . . . . . . . . . 16 |- ( A e. dom vol -> A C_ RR )
47	2, 46	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ RR )
48	47	sselda 3464	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. RR )
49	9	ffvelrnda 6033	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
50		elrege0 11738	. . . . . . . . . . . . . . . 16 |- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
51	49, 50	sylib 199	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
52	51	simpld 460	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
53	48, 52	syldan 472	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
54		itg2gt0.5	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )
55		nnrecl 10867	. . . . . . . . . . . . 13 |- ( ( ( F ` x ) e. RR /\ 0 < ( F ` x ) ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
56	53, 54, 55	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
57		ffn 5742	. . . . . . . . . . . . . . . . . 18 |- ( F : RR --> ( 0 [,) +oo ) -> F Fn RR )
58	9, 57	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> F Fn RR )
59	58	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> F Fn RR )
60		elpreima 6013	. . . . . . . . . . . . . . . 16 |- ( F Fn RR -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
62	48	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> x e. RR )
63	62	biantrurd 510	. . . . . . . . . . . . . . 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 10646	. . . . . . . . . . . . . . . . . . 19 |- ( k e. NN -> ( 1 / k ) e. RR )
65	64	adantl 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR )
66	65	rexrd 9690	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR* )
67	66	adantlr 719	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( 1 / k ) e. RR* )
68		elioopnf 11728	. . . . . . . . . . . . . . . 16 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
69	67, 68	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
70	61, 63, 69	3bitr2d 284	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
71		id 23	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. NN )
72		imaexg 6740	. . . . . . . . . . . . . . . . . 18 |- ( `' F e. _V -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
73	14, 72	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
74	73	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
75		oveq2 6309	. . . . . . . . . . . . . . . . . . 19 |- ( n = k -> ( 1 / n ) = ( 1 / k ) )
76	75	oveq1d 6316	. . . . . . . . . . . . . . . . . 18 |- ( n = k -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / k ) (,) +oo ) )
77	76	imaeq2d 5183	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
78	77, 18	fvmptg 5958	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
80	79	eleq2d 2492	. . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( F ` x ) e. RR )
82	81	biantrurd 510	. . . . . . . . . . . . . 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 289	. . . . . . . . . . . . 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 2936	. . . . . . . . . . . 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 213	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) )
86	85	ex 435	. . . . . . . . . 10 |- ( ph -> ( x e. A -> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
87		eluni2 4220	. . . . . . . . . . 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 2495	. . . . . . . . . . . . 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 6035	. . . . . . . . . . . 12 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN -> ( E. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) x e. z <-> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
90	21, 89	syl 17	. . . . . . . . . . 11 |- ( ph -> ( E. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) x e. z <-> E. k e. NN x e. ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
91	87, 90	syl5bb 260	. . . . . . . . . 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 237	. . . . . . . . 9 |- ( ph -> ( x e. A -> x e. U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
93	92	ssrdv 3470	. . . . . . . 8 |- ( ph -> A C_ U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
94		ovolss 22424	. . . . . . . 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 665	. . . . . . 7 |- ( ph -> ( vol* ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
96	45, 95	eqbrtrd 4441	. . . . . 6 |- ( ph -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
97	96	adantr 466	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
98		mblvol 22470	. . . . . . . . 9 |- ( U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
99	36, 98	syl 17	. . . . . . . 8 |- ( ph -> ( vol ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
100		peano2nn 10621	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( k + 1 ) e. NN )
101	100	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
102		nnrecre 10646	. . . . . . . . . . . . . . 15 |- ( ( k + 1 ) e. NN -> ( 1 / ( k + 1 ) ) e. RR )
103	101, 102	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR )
104	103	rexrd 9690	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR* )
105		nnre 10616	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. RR )
106	105	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> k e. RR )
107	106	lep1d 10538	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> k <_ ( k + 1 ) )
108		nngt0 10638	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> 0 < k )
109	108	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < k )
110	101	nnred 10624	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
111	101	nngt0d 10653	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> 0 < ( k + 1 ) )
112		lerec 10489	. . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
114	107, 113	mpbid 213	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) )
115		iooss1 11671	. . . . . . . . . . . . 13 |- ( ( ( 1 / ( k + 1 ) ) e. RR* /\ ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
116	104, 114, 115	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
117		imass2 5219	. . . . . . . . . . . 12 |- ( ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
118	116, 117	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
119	71, 73, 78	syl2anr 480	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
120		imaexg 6740	. . . . . . . . . . . . 13 |- ( `' F e. _V -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
121	14, 120	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
122		oveq2 6309	. . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( 1 / n ) = ( 1 / ( k + 1 ) ) )
123	122	oveq1d 6316	. . . . . . . . . . . . . 14 |- ( n = ( k + 1 ) -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / ( k + 1 ) ) (,) +oo ) )
124	123	imaeq2d 5183	. . . . . . . . . . . . 13 |- ( n = ( k + 1 ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
125	124, 18	fvmptg 5958	. . . . . . . . . . . 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 480	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
127	118, 119, 126	3sstr4d 3507	. . . . . . . . . 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 2839	. . . . . . . . 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 22495	. . . . . . . . 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 665	. . . . . . . 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 2465	. . . . . . 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 466	. . . . . 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 466	. . . . . . . . . . . . 13 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
134	71, 133, 78	syl2anr 480	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
135	134	fveq2d 5881	. . . . . . . . . . 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 10647	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. NN -> 0 < ( 1 / k ) )
138	137	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN ) -> 0 < ( 1 / k ) )
139		0re 9643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. RR
140		ltle 9722	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 0 e. RR /\ ( 1 / k ) e. RR ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
141	139, 65, 140	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . 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 11741	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 / k ) e. ( 0 [,] +oo ) <-> ( ( 1 / k ) e. RR* /\ 0 <_ ( 1 / k ) ) )
144	66, 142, 143	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,] +oo ) )
145		0e0iccpnf 11743	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. ( 0 [,] +oo )
146		ifcl 3951	. . . . . . . . . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
148	147	adantr 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
149		eqid 2422	. . . . . . . . . . . . . . . . . . . 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 6057	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
151	150	adantrr 721	. . . . . . . . . . . . . . . . . 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 22676	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR* )
153	151, 152	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) e. RR* )
154		icossicc 11721	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
155		fss 5750	. . . . . . . . . . . . . . . . . . . 20 |- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
156	9, 154, 155	sylancl 666	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
157		itg2cl 22676	. . . . . . . . . . . . . . . . . . 19 |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S.2 ` F ) e. RR* )
159	158	adantr 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` F ) e. RR* )
160		0nrp 11334	. . . . . . . . . . . . . . . . . . 19 |- -. 0 e. RR+
161		simpr 462	. . . . . . . . . . . . . . . . . . . . . 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 2511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
163	162	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
164	163	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 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 2519	. . . . . . . . . . . . . . . . . . . . . . . 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 11338	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR+ )
167	166	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. RR+ )
168	167	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 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 22685	. . . . . . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . . . . 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 11738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. ( 0 [,) +oo ) <-> ( ( 1 / k ) e. RR /\ 0 <_ ( 1 / k ) ) )
173	65, 142, 172	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
174	173	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
175	174	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 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 22684	. . . . . . . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . . . . 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 11338	. . . . . . . . . . . . . . . . . . . . . 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 11357	. . . . . . . . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . 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 181	. . . . . . . . . . . . . . . . . 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 22679	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
186	151, 185	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 <_ ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) ) )
187		xrleloe 11443	. . . . . . . . . . . . . . . . . . . . 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 667	. . . . . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . . . . 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 378	. . . . . . . . . . . . . . . . . 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 128	. . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> F : RR --> ( 0 [,] +oo ) )
193	65	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR )
194	58	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. NN ) -> F Fn RR )
195	194, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
196	195	biimpa 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) )
197	196	simpld 460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> x e. RR )
198	52	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
199	197, 198	syldan 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. RR )
200	66	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR* )
201	196	simprd 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. ( ( 1 / k ) (,) +oo ) )
202		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) -> ( 1 / k ) < ( F ` x ) )
203	68, 202	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) -> ( 1 / k ) < ( F ` x ) ) )
204	200, 201, 203	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) < ( F ` x ) )
205	193, 199, 204	ltled 9783	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) <_ ( F ` x ) )
206	51	simprd 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
207	206	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
208	197, 207	syldan 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
209		breq1 4423	. . . . . . . . . . . . . . . . . . . . . . . . 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 4423	. . . . . . . . . . . . . . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . . . . 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 719	. . . . . . . . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
215	214	adantl 467	. . . . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
217	215, 216	eqbrtrd 4441	. . . . . . . . . . . . . . . . . . . . . 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 798	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
219	218	ralrimiva 2839	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
220	219	adantrr 721	. . . . . . . . . . . . . . . . . . 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 6329	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 / k ) e. _V
223		c0ex 9637	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. _V
224	222, 223	ifex 3977	. . . . . . . . . . . . . . . . . . . . . 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 5887	. . . . . . . . . . . . . . . . . . . . . 22 |- ( F ` x ) e. _V
227	226	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. _V )
228		eqidd 2423	. . . . . . . . . . . . . . . . . . . . 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 5930	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
230	221, 225, 227, 228, 229	ofrfval2 6559	. . . . . . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . . 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 22683	. . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . 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 11458	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 < ( S.2 ` F ) )
236	235	expr 618	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 < ( S.2 ` F ) ) )
237	236	con3d 138	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
238	4	ffvelrni 6032	. . . . . . . . . . . . . . . . 17 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. ( 0 [,] +oo ) )
239	3, 238	sseldi 3462	. . . . . . . . . . . . . . . 16 |- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
240	162, 239	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
241		xrlenlt 9699	. . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
243	237, 242	sylibrd 237	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 ) )
244	243	imp 430	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
245	244	an32s 811	. . . . . . . . . . 11 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
246	135, 245	eqbrtrd 4441	. . . . . . . . . 10 |- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
247	246	ralrimiva 2839	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
248		fveq2 5877	. . . . . . . . . . . . 13 |- ( z = ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( vol ` z ) = ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
249	248	breq1d 4430	. . . . . . . . . . . 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 6036	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 <-> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
251	19, 20, 250	3syl 18	. . . . . . . . . 10 |- ( ph -> ( A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 <-> A. k e. NN ( vol ` ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
252	251	adantr 466	. . . . . . . . 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 235	. . . . . . . 8 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. z e. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 )
254		ffn 5742	. . . . . . . . . 10 |- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
255	4, 254	ax-mp 5	. . . . . . . . 9 |- vol Fn dom vol
256		frn 5748	. . . . . . . . . . 11 |- ( ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
257	31, 256	syl 17	. . . . . . . . . 10 |- ( ph -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
258	257	adantr 466	. . . . . . . . 9 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
259		breq1 4423	. . . . . . . . . 10 |- ( x = ( vol ` z ) -> ( x <_ 0 <-> ( vol ` z ) <_ 0 ) )
260	259	ralima 6156	. . . . . . . . 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 667	. . . . . . . 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 235	. . . . . . 7 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. x e. ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 )
263		imassrn 5194	. . . . . . . . 9 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ ran vol
264		frn 5748	. . . . . . . . . . 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 3473	. . . . . . . . 9 |- ran vol C_ RR*
267	263, 266	sstri 3473	. . . . . . . 8 |- ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ RR*
268		supxrleub 11612	. . . . . . . 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 676	. . . . . . 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 215	. . . . . 6 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> sup ( ( vol " ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 )
271	132, 270	eqbrtrd 4441	. . . . 5 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN |-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) <_ 0 )
272	8, 41, 43, 97, 271	xrletrd 11459	. . . 4 |- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ 0 )
273	272	ex 435	. . 3 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> ( vol ` A ) <_ 0 ) )
274		xrlenlt 9699	. . . 4 |- ( ( ( vol ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
275	7, 42, 274	sylancl 666	. . 3 |- ( ph -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
276	273, 275	sylibd 217	. 2 |- ( ph -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` A ) ) )
277	1, 276	mt4d 143	1 |- ( ph -> 0 < ( S.2 ` F ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   = wceq 1437   e. wcel 1868   A.wral 2775   E.wrex 2776   _Vcvv 3081   C_ wss 3436   ifcif 3909   U.cuni 4216   U_ciun 4296   class class class wbr 4420   |-> cmpt 4479   `'ccnv 4848   dom cdm 4849   ran crn 4850   "cima 4852   Fn wfn 5592   -->wf 5593   ` cfv 5597  (class class class)co 6301   oRcofr 6540   supcsup 7956   RRcr 9538   0cc0 9539   1c1 9540   + caddc 9542   x. cmul 9544   +oocpnf 9672   RR*cxr 9674   < clt 9675   <_ cle 9676   / cdiv 10269   NNcn 10609   RR+crp 11302   (,)cioo 11635   [,)cico 11637   [,]cicc 11638   vol*covol 22399   volcvol 22401  MblFncmbf 22558   S.2citg2 22560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cc 8865  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-disj 4392  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-ofr 6542  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fi 7927  df-sup 7958  df-inf 7959  df-oi 8027  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12027  df-seq 12213  df-exp 12272  df-hash 12515  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-clim 13539  df-rlim 13540  df-sum 13740  df-rest 15308  df-topgen 15329  df-psmet 18949  df-xmet 18950  df-met 18951  df-bl 18952  df-mopn 18953  df-top 19907  df-bases 19908  df-topon 19909  df-cmp 20388  df-cncf 21896  df-ovol 22402  df-vol 22404  df-mbf 22563  df-itg1 22564  df-itg2 22565  df-0p 22614

This theorem is referenced by:  itggt0  22785