Theorem itg2monolem1 23517

Description: Lemma for itg2mono 23520. We show that for any constant t less than one, t x. S.1 H is less than S, and so S.1 H <_ S, which is one half of the equality in itg2mono 23520. Consider the sequence A ( n ) = { x | t x. H <_ F ( n ) }. This is an increasing sequence of measurable sets whose union is RR, and so H |` A ( n ) has an integral which equals S.1 H in the limit, by itg1climres 23481. Then by taking the limit in ( t x. H ) |` A ( n ) <_ F ( n ), we get t x. S.1 H <_ S as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
itg2mono.1	|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
itg2mono.2	|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
itg2mono.3	|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
itg2mono.4	|- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
itg2mono.5	|- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
itg2mono.6	|- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
itg2mono.7	|- ( ph -> T e. ( 0 (,) 1 ) )
itg2mono.8	|- ( ph -> H e. dom S.1 )
itg2mono.9	|- ( ph -> H oR <_ G )
itg2mono.10	|- ( ph -> S e. RR )
itg2mono.11	|- A = ( n e. NN |-> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } )

Assertion

Ref	Expression
itg2monolem1	|- ( ph -> ( T x. ( S.1 ` H ) ) <_ S )

Distinct variable groups:   x, A   x, n, y, G   n, H, x, y   n, F, x, y   ph, n, x, y   S, n, x, y   T, n, x, y

Allowed substitution hints:   A( y, n)

Proof of Theorem itg2monolem1

Dummy variables j k m z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11723	. 2 |- NN = ( ZZ>= ` 1 )
2		1zzd 11408	. 2 |- ( ph -> 1 e. ZZ )
3		readdcl 10019	. . . . . . . . . . . . . . . 16 |- ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
4	3	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
5		itg2mono.3	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
6		rge0ssre 12280	. . . . . . . . . . . . . . . 16 |- ( 0 [,) +oo ) C_ RR
7		fss 6056	. . . . . . . . . . . . . . . 16 |- ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` n ) : RR --> RR )
8	5, 6, 7	sylancl 694	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> RR )
9		itg2mono.8	. . . . . . . . . . . . . . . . . 18 |- ( ph -> H e. dom S.1 )
10		itg2mono.7	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> T e. ( 0 (,) 1 ) )
11		0xr 10086	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. RR*
12		1re 10039	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. RR
13	12	rexri 10097	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. RR*
14		elioo2 12216	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 0 e. RR* /\ 1 e. RR* ) -> ( T e. ( 0 (,) 1 ) <-> ( T e. RR /\ 0 < T /\ T < 1 ) ) )
15	11, 13, 14	mp2an 708	. . . . . . . . . . . . . . . . . . . . 21 |- ( T e. ( 0 (,) 1 ) <-> ( T e. RR /\ 0 < T /\ T < 1 ) )
16	10, 15	sylib 208	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( T e. RR /\ 0 < T /\ T < 1 ) )
17	16	simp1d 1073	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> T e. RR )
18	17	renegcld 10457	. . . . . . . . . . . . . . . . . 18 |- ( ph -> -u T e. RR )
19	9, 18	i1fmulc 23470	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 )
20	19	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 )
21		i1ff 23443	. . . . . . . . . . . . . . . 16 |- ( ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 -> ( ( RR X. { -u T } ) oF x. H ) : RR --> RR )
22	20, 21	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) : RR --> RR )
23		reex 10027	. . . . . . . . . . . . . . . 16 |- RR e. _V
24	23	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> RR e. _V )
25		inidm 3822	. . . . . . . . . . . . . . 15 |- ( RR i^i RR ) = RR
26	4, 8, 22, 24, 24, 25	off 6912	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR )
27	26	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR )
28		ffn 6045	. . . . . . . . . . . . 13 |- ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) Fn RR )
29	27, 28	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) Fn RR )
30		elpreima 6337	. . . . . . . . . . . 12 |- ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) Fn RR -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( x e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) ) )
31	29, 30	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( x e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) ) )
32		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> x e. RR )
33	32	biantrurd 529	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( x e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) ) )
34	31, 33	bitr4d 271	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) )
35	26	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR )
36	35	biantrurd 529	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 <-> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) ) )
37		elioomnf 12268	. . . . . . . . . . . 12 |- ( 0 e. RR* -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) ) )
38	11, 37	ax-mp 5	. . . . . . . . . . 11 |- ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) )
39	36, 38	syl6rbbr 279	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) )
40		ffn 6045	. . . . . . . . . . . . . . 15 |- ( ( F ` n ) : RR --> RR -> ( F ` n ) Fn RR )
41	8, 40	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( F ` n ) Fn RR )
42		ffn 6045	. . . . . . . . . . . . . . 15 |- ( ( ( RR X. { -u T } ) oF x. H ) : RR --> RR -> ( ( RR X. { -u T } ) oF x. H ) Fn RR )
43	22, 42	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) Fn RR )
44		eqidd 2623	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` x ) )
45	18	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> -u T e. RR )
46		i1ff 23443	. . . . . . . . . . . . . . . . . . 19 |- ( H e. dom S.1 -> H : RR --> RR )
47	9, 46	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> H : RR --> RR )
48		ffn 6045	. . . . . . . . . . . . . . . . . 18 |- ( H : RR --> RR -> H Fn RR )
49	47, 48	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> H Fn RR )
50	49	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> H Fn RR )
51		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( H ` x ) = ( H ` x ) )
52	24, 45, 50, 51	ofc1 6920	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( RR X. { -u T } ) oF x. H ) ` x ) = ( -u T x. ( H ` x ) ) )
53	17	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. CC )
54	53	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> T e. CC )
55	47	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. RR ) -> ( H ` x ) e. RR )
56	55	adantlr 751	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( H ` x ) e. RR )
57	56	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( H ` x ) e. CC )
58	54, 57	mulneg1d 10483	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( -u T x. ( H ` x ) ) = -u ( T x. ( H ` x ) ) )
59	52, 58	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( RR X. { -u T } ) oF x. H ) ` x ) = -u ( T x. ( H ` x ) ) )
60	41, 43, 24, 24, 25, 44, 59	ofval 6906	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) = ( ( ( F ` n ) ` x ) + -u ( T x. ( H ` x ) ) ) )
61	8	ffvelrnda 6359	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) e. RR )
62	61	recnd 10068	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) e. CC )
63	17	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. RR ) -> T e. RR )
64	63, 55	remulcld 10070	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ( T x. ( H ` x ) ) e. RR )
65	64	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( T x. ( H ` x ) ) e. RR )
66	65	recnd 10068	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( T x. ( H ` x ) ) e. CC )
67	62, 66	negsubd 10398	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) ` x ) + -u ( T x. ( H ` x ) ) ) = ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) )
68	60, 67	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) = ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) )
69	68	breq1d 4663	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 <-> ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) < 0 ) )
70		0red 10041	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> 0 e. RR )
71	61, 65, 70	ltsubaddd 10623	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) < 0 <-> ( ( F ` n ) ` x ) < ( 0 + ( T x. ( H ` x ) ) ) ) )
72	66	addid2d 10237	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( 0 + ( T x. ( H ` x ) ) ) = ( T x. ( H ` x ) ) )
73	72	breq2d 4665	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) ` x ) < ( 0 + ( T x. ( H ` x ) ) ) <-> ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) )
74	69, 71, 73	3bitrd 294	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 <-> ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) )
75	34, 39, 74	3bitrd 294	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) )
76	75	notbid 308	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> -. ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) )
77		eldif 3584	. . . . . . . . . 10 |- ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> ( x e. RR /\ -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) )
78	77	baib 944	. . . . . . . . 9 |- ( x e. RR -> ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) )
79	78	adantl 482	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) )
80	65, 61	lenltd 10183	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> -. ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) )
81	76, 79, 80	3bitr4d 300	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) ) )
82	81	rabbi2dva 3821	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( RR i^i ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } )
83		rembl 23308	. . . . . . 7 |- RR e. dom vol
84		itg2mono.2	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
85		i1fmbf 23442	. . . . . . . . . . 11 |- ( ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 -> ( ( RR X. { -u T } ) oF x. H ) e. MblFn )
86	20, 85	syl 17	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) e. MblFn )
87	84, 86	mbfadd 23428	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) e. MblFn )
88		mbfima 23399	. . . . . . . . 9 |- ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) e. MblFn /\ ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR ) -> ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) e. dom vol )
89	87, 26, 88	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) e. dom vol )
90		cmmbl 23302	. . . . . . . 8 |- ( ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) e. dom vol -> ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) e. dom vol )
91	89, 90	syl 17	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) e. dom vol )
92		inmbl 23310	. . . . . . 7 |- ( ( RR e. dom vol /\ ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) e. dom vol ) -> ( RR i^i ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) e. dom vol )
93	83, 91, 92	sylancr 695	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( RR i^i ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) e. dom vol )
94	82, 93	eqeltrrd 2702	. . . . 5 |- ( ( ph /\ n e. NN ) -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } e. dom vol )
95		itg2mono.11	. . . . 5 |- A = ( n e. NN |-> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } )
96	94, 95	fmptd 6385	. . . 4 |- ( ph -> A : NN --> dom vol )
97		itg2mono.4	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
98	97	ralrimiva 2966	. . . . . . . . . . 11 |- ( ph -> A. n e. NN ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
99		fveq2 6191	. . . . . . . . . . . . 13 |- ( n = j -> ( F ` n ) = ( F ` j ) )
100		oveq1 6657	. . . . . . . . . . . . . 14 |- ( n = j -> ( n + 1 ) = ( j + 1 ) )
101	100	fveq2d 6195	. . . . . . . . . . . . 13 |- ( n = j -> ( F ` ( n + 1 ) ) = ( F ` ( j + 1 ) ) )
102	99, 101	breq12d 4666	. . . . . . . . . . . 12 |- ( n = j -> ( ( F ` n ) oR <_ ( F ` ( n + 1 ) ) <-> ( F ` j ) oR <_ ( F ` ( j + 1 ) ) ) )
103	102	cbvralv 3171	. . . . . . . . . . 11 |- ( A. n e. NN ( F ` n ) oR <_ ( F ` ( n + 1 ) ) <-> A. j e. NN ( F ` j ) oR <_ ( F ` ( j + 1 ) ) )
104	98, 103	sylib 208	. . . . . . . . . 10 |- ( ph -> A. j e. NN ( F ` j ) oR <_ ( F ` ( j + 1 ) ) )
105	104	r19.21bi 2932	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( F ` j ) oR <_ ( F ` ( j + 1 ) ) )
106	5	ralrimiva 2966	. . . . . . . . . . . . 13 |- ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) )
107	99	feq1d 6030	. . . . . . . . . . . . . 14 |- ( n = j -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` j ) : RR --> ( 0 [,) +oo ) ) )
108	107	cbvralv 3171	. . . . . . . . . . . . 13 |- ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) <-> A. j e. NN ( F ` j ) : RR --> ( 0 [,) +oo ) )
109	106, 108	sylib 208	. . . . . . . . . . . 12 |- ( ph -> A. j e. NN ( F ` j ) : RR --> ( 0 [,) +oo ) )
110	109	r19.21bi 2932	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> ( F ` j ) : RR --> ( 0 [,) +oo ) )
111		ffn 6045	. . . . . . . . . . 11 |- ( ( F ` j ) : RR --> ( 0 [,) +oo ) -> ( F ` j ) Fn RR )
112	110, 111	syl 17	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( F ` j ) Fn RR )
113		peano2nn 11032	. . . . . . . . . . . 12 |- ( j e. NN -> ( j + 1 ) e. NN )
114		fveq2 6191	. . . . . . . . . . . . . 14 |- ( n = ( j + 1 ) -> ( F ` n ) = ( F ` ( j + 1 ) ) )
115	114	feq1d 6030	. . . . . . . . . . . . 13 |- ( n = ( j + 1 ) -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) ) )
116	115	rspccva 3308	. . . . . . . . . . . 12 |- ( ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( j + 1 ) e. NN ) -> ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) )
117	106, 113, 116	syl2an 494	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) )
118		ffn 6045	. . . . . . . . . . 11 |- ( ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) -> ( F ` ( j + 1 ) ) Fn RR )
119	117, 118	syl 17	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> ( F ` ( j + 1 ) ) Fn RR )
120	23	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> RR e. _V )
121		eqidd 2623	. . . . . . . . . 10 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` j ) ` x ) = ( ( F ` j ) ` x ) )
122		eqidd 2623	. . . . . . . . . 10 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` ( j + 1 ) ) ` x ) = ( ( F ` ( j + 1 ) ) ` x ) )
123	112, 119, 120, 120, 25, 121, 122	ofrfval 6905	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( ( F ` j ) oR <_ ( F ` ( j + 1 ) ) <-> A. x e. RR ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) )
124	105, 123	mpbid 222	. . . . . . . 8 |- ( ( ph /\ j e. NN ) -> A. x e. RR ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) )
125	124	r19.21bi 2932	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) )
126	17	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> T e. RR )
127	47	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ j e. NN ) -> H : RR --> RR )
128	127	ffvelrnda 6359	. . . . . . . . 9 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( H ` x ) e. RR )
129	126, 128	remulcld 10070	. . . . . . . 8 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( T x. ( H ` x ) ) e. RR )
130		fss 6056	. . . . . . . . . 10 |- ( ( ( F ` j ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` j ) : RR --> RR )
131	110, 6, 130	sylancl 694	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( F ` j ) : RR --> RR )
132	131	ffvelrnda 6359	. . . . . . . 8 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` j ) ` x ) e. RR )
133		fss 6056	. . . . . . . . . 10 |- ( ( ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` ( j + 1 ) ) : RR --> RR )
134	117, 6, 133	sylancl 694	. . . . . . . . 9 |- ( ( ph /\ j e. NN ) -> ( F ` ( j + 1 ) ) : RR --> RR )
135	134	ffvelrnda 6359	. . . . . . . 8 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` ( j + 1 ) ) ` x ) e. RR )
136		letr 10131	. . . . . . . 8 |- ( ( ( T x. ( H ` x ) ) e. RR /\ ( ( F ` j ) ` x ) e. RR /\ ( ( F ` ( j + 1 ) ) ` x ) e. RR ) -> ( ( ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) /\ ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) -> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) )
137	129, 132, 135, 136	syl3anc 1326	. . . . . . 7 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) /\ ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) -> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) )
138	125, 137	mpan2d 710	. . . . . 6 |- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) -> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) )
139	138	ss2rabdv 3683	. . . . 5 |- ( ( ph /\ j e. NN ) -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } C_ { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } )
140	99	fveq1d 6193	. . . . . . . . 9 |- ( n = j -> ( ( F ` n ) ` x ) = ( ( F ` j ) ` x ) )
141	140	breq2d 4665	. . . . . . . 8 |- ( n = j -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) )
142	141	rabbidv 3189	. . . . . . 7 |- ( n = j -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } )
143	23	rabex 4813	. . . . . . 7 |- { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } e. _V
144	142, 95, 143	fvmpt 6282	. . . . . 6 |- ( j e. NN -> ( A ` j ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } )
145	144	adantl 482	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( A ` j ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } )
146	113	adantl 482	. . . . . 6 |- ( ( ph /\ j e. NN ) -> ( j + 1 ) e. NN )
147	114	fveq1d 6193	. . . . . . . . 9 |- ( n = ( j + 1 ) -> ( ( F ` n ) ` x ) = ( ( F ` ( j + 1 ) ) ` x ) )
148	147	breq2d 4665	. . . . . . . 8 |- ( n = ( j + 1 ) -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) )
149	148	rabbidv 3189	. . . . . . 7 |- ( n = ( j + 1 ) -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } )
150	23	rabex 4813	. . . . . . 7 |- { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } e. _V
151	149, 95, 150	fvmpt 6282	. . . . . 6 |- ( ( j + 1 ) e. NN -> ( A ` ( j + 1 ) ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } )
152	146, 151	syl 17	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( A ` ( j + 1 ) ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } )
153	139, 145, 152	3sstr4d 3648	. . . 4 |- ( ( ph /\ j e. NN ) -> ( A ` j ) C_ ( A ` ( j + 1 ) ) )
154	64	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) e. RR )
155	55	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( H ` x ) e. RR )
156	61	an32s 846	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR ) /\ n e. NN ) -> ( ( F ` n ) ` x ) e. RR )
157		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN |-> ( ( F ` n ) ` x ) ) = ( n e. NN |-> ( ( F ` n ) ` x ) )
158	156, 157	fmptd 6385	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) : NN --> RR )
159		frn 6053	. . . . . . . . . . . . . . . . 17 |- ( ( n e. NN |-> ( ( F ` n ) ` x ) ) : NN --> RR -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR )
160	158, 159	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR )
161		1nn 11031	. . . . . . . . . . . . . . . . . . 19 |- 1 e. NN
162	157, 156	dmmptd 6024	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) = NN )
163	161, 162	syl5eleqr 2708	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. RR ) -> 1 e. dom ( n e. NN |-> ( ( F ` n ) ` x ) ) )
164		ne0i 3921	. . . . . . . . . . . . . . . . . 18 |- ( 1 e. dom ( n e. NN |-> ( ( F ` n ) ` x ) ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
165	163, 164	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
166		dm0rn0 5342	. . . . . . . . . . . . . . . . . 18 |- ( dom ( n e. NN |-> ( ( F ` n ) ` x ) ) = (/) <-> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) = (/) )
167	166	necon3bii 2846	. . . . . . . . . . . . . . . . 17 |- ( dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) <-> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
168	165, 167	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
169		itg2mono.5	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
170		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. NN |-> ( ( F ` n ) ` x ) ) : NN --> RR -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN )
171	158, 170	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN )
172		breq1 4656	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) -> ( z <_ y <-> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) )
173	172	ralrn 6362	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) )
174	171, 173	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. RR ) -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) )
175		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = m -> ( F ` n ) = ( F ` m ) )
176	175	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = m -> ( ( F ` n ) ` x ) = ( ( F ` m ) ` x ) )
177		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` m ) ` x ) e. _V
178	176, 157, 177	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. NN -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
179	178	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> ( ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> ( ( F ` m ) ` x ) <_ y ) )
180	179	ralbiia 2979	. . . . . . . . . . . . . . . . . . . 20 |- ( A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> A. m e. NN ( ( F ` m ) ` x ) <_ y )
181	176	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = m -> ( ( ( F ` n ) ` x ) <_ y <-> ( ( F ` m ) ` x ) <_ y ) )
182	181	cbvralv 3171	. . . . . . . . . . . . . . . . . . . 20 |- ( A. n e. NN ( ( F ` n ) ` x ) <_ y <-> A. m e. NN ( ( F ` m ) ` x ) <_ y )
183	180, 182	bitr4i 267	. . . . . . . . . . . . . . . . . . 19 |- ( A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> A. n e. NN ( ( F ` n ) ` x ) <_ y )
184	174, 183	syl6bb 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. RR ) -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. n e. NN ( ( F ` n ) ` x ) <_ y ) )
185	184	rexbidv 3052	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. RR ) -> ( E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y ) )
186	169, 185	mpbird 247	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y )
187		suprcl 10983	. . . . . . . . . . . . . . . 16 |- ( ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR /\ ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
188	160, 168, 186, 187	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
189	188	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
190	16	simp3d 1075	. . . . . . . . . . . . . . . . 17 |- ( ph -> T < 1 )
191	190	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> T < 1 )
192	17	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> T e. RR )
193		1red 10055	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> 1 e. RR )
194		simprr 796	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> 0 < ( H ` x ) )
195		ltmul1 10873	. . . . . . . . . . . . . . . . 17 |- ( ( T e. RR /\ 1 e. RR /\ ( ( H ` x ) e. RR /\ 0 < ( H ` x ) ) ) -> ( T < 1 <-> ( T x. ( H ` x ) ) < ( 1 x. ( H ` x ) ) ) )
196	192, 193, 155, 194, 195	syl112anc 1330	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T < 1 <-> ( T x. ( H ` x ) ) < ( 1 x. ( H ` x ) ) ) )
197	191, 196	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) < ( 1 x. ( H ` x ) ) )
198	155	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( H ` x ) e. CC )
199	198	mulid2d 10058	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( 1 x. ( H ` x ) ) = ( H ` x ) )
200	197, 199	breqtrd 4679	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) < ( H ` x ) )
201		itg2mono.9	. . . . . . . . . . . . . . . . . 18 |- ( ph -> H oR <_ G )
202		itg2mono.1	. . . . . . . . . . . . . . . . . . . . 21 |- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
203	188, 202	fmptd 6385	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> G : RR --> RR )
204		ffn 6045	. . . . . . . . . . . . . . . . . . . 20 |- ( G : RR --> RR -> G Fn RR )
205	203, 204	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> G Fn RR )
206	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> RR e. _V )
207		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. RR ) -> ( H ` y ) = ( H ` y ) )
208		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = y -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` y ) )
209	208	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( n e. NN |-> ( ( F ` n ) ` x ) ) = ( n e. NN |-> ( ( F ` n ) ` y ) ) )
210	209	rneqd 5353	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) = ran ( n e. NN |-> ( ( F ` n ) ` y ) ) )
211	210	supeq1d 8352	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) )
212		ltso 10118	. . . . . . . . . . . . . . . . . . . . . 22 |- < Or RR
213	212	supex 8369	. . . . . . . . . . . . . . . . . . . . 21 |- sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) e. _V
214	211, 202, 213	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. RR -> ( G ` y ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) )
215	214	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. RR ) -> ( G ` y ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) )
216	49, 205, 206, 206, 25, 207, 215	ofrfval 6905	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( H oR <_ G <-> A. y e. RR ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) )
217	201, 216	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. y e. RR ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) )
218		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( H ` x ) = ( H ` y ) )
219	218, 211	breq12d 4666	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) )
220	219	cbvralv 3171	. . . . . . . . . . . . . . . . 17 |- ( A. x e. RR ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> A. y e. RR ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) )
221	217, 220	sylibr 224	. . . . . . . . . . . . . . . 16 |- ( ph -> A. x e. RR ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
222	221	r19.21bi 2932	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
223	222	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
224	154, 155, 189, 200, 223	ltletrd 10197	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) < sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
225	160	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR )
226	168	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
227	186	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y )
228		suprlub 10987	. . . . . . . . . . . . . 14 |- ( ( ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR /\ ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) /\ ( T x. ( H ` x ) ) e. RR ) -> ( ( T x. ( H ` x ) ) < sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w ) )
229	225, 226, 227, 154, 228	syl31anc 1329	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( ( T x. ( H ` x ) ) < sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w ) )
230	224, 229	mpbid 222	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w )
231	171	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN )
232		breq2 4657	. . . . . . . . . . . . . . 15 |- ( w = ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) -> ( ( T x. ( H ` x ) ) < w <-> ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) ) )
233	232	rexrn 6361	. . . . . . . . . . . . . 14 |- ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN -> ( E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) ) )
234	231, 233	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) ) )
235		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( ( F ` j ) ` x ) e. _V
236	140, 157, 235	fvmpt 6282	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) = ( ( F ` j ) ` x ) )
237	236	breq2d 4665	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) <-> ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) ) )
238	237	rexbiia 3040	. . . . . . . . . . . . 13 |- ( E. j e. NN ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) )
239	234, 238	syl6bb 276	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) ) )
240	230, 239	mpbid 222	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) )
241	192, 155	remulcld 10070	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) e. RR )
242	241	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) e. RR )
243	110	adantlr 751	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( F ` j ) : RR --> ( 0 [,) +oo ) )
244		simplr 792	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> x e. RR )
245	243, 244	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. ( 0 [,) +oo ) )
246		elrege0 12278	. . . . . . . . . . . . . . . 16 |- ( ( ( F ` j ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( F ` j ) ` x ) e. RR /\ 0 <_ ( ( F ` j ) ` x ) ) )
247	245, 246	sylib 208	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( ( F ` j ) ` x ) e. RR /\ 0 <_ ( ( F ` j ) ` x ) ) )
248	247	simpld 475	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. RR )
249	248	adantlrr 757	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. RR )
250		ltle 10126	. . . . . . . . . . . . 13 |- ( ( ( T x. ( H ` x ) ) e. RR /\ ( ( F ` j ) ` x ) e. RR ) -> ( ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) -> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) )
251	242, 249, 250	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) /\ j e. NN ) -> ( ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) -> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) )
252	251	reximdva 3017	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) )
253	240, 252	mpd 15	. . . . . . . . . 10 |- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
254	253	anassrs 680	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ 0 < ( H ` x ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
255	161	ne0ii 3923	. . . . . . . . . . 11 |- NN =/= (/)
256	64	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> ( T x. ( H ` x ) ) e. RR )
257	256	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) e. RR )
258		0red 10041	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> 0 e. RR )
259	247	adantlrr 757	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( ( ( F ` j ) ` x ) e. RR /\ 0 <_ ( ( F ` j ) ` x ) ) )
260	259	simpld 475	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. RR )
261		simplrr 801	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( H ` x ) <_ 0 )
262	55	adantrr 753	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> ( H ` x ) e. RR )
263	262	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( H ` x ) e. RR )
264	17	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> T e. RR )
265	16	simp2d 1074	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 < T )
266	265	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> 0 < T )
267		lemul2 10876	. . . . . . . . . . . . . . . 16 |- ( ( ( H ` x ) e. RR /\ 0 e. RR /\ ( T e. RR /\ 0 < T ) ) -> ( ( H ` x ) <_ 0 <-> ( T x. ( H ` x ) ) <_ ( T x. 0 ) ) )
268	263, 258, 264, 266, 267	syl112anc 1330	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( ( H ` x ) <_ 0 <-> ( T x. ( H ` x ) ) <_ ( T x. 0 ) ) )
269	261, 268	mpbid 222	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) <_ ( T x. 0 ) )
270	264	recnd 10068	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> T e. CC )
271	270	mul01d 10235	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. 0 ) = 0 )
272	269, 271	breqtrd 4679	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) <_ 0 )
273	259	simprd 479	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> 0 <_ ( ( F ` j ) ` x ) )
274	257, 258, 260, 272, 273	letrd 10194	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
275	274	ralrimiva 2966	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> A. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
276		r19.2z 4060	. . . . . . . . . . 11 |- ( ( NN =/= (/) /\ A. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
277	255, 275, 276	sylancr 695	. . . . . . . . . 10 |- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
278	277	anassrs 680	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ ( H ` x ) <_ 0 ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
279		0red 10041	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> 0 e. RR )
280	254, 278, 279, 55	ltlecasei 10145	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
281	280	ralrimiva 2966	. . . . . . 7 |- ( ph -> A. x e. RR E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
282		rabid2 3118	. . . . . . 7 |- ( RR = { x e. RR | E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } <-> A. x e. RR E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) )
283	281, 282	sylibr 224	. . . . . 6 |- ( ph -> RR = { x e. RR | E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } )
284		iunrab 4567	. . . . . 6 |- U_ j e. NN { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } = { x e. RR | E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) }
285	283, 284	syl6eqr 2674	. . . . 5 |- ( ph -> RR = U_ j e. NN { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } )
286	145	iuneq2dv 4542	. . . . 5 |- ( ph -> U_ j e. NN ( A ` j ) = U_ j e. NN { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } )
287		ffn 6045	. . . . . . 7 |- ( A : NN --> dom vol -> A Fn NN )
288	96, 287	syl 17	. . . . . 6 |- ( ph -> A Fn NN )
289		fniunfv 6505	. . . . . 6 |- ( A Fn NN -> U_ j e. NN ( A ` j ) = U. ran A )
290	288, 289	syl 17	. . . . 5 |- ( ph -> U_ j e. NN ( A ` j ) = U. ran A )
291	285, 286, 290	3eqtr2rd 2663	. . . 4 |- ( ph -> U. ran A = RR )
292		eqid 2622	. . . 4 |- ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) )
293	96, 153, 291, 9, 292	itg1climres 23481	. . 3 |- ( ph -> ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ~~> ( S.1 ` H ) )
294		nnex 11026	. . . . 5 |- NN e. _V
295	294	mptex 6486	. . . 4 |- ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) e. _V
296	295	a1i 11	. . 3 |- ( ph -> ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) e. _V )
297		fveq2 6191	. . . . . . . . . . 11 |- ( j = k -> ( A ` j ) = ( A ` k ) )
298	297	eleq2d 2687	. . . . . . . . . 10 |- ( j = k -> ( x e. ( A ` j ) <-> x e. ( A ` k ) ) )
299	298	ifbid 4108	. . . . . . . . 9 |- ( j = k -> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) = if ( x e. ( A ` k ) , ( H ` x ) , 0 ) )
300	299	mpteq2dv 4745	. . . . . . . 8 |- ( j = k -> ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) )
301	300	fveq2d 6195	. . . . . . 7 |- ( j = k -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) )
302		eqid 2622	. . . . . . 7 |- ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) = ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) )
303		fvex 6201	. . . . . . 7 |- ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. _V
304	301, 302, 303	fvmpt 6282	. . . . . 6 |- ( k e. NN -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) )
305	304	adantl 482	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) )
306	9	adantr 481	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> H e. dom S.1 )
307	96	ffvelrnda 6359	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( A ` k ) e. dom vol )
308		eqid 2622	. . . . . . . 8 |- ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) )
309	308	i1fres 23472	. . . . . . 7 |- ( ( H e. dom S.1 /\ ( A ` k ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) e. dom S.1 )
310	306, 307, 309	syl2anc 693	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) e. dom S.1 )
311		itg1cl 23452	. . . . . 6 |- ( ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. RR )
312	310, 311	syl 17	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. RR )
313	305, 312	eqeltrd 2701	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) e. RR )
314	313	recnd 10068	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) e. CC )
315	301	oveq2d 6666	. . . . . 6 |- ( j = k -> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) )
316		eqid 2622	. . . . . 6 |- ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) = ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) )
317		ovex 6678	. . . . . 6 |- ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) e. _V
318	315, 316, 317	fvmpt 6282	. . . . 5 |- ( k e. NN -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) )
319	304	oveq2d 6666	. . . . 5 |- ( k e. NN -> ( T x. ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) )
320	318, 319	eqtr4d 2659	. . . 4 |- ( k e. NN -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) ) )
321	320	adantl 482	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) ) )
322	1, 2, 293, 53, 296, 314, 321	climmulc2 14367	. 2 |- ( ph -> ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ~~> ( T x. ( S.1 ` H ) ) )
323		icossicc 12260	. . . . . . 7 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
324		fss 6056	. . . . . . 7 |- ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
325	5, 323, 324	sylancl 694	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
326		itg2mono.10	. . . . . . 7 |- ( ph -> S e. RR )
327	326	adantr 481	. . . . . 6 |- ( ( ph /\ n e. NN ) -> S e. RR )
328		itg2cl 23499	. . . . . . . . . . . 12 |- ( ( F ` n ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` n ) ) e. RR* )
329	325, 328	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR* )
330		eqid 2622	. . . . . . . . . . 11 |- ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = ( n e. NN |-> ( S.2 ` ( F ` n ) ) )
331	329, 330	fmptd 6385	. . . . . . . . . 10 |- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR* )
332		frn 6053	. . . . . . . . . 10 |- ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR* -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* )
333	331, 332	syl 17	. . . . . . . . 9 |- ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* )
334	333	adantr 481	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* )
335		fvex 6201	. . . . . . . . . . 11 |- ( S.2 ` ( F ` n ) ) e. _V
336	335	elabrex 6501	. . . . . . . . . 10 |- ( n e. NN -> ( S.2 ` ( F ` n ) ) e. { x | E. n e. NN x = ( S.2 ` ( F ` n ) ) } )
337	336	adantl 482	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. { x | E. n e. NN x = ( S.2 ` ( F ` n ) ) } )
338	330	rnmpt 5371	. . . . . . . . 9 |- ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = { x | E. n e. NN x = ( S.2 ` ( F ` n ) ) }
339	337, 338	syl6eleqr 2712	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
340		supxrub 12154	. . . . . . . 8 |- ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* /\ ( S.2 ` ( F ` n ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ) -> ( S.2 ` ( F ` n ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) )
341	334, 339, 340	syl2anc 693	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) )
342		itg2mono.6	. . . . . . 7 |- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
343	341, 342	syl6breqr 4695	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) <_ S )
344		itg2lecl 23505	. . . . . 6 |- ( ( ( F ` n ) : RR --> ( 0 [,] +oo ) /\ S e. RR /\ ( S.2 ` ( F ` n ) ) <_ S ) -> ( S.2 ` ( F ` n ) ) e. RR )
345	325, 327, 343, 344	syl3anc 1326	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR )
346	345, 330	fmptd 6385	. . . 4 |- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR )
347	325	ralrimiva 2966	. . . . . . . . . 10 |- ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,] +oo ) )
348		fveq2 6191	. . . . . . . . . . . 12 |- ( n = k -> ( F ` n ) = ( F ` k ) )
349	348	feq1d 6030	. . . . . . . . . . 11 |- ( n = k -> ( ( F ` n ) : RR --> ( 0 [,] +oo ) <-> ( F ` k ) : RR --> ( 0 [,] +oo ) ) )
350	349	cbvralv 3171	. . . . . . . . . 10 |- ( A. n e. NN ( F ` n ) : RR --> ( 0 [,] +oo ) <-> A. k e. NN ( F ` k ) : RR --> ( 0 [,] +oo ) )
351	347, 350	sylib 208	. . . . . . . . 9 |- ( ph -> A. k e. NN ( F ` k ) : RR --> ( 0 [,] +oo ) )
352		peano2nn 11032	. . . . . . . . 9 |- ( n e. NN -> ( n + 1 ) e. NN )
353		fveq2 6191	. . . . . . . . . . 11 |- ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
354	353	feq1d 6030	. . . . . . . . . 10 |- ( k = ( n + 1 ) -> ( ( F ` k ) : RR --> ( 0 [,] +oo ) <-> ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) ) )
355	354	rspccva 3308	. . . . . . . . 9 |- ( ( A. k e. NN ( F ` k ) : RR --> ( 0 [,] +oo ) /\ ( n + 1 ) e. NN ) -> ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) )
356	351, 352, 355	syl2an 494	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) )
357		itg2le 23506	. . . . . . . 8 |- ( ( ( F ` n ) : RR --> ( 0 [,] +oo ) /\ ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) /\ ( F ` n ) oR <_ ( F ` ( n + 1 ) ) ) -> ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) )
358	325, 356, 97, 357	syl3anc 1326	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) )
359	358	ralrimiva 2966	. . . . . 6 |- ( ph -> A. n e. NN ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) )
360	348	fveq2d 6195	. . . . . . . . . 10 |- ( n = k -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` k ) ) )
361		fvex 6201	. . . . . . . . . 10 |- ( S.2 ` ( F ` k ) ) e. _V
362	360, 330, 361	fvmpt 6282	. . . . . . . . 9 |- ( k e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) = ( S.2 ` ( F ` k ) ) )
363		peano2nn 11032	. . . . . . . . . 10 |- ( k e. NN -> ( k + 1 ) e. NN )
364		fveq2 6191	. . . . . . . . . . . 12 |- ( n = ( k + 1 ) -> ( F ` n ) = ( F ` ( k + 1 ) ) )
365	364	fveq2d 6195	. . . . . . . . . . 11 |- ( n = ( k + 1 ) -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) )
366		fvex 6201	. . . . . . . . . . 11 |- ( S.2 ` ( F ` ( k + 1 ) ) ) e. _V
367	365, 330, 366	fvmpt 6282	. . . . . . . . . 10 |- ( ( k + 1 ) e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) )
368	363, 367	syl 17	. . . . . . . . 9 |- ( k e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) )
369	362, 368	breq12d 4666	. . . . . . . 8 |- ( k e. NN -> ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) <-> ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) ) )
370	369	ralbiia 2979	. . . . . . 7 |- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) )
371		oveq1 6657	. . . . . . . . . . 11 |- ( n = k -> ( n + 1 ) = ( k + 1 ) )
372	371	fveq2d 6195	. . . . . . . . . 10 |- ( n = k -> ( F ` ( n + 1 ) ) = ( F ` ( k + 1 ) ) )
373	372	fveq2d 6195	. . . . . . . . 9 |- ( n = k -> ( S.2 ` ( F ` ( n + 1 ) ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) )
374	360, 373	breq12d 4666	. . . . . . . 8 |- ( n = k -> ( ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) <-> ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) ) )
375	374	cbvralv 3171	. . . . . . 7 |- ( A. n e. NN ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) )
376	370, 375	bitr4i 267	. . . . . 6 |- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) )
377	359, 376	sylibr 224	. . . . 5 |- ( ph -> A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) )
378	377	r19.21bi 2932	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) )
379	343	ralrimiva 2966	. . . . 5 |- ( ph -> A. n e. NN ( S.2 ` ( F ` n ) ) <_ S )
380	362	breq1d 4663	. . . . . . . . 9 |- ( k e. NN -> ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> ( S.2 ` ( F ` k ) ) <_ x ) )
381	380	ralbiia 2979	. . . . . . . 8 |- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ x )
382	360	breq1d 4663	. . . . . . . . 9 |- ( n = k -> ( ( S.2 ` ( F ` n ) ) <_ x <-> ( S.2 ` ( F ` k ) ) <_ x ) )
383	382	cbvralv 3171	. . . . . . . 8 |- ( A. n e. NN ( S.2 ` ( F ` n ) ) <_ x <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ x )
384	381, 383	bitr4i 267	. . . . . . 7 |- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ x )
385		breq2 4657	. . . . . . . 8 |- ( x = S -> ( ( S.2 ` ( F ` n ) ) <_ x <-> ( S.2 ` ( F ` n ) ) <_ S ) )
386	385	ralbidv 2986	. . . . . . 7 |- ( x = S -> ( A. n e. NN ( S.2 ` ( F ` n ) ) <_ x <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) )
387	384, 386	syl5bb 272	. . . . . 6 |- ( x = S -> ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) )
388	387	rspcev 3309	. . . . 5 |- ( ( S e. RR /\ A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) -> E. x e. RR A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x )
389	326, 379, 388	syl2anc 693	. . . 4 |- ( ph -> E. x e. RR A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x )
390	1, 2, 346, 378, 389	climsup 14400	. . 3 |- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ~~> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) )
391		frn 6053	. . . . . 6 |- ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR )
392	346, 391	syl 17	. . . . 5 |- ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR )
393	330, 329	dmmptd 6024	. . . . . . 7 |- ( ph -> dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = NN )
394	255	a1i 11	. . . . . . 7 |- ( ph -> NN =/= (/) )
395	393, 394	eqnetrd 2861	. . . . . 6 |- ( ph -> dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) )
396		dm0rn0 5342	. . . . . . 7 |- ( dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = (/) <-> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = (/) )
397	396	necon3bii 2846	. . . . . 6 |- ( dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) <-> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) )
398	395, 397	sylib 208	. . . . 5 |- ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) )
399	335, 330	fnmpti 6022	. . . . . . . . 9 |- ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN
400	399	a1i 11	. . . . . . . 8 |- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN )
401		breq1 4656	. . . . . . . . 9 |- ( z = ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) -> ( z <_ x <-> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) )
402	401	ralrn 6362	. . . . . . . 8 |- ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x <-> A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) )
403	400, 402	syl 17	. . . . . . 7 |- ( ph -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x <-> A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) )
404	403	rexbidv 3052	. . . . . 6 |- ( ph -> ( E. x e. RR A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x <-> E. x e. RR A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) )
405	389, 404	mpbird 247	. . . . 5 |- ( ph -> E. x e. RR A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x )
406		supxrre 12157	. . . . 5 |- ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR /\ ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) /\ E. x e. RR A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x ) -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) )
407	392, 398, 405, 406	syl3anc 1326	. . . 4 |- ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) )
408	342, 407	syl5req 2669	. . 3 |- ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) = S )
409	390, 408	breqtrd 4679	. 2 |- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ~~> S )
410	17	adantr 481	. . . . 5 |- ( ( ph /\ j e. NN ) -> T e. RR )
411	9	adantr 481	. . . . . . 7 |- ( ( ph /\ j e. NN ) -> H e. dom S.1 )
412	96	ffvelrnda 6359	. . . . . . 7 |- ( ( ph /\ j e. NN ) -> ( A ` j ) e. dom vol )
413	292	i1fres 23472	. . . . . . 7 |- ( ( H e. dom S.1 /\ ( A ` j ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) e. dom S.1 )
414	411, 412, 413	syl2anc 693	. . . . . 6 |- ( ( ph /\ j e. NN ) -> ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) e. dom S.1 )
415		itg1cl 23452	. . . . . 6 |- ( ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) e. RR )
416	414, 415	syl 17	. . . . 5 |- ( ( ph /\ j e. NN ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) e. RR )
417	410, 416	remulcld 10070	. . . 4 |- ( ( ph /\ j e. NN ) -> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) e. RR )
418	417, 316	fmptd 6385	. . 3 |- ( ph -> ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) : NN --> RR )
419	418	ffvelrnda 6359	. 2 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) e. RR )
420	346	ffvelrnda 6359	. 2 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) e. RR )
421	348	feq1d 6030	. . . . . . . 8 |- ( n = k -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` k ) : RR --> ( 0 [,) +oo ) ) )
422	421	cbvralv 3171	. . . . . . 7 |- ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) <-> A. k e. NN ( F ` k ) : RR --> ( 0 [,) +oo ) )
423	106, 422	sylib 208	. . . . . 6 |- ( ph -> A. k e. NN ( F ` k ) : RR --> ( 0 [,) +oo ) )
424	423	r19.21bi 2932	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( F ` k ) : RR --> ( 0 [,) +oo ) )
425		fss 6056	. . . . 5 |- ( ( ( F ` k ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` k ) : RR --> ( 0 [,] +oo ) )
426	424, 323, 425	sylancl 694	. . . 4 |- ( ( ph /\ k e. NN ) -> ( F ` k ) : RR --> ( 0 [,] +oo ) )
427	23	a1i 11	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> RR e. _V )
428	17	adantr 481	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> T e. RR )
429	428	adantr 481	. . . . . . 7 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> T e. RR )
430		fvex 6201	. . . . . . . . 9 |- ( H ` x ) e. _V
431		c0ex 10034	. . . . . . . . 9 |- 0 e. _V
432	430, 431	ifex 4156	. . . . . . . 8 |- if ( x e. ( A ` k ) , ( H ` x ) , 0 ) e. _V
433	432	a1i 11	. . . . . . 7 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) e. _V )
434		fconstmpt 5163	. . . . . . . 8 |- ( RR X. { T } ) = ( x e. RR |-> T )
435	434	a1i 11	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( RR X. { T } ) = ( x e. RR |-> T ) )
436		eqidd 2623	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) )
437	427, 429, 433, 435, 436	offval2 6914	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) = ( x e. RR |-> ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) )
438		ovif2 6738	. . . . . . . 8 |- ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , ( T x. 0 ) )
439	53	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> T e. CC )
440	439	mul01d 10235	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> ( T x. 0 ) = 0 )
441	440	ifeq2d 4105	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , ( T x. 0 ) ) = if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) )
442	438, 441	syl5eq 2668	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) )
443	442	mpteq2dv 4745	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) )
444	437, 443	eqtrd 2656	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) )
445	310, 428	i1fmulc 23470	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. dom S.1 )
446	444, 445	eqeltrrd 2702	. . . 4 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) e. dom S.1 )
447		iftrue 4092	. . . . . . . . 9 |- ( x e. ( A ` k ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = ( T x. ( H ` x ) ) )
448	447	adantl 482	. . . . . . . 8 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = ( T x. ( H ` x ) ) )
449	348	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( n = k -> ( ( F ` n ) ` x ) = ( ( F ` k ) ` x ) )
450	449	breq2d 4665	. . . . . . . . . . . . . 14 |- ( n = k -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) ) )
451	450	rabbidv 3189	. . . . . . . . . . . . 13 |- ( n = k -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } )
452	23	rabex 4813	. . . . . . . . . . . . 13 |- { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } e. _V
453	451, 95, 452	fvmpt 6282	. . . . . . . . . . . 12 |- ( k e. NN -> ( A ` k ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } )
454	453	ad2antlr 763	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( A ` k ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } )
455	454	eleq2d 2687	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( x e. ( A ` k ) <-> x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } ) )
456	455	biimpa 501	. . . . . . . . 9 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } )
457		rabid 3116	. . . . . . . . . 10 |- ( x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } <-> ( x e. RR /\ ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) ) )
458	457	simprbi 480	. . . . . . . . 9 |- ( x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } -> ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) )
459	456, 458	syl 17	. . . . . . . 8 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) )
460	448, 459	eqbrtrd 4675	. . . . . . 7 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) )
461		iffalse 4095	. . . . . . . . 9 |- ( -. x e. ( A ` k ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = 0 )
462	461	adantl 482	. . . . . . . 8 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = 0 )
463	424	ffvelrnda 6359	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( ( F ` k ) ` x ) e. ( 0 [,) +oo ) )
464		elrege0 12278	. . . . . . . . . . 11 |- ( ( ( F ` k ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( F ` k ) ` x ) e. RR /\ 0 <_ ( ( F ` k ) ` x ) ) )
465	464	simprbi 480	. . . . . . . . . 10 |- ( ( ( F ` k ) ` x ) e. ( 0 [,) +oo ) -> 0 <_ ( ( F ` k ) ` x ) )
466	463, 465	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( ( F ` k ) ` x ) )
467	466	adantr 481	. . . . . . . 8 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( A ` k ) ) -> 0 <_ ( ( F ` k ) ` x ) )
468	462, 467	eqbrtrd 4675	. . . . . . 7 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) )
469	460, 468	pm2.61dan 832	. . . . . 6 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) )
470	469	ralrimiva 2966	. . . . 5 |- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) )
471		ovex 6678	. . . . . . . 8 |- ( T x. ( H ` x ) ) e. _V
472	471, 431	ifex 4156	. . . . . . 7 |- if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) e. _V
473	472	a1i 11	. . . . . 6 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) e. _V )
474		fvexd 6203	. . . . . 6 |- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( ( F ` k ) ` x ) e. _V )
475		eqidd 2623	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) )
476	424	feqmptd 6249	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( x e. RR |-> ( ( F ` k ) ` x ) ) )
477	427, 473, 474, 475, 476	ofrfval2 6915	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) oR <_ ( F ` k ) <-> A. x e. RR if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) ) )
478	470, 477	mpbird 247	. . . 4 |- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) oR <_ ( F ` k ) )
479		itg2ub 23500	. . . 4 |- ( ( ( F ` k ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) e. dom S.1 /\ ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) oR <_ ( F ` k ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) <_ ( S.2 ` ( F ` k ) ) )
480	426, 446, 478, 479	syl3anc 1326	. . 3 |- ( ( ph /\ k e. NN ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) <_ ( S.2 ` ( F ` k ) ) )
481	318	adantl 482	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) )
482	310, 428	itg1mulc 23471	. . . 4 |- ( ( ph /\ k e. NN ) -> ( S.1 ` ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) )
483	444	fveq2d 6195	. . . 4 |- ( ( ph /\ k e. NN ) -> ( S.1 ` ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) )
484	481, 482, 483	3eqtr2d 2662	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) )
485	362	adantl 482	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) = ( S.2 ` ( F ` k ) ) )
486	480, 484, 485	3brtr4d 4685	. 2 |- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) )
487	1, 2, 322, 409, 419, 420, 486	climle 14370	1 |- ( ph -> ( T x. ( S.1 ` H ) ) <_ S )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   U.cuni 4436   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   oRcofr 6896   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   NNcn 11020   (,)cioo 12175   [,)cico 12177   [,]cicc 12178   ~~> cli 14215   volcvol 23232  MblFncmbf 23383   S.1citg1 23384   S.2citg2 23385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cc 9257  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cmp 21190  df-ovol 23233  df-vol 23234  df-mbf 23388  df-itg1 23389  df-itg2 23390

This theorem is referenced by:  itg2monolem3  23519