itg2gt0

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)

	Ref	Expression
Hypotheses	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	itg2gt0	\|- ( ph -> 0 < ( S.2 ` F ) )

Proof

Step	Hyp	Ref	Expression
1		itg2gt0.1	\|- ( ph -> A e. dom vol )
2		itg2gt0.2	\|- ( ph -> 0 < ( vol ` A ) )
3		itg2gt0.3	\|- ( ph -> F : RR --> ( 0 [,) +oo ) )
4		itg2gt0.4	\|- ( ph -> F e. MblFn )
5		itg2gt0.5	\|- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )
6		iccssxr	\|- ( 0 [,] +oo ) C_ RR*
7		volf	\|- vol : dom vol --> ( 0 [,] +oo )
8	7	ffvelrni	\|- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
9	6 8	sselid	\|- ( A e. dom vol -> ( vol ` A ) e. RR* )
10	1 9	syl	\|- ( ph -> ( vol ` A ) e. RR* )
11	10	adantr	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) e. RR* )
12	4	elexd	\|- ( ph -> F e. _V )
13		cnvexg	\|- ( F e. _V -> `' F e. _V )
14	12 13	syl	\|- ( ph -> `' F e. _V )
15		imaexg	\|- ( `' F e. _V -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
16	14 15	syl	\|- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
17	16	adantr	\|- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. _V )
18	17	fmpttd	\|- ( ph -> ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V )
19	18	ffnd	\|- ( ph -> ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
20		fniunfv	\|- ( ( 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 ) ) ) )
21	19 20	syl	\|- ( ph -> U_ k e. NN ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
22		rge0ssre	\|- ( 0 [,) +oo ) C_ RR
23		fss	\|- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
24	3 22 23	sylancl	\|- ( ph -> F : RR --> RR )
25		mbfima	\|- ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
26	4 24 25	syl2anc	\|- ( ph -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
27	26	adantr	\|- ( ( ph /\ n e. NN ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) e. dom vol )
28	27	fmpttd	\|- ( ph -> ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> dom vol )
29	28	ffvelrnda	\|- ( ( ph /\ k e. NN ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
30	29	ralrimiva	\|- ( ph -> A. k e. NN ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
31		iunmbl	\|- ( 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 )
32	30 31	syl	\|- ( ph -> U_ k e. NN ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) e. dom vol )
33	21 32	eqeltrrd	\|- ( ph -> U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol )
34		mblss	\|- ( U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) e. dom vol -> U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
35	33 34	syl	\|- ( ph -> U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR )
36		ovolcl	\|- ( U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ RR -> ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
37	35 36	syl	\|- ( ph -> ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
38	37	adantr	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) e. RR* )
39		0xr	\|- 0 e. RR*
40	39	a1i	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> 0 e. RR* )
41		mblvol	\|- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
42	1 41	syl	\|- ( ph -> ( vol ` A ) = ( vol* ` A ) )
43		mblss	\|- ( A e. dom vol -> A C_ RR )
44	1 43	syl	\|- ( ph -> A C_ RR )
45	44	sselda	\|- ( ( ph /\ x e. A ) -> x e. RR )
46	3	ffvelrnda	\|- ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
47		elrege0	\|- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
48	46 47	sylib	\|- ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
49	48	simpld	\|- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
50	45 49	syldan	\|- ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
51		nnrecl	\|- ( ( ( F ` x ) e. RR /\ 0 < ( F ` x ) ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
52	50 5 51	syl2anc	\|- ( ( ph /\ x e. A ) -> E. k e. NN ( 1 / k ) < ( F ` x ) )
53	3	ffnd	\|- ( ph -> F Fn RR )
54	53	ad2antrr	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> F Fn RR )
55		elpreima	\|- ( F Fn RR -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
56	54 55	syl	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
57	45	adantr	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> x e. RR )
58	57	biantrurd	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
59		nnrecre	\|- ( k e. NN -> ( 1 / k ) e. RR )
60	59	adantl	\|- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR )
61	60	rexrd	\|- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR* )
62	61	adantlr	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( 1 / k ) e. RR* )
63		elioopnf	\|- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
64	62 63	syl	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
65	56 58 64	3bitr2d	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
66		id	\|- ( k e. NN -> k e. NN )
67		imaexg	\|- ( `' F e. _V -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
68	14 67	syl	\|- ( ph -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
69	68	adantr	\|- ( ( ph /\ x e. A ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
70		oveq2	\|- ( n = k -> ( 1 / n ) = ( 1 / k ) )
71	70	oveq1d	\|- ( n = k -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / k ) (,) +oo ) )
72	71	imaeq2d	\|- ( n = k -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
73		eqid	\|- ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) = ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) )
74	72 73	fvmptg	\|- ( ( k e. NN /\ ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
75	66 69 74	syl2anr	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
76	75	eleq2d	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( x e. ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) <-> x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
77	50	adantr	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( F ` x ) e. RR )
78	77	biantrurd	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( 1 / k ) < ( F ` x ) <-> ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) ) )
79	65 76 78	3bitr4rd	\|- ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( 1 / k ) < ( F ` x ) <-> x e. ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
80	79	rexbidva	\|- ( ( 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 ) ) )
81	52 80	mpbid	\|- ( ( ph /\ x e. A ) -> E. k e. NN x e. ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) )
82	81	ex	\|- ( ph -> ( x e. A -> E. k e. NN x e. ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
83		eluni2	\|- ( 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 )
84		eleq2	\|- ( z = ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( x e. z <-> x e. ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
85	84	rexrn	\|- ( ( 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 ) ) )
86	19 85	syl	\|- ( 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 ) ) )
87	83 86	syl5bb	\|- ( 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 ) ) )
88	82 87	sylibrd	\|- ( ph -> ( x e. A -> x e. U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
89	88	ssrdv	\|- ( ph -> A C_ U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) )
90		ovolss	\|- ( ( 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 ) ) ) ) )
91	89 35 90	syl2anc	\|- ( ph -> ( vol* ` A ) <_ ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
92	42 91	eqbrtrd	\|- ( ph -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
93	92	adantr	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
94		mblvol	\|- ( 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 ) ) ) ) )
95	33 94	syl	\|- ( ph -> ( vol ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) )
96		peano2nn	\|- ( k e. NN -> ( k + 1 ) e. NN )
97	96	adantl	\|- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
98		nnrecre	\|- ( ( k + 1 ) e. NN -> ( 1 / ( k + 1 ) ) e. RR )
99	97 98	syl	\|- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR )
100	99	rexrd	\|- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR* )
101		nnre	\|- ( k e. NN -> k e. RR )
102	101	adantl	\|- ( ( ph /\ k e. NN ) -> k e. RR )
103	102	lep1d	\|- ( ( ph /\ k e. NN ) -> k <_ ( k + 1 ) )
104		nngt0	\|- ( k e. NN -> 0 < k )
105	104	adantl	\|- ( ( ph /\ k e. NN ) -> 0 < k )
106	97	nnred	\|- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
107	97	nngt0d	\|- ( ( ph /\ k e. NN ) -> 0 < ( k + 1 ) )
108		lerec	\|- ( ( ( k e. RR /\ 0 < k ) /\ ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
109	102 105 106 107 108	syl22anc	\|- ( ( ph /\ k e. NN ) -> ( k <_ ( k + 1 ) <-> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) )
110	103 109	mpbid	\|- ( ( ph /\ k e. NN ) -> ( 1 / ( k + 1 ) ) <_ ( 1 / k ) )
111		iooss1	\|- ( ( ( 1 / ( k + 1 ) ) e. RR* /\ ( 1 / ( k + 1 ) ) <_ ( 1 / k ) ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
112	100 110 111	syl2anc	\|- ( ( ph /\ k e. NN ) -> ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) )
113		imass2	\|- ( ( ( 1 / k ) (,) +oo ) C_ ( ( 1 / ( k + 1 ) ) (,) +oo ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
114	112 113	syl	\|- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) C_ ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
115	66 68 74	syl2anr	\|- ( ( ph /\ k e. NN ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
116		imaexg	\|- ( `' F e. _V -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
117	14 116	syl	\|- ( ph -> ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) e. _V )
118		oveq2	\|- ( n = ( k + 1 ) -> ( 1 / n ) = ( 1 / ( k + 1 ) ) )
119	118	oveq1d	\|- ( n = ( k + 1 ) -> ( ( 1 / n ) (,) +oo ) = ( ( 1 / ( k + 1 ) ) (,) +oo ) )
120	119	imaeq2d	\|- ( n = ( k + 1 ) -> ( `' F " ( ( 1 / n ) (,) +oo ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
121	120 73	fvmptg	\|- ( ( ( 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 ) ) )
122	96 117 121	syl2anr	\|- ( ( ph /\ k e. NN ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) = ( `' F " ( ( 1 / ( k + 1 ) ) (,) +oo ) ) )
123	114 115 122	3sstr4d	\|- ( ( ph /\ k e. NN ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) )
124	123	ralrimiva	\|- ( ph -> A. k e. NN ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) C_ ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` ( k + 1 ) ) )
125		volsup	\|- ( ( ( 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* , < ) )
126	28 124 125	syl2anc	\|- ( ph -> ( vol ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
127	95 126	eqtr3d	\|- ( ph -> ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) = sup ( ( vol " ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) )
128	127	adantr	\|- ( ( 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* , < ) )
129	68	adantr	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. _V )
130	66 129 74	syl2anr	\|- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) = ( `' F " ( ( 1 / k ) (,) +oo ) ) )
131	130	fveq2d	\|- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) = ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) )
132	39	a1i	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 e. RR* )
133		nnrecgt0	\|- ( k e. NN -> 0 < ( 1 / k ) )
134	133	adantl	\|- ( ( ph /\ k e. NN ) -> 0 < ( 1 / k ) )
135		0re	\|- 0 e. RR
136		ltle	\|- ( ( 0 e. RR /\ ( 1 / k ) e. RR ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
137	135 60 136	sylancr	\|- ( ( ph /\ k e. NN ) -> ( 0 < ( 1 / k ) -> 0 <_ ( 1 / k ) ) )
138	134 137	mpd	\|- ( ( ph /\ k e. NN ) -> 0 <_ ( 1 / k ) )
139		elxrge0	\|- ( ( 1 / k ) e. ( 0 [,] +oo ) <-> ( ( 1 / k ) e. RR* /\ 0 <_ ( 1 / k ) ) )
140	61 138 139	sylanbrc	\|- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,] +oo ) )
141		0e0iccpnf	\|- 0 e. ( 0 [,] +oo )
142		ifcl	\|- ( ( ( 1 / k ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
143	140 141 142	sylancl	\|- ( ( ph /\ k e. NN ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
144	143	adantr	\|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. ( 0 [,] +oo ) )
145	144	fmpttd	\|- ( ( ph /\ k e. NN ) -> ( x e. RR \|-> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
146	145	adantrr	\|- ( ( 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 ) )
147		itg2cl	\|- ( ( 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* )
148	146 147	syl	\|- ( ( 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* )
149		icossicc	\|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
150		fss	\|- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
151	3 149 150	sylancl	\|- ( ph -> F : RR --> ( 0 [,] +oo ) )
152		itg2cl	\|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
153	151 152	syl	\|- ( ph -> ( S.2 ` F ) e. RR* )
154	153	adantr	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( S.2 ` F ) e. RR* )
155		0nrp	\|- -. 0 e. RR+
156		simpr	\|- ( ( ( 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 ) ) ) )
157	115 29	eqeltrrd	\|- ( ( ph /\ k e. NN ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
158	157	adantrr	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol )
159	158	adantr	\|- ( ( ( 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 )
160	156 135	eqeltrrdi	\|- ( ( ( 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 )
161	60 134	elrpd	\|- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR+ )
162	161	adantrr	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. RR+ )
163	162	adantr	\|- ( ( ( 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+ )
164		itg2const2	\|- ( ( ( `' 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 ) )
165	159 163 164	syl2anc	\|- ( ( ( 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 ) )
166	160 165	mpbird	\|- ( ( ( 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 )
167		elrege0	\|- ( ( 1 / k ) e. ( 0 [,) +oo ) <-> ( ( 1 / k ) e. RR /\ 0 <_ ( 1 / k ) ) )
168	60 138 167	sylanbrc	\|- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
169	168	adantrr	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> ( 1 / k ) e. ( 0 [,) +oo ) )
170	169	adantr	\|- ( ( ( 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 ) )
171		itg2const	\|- ( ( ( `' 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 ) ) ) ) )
172	159 166 170 171	syl3anc	\|- ( ( ( 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 ) ) ) ) )
173	156 172	eqtrd	\|- ( ( ( 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 ) ) ) ) )
174		simplrr	\|- ( ( ( 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 ) ) ) )
175	166 174	elrpd	\|- ( ( ( 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+ )
176	163 175	rpmulcld	\|- ( ( ( 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+ )
177	173 176	eqeltrd	\|- ( ( ( 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+ )
178	177	ex	\|- ( ( 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+ ) )
179	155 178	mtoi	\|- ( ( 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 ) ) ) )
180		itg2ge0	\|- ( ( 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 ) ) ) )
181	146 180	syl	\|- ( ( 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 ) ) ) )
182		xrleloe	\|- ( ( 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 ) ) ) ) ) )
183	39 148 182	sylancr	\|- ( ( 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 ) ) ) ) ) )
184	181 183	mpbid	\|- ( ( 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 ) ) ) ) )
185	184	ord	\|- ( ( 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 ) ) ) ) )
186	179 185	mt3d	\|- ( ( 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	151	adantr	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> F : RR --> ( 0 [,] +oo ) )
188	60	adantr	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR )
189	53	adantr	\|- ( ( ph /\ k e. NN ) -> F Fn RR )
190	189 55	syl	\|- ( ( ph /\ k e. NN ) -> ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) ) )
191	190	biimpa	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( x e. RR /\ ( F ` x ) e. ( ( 1 / k ) (,) +oo ) ) )
192	191	simpld	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> x e. RR )
193	49	adantlr	\|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
194	192 193	syldan	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. RR )
195	61	adantr	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) e. RR* )
196	191	simprd	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( F ` x ) e. ( ( 1 / k ) (,) +oo ) )
197		simpr	\|- ( ( ( F ` x ) e. RR /\ ( 1 / k ) < ( F ` x ) ) -> ( 1 / k ) < ( F ` x ) )
198	63 197	syl6bi	\|- ( ( 1 / k ) e. RR* -> ( ( F ` x ) e. ( ( 1 / k ) (,) +oo ) -> ( 1 / k ) < ( F ` x ) ) )
199	195 196 198	sylc	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) < ( F ` x ) )
200	188 194 199	ltled	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> ( 1 / k ) <_ ( F ` x ) )
201	48	simprd	\|- ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
202	201	adantlr	\|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
203	192 202	syldan	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
204		breq1	\|- ( ( 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 ) ) )
205		breq1	\|- ( 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 ) ) )
206	204 205	ifboth	\|- ( ( ( 1 / k ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
207	200 203 206	syl2anc	\|- ( ( ( ph /\ k e. NN ) /\ x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
208	207	adantlr	\|- ( ( ( ( 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 ) )
209		iffalse	\|- ( -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
210	209	adantl	\|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) = 0 )
211	202	adantr	\|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 <_ ( F ` x ) )
212	210 211	eqbrtrd	\|- ( ( ( ( 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 ) )
213	208 212	pm2.61dan	\|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
214	213	ralrimiva	\|- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) <_ ( F ` x ) )
215	214	adantrr	\|- ( ( 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 ) )
216		reex	\|- RR e. _V
217	216	a1i	\|- ( ph -> RR e. _V )
218		ovex	\|- ( 1 / k ) e. _V
219		c0ex	\|- 0 e. _V
220	218 219	ifex	\|- if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. _V
221	220	a1i	\|- ( ( ph /\ x e. RR ) -> if ( x e. ( `' F " ( ( 1 / k ) (,) +oo ) ) , ( 1 / k ) , 0 ) e. _V )
222		fvexd	\|- ( ( ph /\ x e. RR ) -> ( F ` x ) e. _V )
223		eqidd	\|- ( 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 ) ) )
224	3	feqmptd	\|- ( ph -> F = ( x e. RR \|-> ( F ` x ) ) )
225	217 221 222 223 224	ofrfval2	\|- ( 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 ) ) )
226	225	biimpar	\|- ( ( 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 )
227	215 226	syldan	\|- ( ( 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 )
228		itg2le	\|- ( ( ( 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 ) )
229	146 187 227 228	syl3anc	\|- ( ( 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 ) )
230	132 148 154 186 229	xrltletrd	\|- ( ( ph /\ ( k e. NN /\ 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) ) -> 0 < ( S.2 ` F ) )
231	230	expr	\|- ( ( ph /\ k e. NN ) -> ( 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) -> 0 < ( S.2 ` F ) ) )
232	231	con3d	\|- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
233	7	ffvelrni	\|- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. ( 0 [,] +oo ) )
234	6 233	sselid	\|- ( ( `' F " ( ( 1 / k ) (,) +oo ) ) e. dom vol -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
235	157 234	syl	\|- ( ( ph /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* )
236		xrlenlt	\|- ( ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
237	235 39 236	sylancl	\|- ( ( ph /\ k e. NN ) -> ( ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 <-> -. 0 < ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) ) )
238	232 237	sylibrd	\|- ( ( ph /\ k e. NN ) -> ( -. 0 < ( S.2 ` F ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 ) )
239	238	imp	\|- ( ( ( ph /\ k e. NN ) /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
240	239	an32s	\|- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( `' F " ( ( 1 / k ) (,) +oo ) ) ) <_ 0 )
241	131 240	eqbrtrd	\|- ( ( ( ph /\ -. 0 < ( S.2 ` F ) ) /\ k e. NN ) -> ( vol ` ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
242	241	ralrimiva	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. k e. NN ( vol ` ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 )
243		ffn	\|- ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) : NN --> _V -> ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) Fn NN )
244		fveq2	\|- ( z = ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( vol ` z ) = ( vol ` ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) )
245	244	breq1d	\|- ( z = ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) -> ( ( vol ` z ) <_ 0 <-> ( vol ` ( ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ` k ) ) <_ 0 ) )
246	245	ralrn	\|- ( ( 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 ) )
247	18 243 246	3syl	\|- ( 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 ) )
248	247	adantr	\|- ( ( 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 ) )
249	242 248	mpbird	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. z e. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ( vol ` z ) <_ 0 )
250		ffn	\|- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
251	7 250	ax-mp	\|- vol Fn dom vol
252	28	frnd	\|- ( ph -> ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
253	252	adantr	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) C_ dom vol )
254		breq1	\|- ( x = ( vol ` z ) -> ( x <_ 0 <-> ( vol ` z ) <_ 0 ) )
255	254	ralima	\|- ( ( 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 ) )
256	251 253 255	sylancr	\|- ( ( 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 ) )
257	249 256	mpbird	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> A. x e. ( vol " ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) x <_ 0 )
258		imassrn	\|- ( vol " ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ ran vol
259		frn	\|- ( vol : dom vol --> ( 0 [,] +oo ) -> ran vol C_ ( 0 [,] +oo ) )
260	7 259	ax-mp	\|- ran vol C_ ( 0 [,] +oo )
261	260 6	sstri	\|- ran vol C_ RR*
262	258 261	sstri	\|- ( vol " ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) C_ RR*
263		supxrleub	\|- ( ( ( 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 ) )
264	262 39 263	mp2an	\|- ( 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 )
265	257 264	sylibr	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> sup ( ( vol " ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) , RR* , < ) <_ 0 )
266	128 265	eqbrtrd	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol* ` U. ran ( n e. NN \|-> ( `' F " ( ( 1 / n ) (,) +oo ) ) ) ) <_ 0 )
267	11 38 40 93 266	xrletrd	\|- ( ( ph /\ -. 0 < ( S.2 ` F ) ) -> ( vol ` A ) <_ 0 )
268	267	ex	\|- ( ph -> ( -. 0 < ( S.2 ` F ) -> ( vol ` A ) <_ 0 ) )
269		xrlenlt	\|- ( ( ( vol ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
270	10 39 269	sylancl	\|- ( ph -> ( ( vol ` A ) <_ 0 <-> -. 0 < ( vol ` A ) ) )
271	268 270	sylibd	\|- ( ph -> ( -. 0 < ( S.2 ` F ) -> -. 0 < ( vol ` A ) ) )
272	2 271	mt4d	\|- ( ph -> 0 < ( S.2 ` F ) )

Metamath Proof Explorer

Theorem itg2gt0

Proof