Metamath Proof Explorer

Theorem itgulm

Description: A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses itgulm.z 
|- Z = ( ZZ>= ` M )
itgulm.m 
|- ( ph -> M e. ZZ )
itgulm.f 
|- ( ph -> F : Z --> L^1 )
itgulm.u 
|- ( ph -> F ( ~~>u ` S ) G )
itgulm.s 
|- ( ph -> ( vol ` S ) e. RR )
Assertion itgulm 
|- ( ph -> ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) ~~> S. S ( G ` x ) _d x )

Proof

Step Hyp Ref Expression
1 itgulm.z 
 |-  Z = ( ZZ>= ` M )
2 itgulm.m 
 |-  ( ph -> M e. ZZ )
3 itgulm.f 
 |-  ( ph -> F : Z --> L^1 )
4 itgulm.u 
 |-  ( ph -> F ( ~~>u ` S ) G )
5 itgulm.s 
 |-  ( ph -> ( vol ` S ) e. RR )
6 2 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> M e. ZZ )
7 3 ffnd 
 |-  ( ph -> F Fn Z )
8 ulmf2 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : Z --> ( CC ^m S ) )
9 7 4 8 syl2anc 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
10 9 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> F : Z --> ( CC ^m S ) )
11 eqidd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ z e. S ) ) -> ( ( F ` n ) ` z ) = ( ( F ` n ) ` z ) )
12 eqidd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
13 4 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> F ( ~~>u ` S ) G )
14 simpr 
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR+ )
15 5 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> ( vol ` S ) e. RR )
16 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
17 fdm 
 |-  ( G : S --> CC -> dom G = S )
18 4 16 17 3syl 
 |-  ( ph -> dom G = S )
19 1 2 3 4 5 iblulm 
 |-  ( ph -> G e. L^1 )
20 iblmbf 
 |-  ( G e. L^1 -> G e. MblFn )
21 mbfdm 
 |-  ( G e. MblFn -> dom G e. dom vol )
22 19 20 21 3syl 
 |-  ( ph -> dom G e. dom vol )
23 18 22 eqeltrrd 
 |-  ( ph -> S e. dom vol )
24 mblss 
 |-  ( S e. dom vol -> S C_ RR )
25 ovolge0 
 |-  ( S C_ RR -> 0 <_ ( vol* ` S ) )
26 23 24 25 3syl 
 |-  ( ph -> 0 <_ ( vol* ` S ) )
27 mblvol 
 |-  ( S e. dom vol -> ( vol ` S ) = ( vol* ` S ) )
28 23 27 syl 
 |-  ( ph -> ( vol ` S ) = ( vol* ` S ) )
29 26 28 breqtrrd 
 |-  ( ph -> 0 <_ ( vol ` S ) )
30 29 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> 0 <_ ( vol ` S ) )
31 15 30 ge0p1rpd 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( vol ` S ) + 1 ) e. RR+ )
32 14 31 rpdivcld 
 |-  ( ( ph /\ r e. RR+ ) -> ( r / ( ( vol ` S ) + 1 ) ) e. RR+ )
33 1 6 10 11 12 13 32 ulmi 
 |-  ( ( ph /\ r e. RR+ ) -> E. j e. Z A. n e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) )
34 1 uztrn2 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
35 9 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( CC ^m S ) )
36 elmapi 
 |-  ( ( F ` n ) e. ( CC ^m S ) -> ( F ` n ) : S --> CC )
37 35 36 syl 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : S --> CC )
38 37 ffvelrnda 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. S ) -> ( ( F ` n ) ` x ) e. CC )
39 38 adantllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ n e. Z ) /\ x e. S ) -> ( ( F ` n ) ` x ) e. CC )
40 39 adantlrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( ( F ` n ) ` x ) e. CC )
41 37 feqmptd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) = ( x e. S |-> ( ( F ` n ) ` x ) ) )
42 3 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. L^1 )
43 41 42 eqeltrrd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. S |-> ( ( F ` n ) ` x ) ) e. L^1 )
44 43 ad2ant2r 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( x e. S |-> ( ( F ` n ) ` x ) ) e. L^1 )
45 4 16 syl 
 |-  ( ph -> G : S --> CC )
46 45 ffvelrnda 
 |-  ( ( ph /\ x e. S ) -> ( G ` x ) e. CC )
47 46 ad4ant14 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( G ` x ) e. CC )
48 45 feqmptd 
 |-  ( ph -> G = ( x e. S |-> ( G ` x ) ) )
49 48 19 eqeltrrd 
 |-  ( ph -> ( x e. S |-> ( G ` x ) ) e. L^1 )
50 49 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( x e. S |-> ( G ` x ) ) e. L^1 )
51 40 44 47 50 itgsub 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( ( ( F ` n ) ` x ) - ( G ` x ) ) _d x = ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) )
52 51 fveq2d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( abs ` S. S ( ( ( F ` n ) ` x ) - ( G ` x ) ) _d x ) = ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) )
53 40 47 subcld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( ( ( F ` n ) ` x ) - ( G ` x ) ) e. CC )
54 40 44 47 50 iblsub 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( x e. S |-> ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) e. L^1 )
55 53 54 itgcl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( ( ( F ` n ) ` x ) - ( G ` x ) ) _d x e. CC )
56 55 abscld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( abs ` S. S ( ( ( F ` n ) ` x ) - ( G ` x ) ) _d x ) e. RR )
57 53 abscld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) e. RR )
58 53 54 iblabs 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( x e. S |-> ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) ) e. L^1 )
59 57 58 itgrecl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) _d x e. RR )
60 rpre 
 |-  ( r e. RR+ -> r e. RR )
61 60 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> r e. RR )
62 53 54 itgabs 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( abs ` S. S ( ( ( F ` n ) ` x ) - ( G ` x ) ) _d x ) <_ S. S ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) _d x )
63 32 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( r / ( ( vol ` S ) + 1 ) ) e. RR+ )
64 63 rpred 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( r / ( ( vol ` S ) + 1 ) ) e. RR )
65 5 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( vol ` S ) e. RR )
66 64 65 remulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( r / ( ( vol ` S ) + 1 ) ) x. ( vol ` S ) ) e. RR )
67 fconstmpt 
 |-  ( S X. { ( r / ( ( vol ` S ) + 1 ) ) } ) = ( x e. S |-> ( r / ( ( vol ` S ) + 1 ) ) )
68 23 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S e. dom vol )
69 63 rpcnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( r / ( ( vol ` S ) + 1 ) ) e. CC )
70 iblconst 
 |-  ( ( S e. dom vol /\ ( vol ` S ) e. RR /\ ( r / ( ( vol ` S ) + 1 ) ) e. CC ) -> ( S X. { ( r / ( ( vol ` S ) + 1 ) ) } ) e. L^1 )
71 68 65 69 70 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( S X. { ( r / ( ( vol ` S ) + 1 ) ) } ) e. L^1 )
72 67 71 eqeltrrid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( x e. S |-> ( r / ( ( vol ` S ) + 1 ) ) ) e. L^1 )
73 64 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( r / ( ( vol ` S ) + 1 ) ) e. RR )
74 simprr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) )
75 fveq2 
 |-  ( z = x -> ( ( F ` n ) ` z ) = ( ( F ` n ) ` x ) )
76 fveq2 
 |-  ( z = x -> ( G ` z ) = ( G ` x ) )
77 75 76 oveq12d 
 |-  ( z = x -> ( ( ( F ` n ) ` z ) - ( G ` z ) ) = ( ( ( F ` n ) ` x ) - ( G ` x ) ) )
78 77 fveq2d 
 |-  ( z = x -> ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) = ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) )
79 78 breq1d 
 |-  ( z = x -> ( ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) <-> ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) )
80 79 rspccva 
 |-  ( ( A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) /\ x e. S ) -> ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) )
81 74 80 sylan 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) )
82 57 73 81 ltled 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) /\ x e. S ) -> ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) <_ ( r / ( ( vol ` S ) + 1 ) ) )
83 58 72 57 73 82 itgle 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) _d x <_ S. S ( r / ( ( vol ` S ) + 1 ) ) _d x )
84 itgconst 
 |-  ( ( S e. dom vol /\ ( vol ` S ) e. RR /\ ( r / ( ( vol ` S ) + 1 ) ) e. CC ) -> S. S ( r / ( ( vol ` S ) + 1 ) ) _d x = ( ( r / ( ( vol ` S ) + 1 ) ) x. ( vol ` S ) ) )
85 68 65 69 84 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( r / ( ( vol ` S ) + 1 ) ) _d x = ( ( r / ( ( vol ` S ) + 1 ) ) x. ( vol ` S ) ) )
86 83 85 breqtrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) _d x <_ ( ( r / ( ( vol ` S ) + 1 ) ) x. ( vol ` S ) ) )
87 61 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> r e. CC )
88 65 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( vol ` S ) e. CC )
89 31 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( vol ` S ) + 1 ) e. RR+ )
90 89 rpcnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( vol ` S ) + 1 ) e. CC )
91 89 rpne0d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( vol ` S ) + 1 ) =/= 0 )
92 87 88 90 91 div23d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( r x. ( vol ` S ) ) / ( ( vol ` S ) + 1 ) ) = ( ( r / ( ( vol ` S ) + 1 ) ) x. ( vol ` S ) ) )
93 65 ltp1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( vol ` S ) < ( ( vol ` S ) + 1 ) )
94 peano2re 
 |-  ( ( vol ` S ) e. RR -> ( ( vol ` S ) + 1 ) e. RR )
95 65 94 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( vol ` S ) + 1 ) e. RR )
96 rpgt0 
 |-  ( r e. RR+ -> 0 < r )
97 96 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> 0 < r )
98 ltmul2 
 |-  ( ( ( vol ` S ) e. RR /\ ( ( vol ` S ) + 1 ) e. RR /\ ( r e. RR /\ 0 < r ) ) -> ( ( vol ` S ) < ( ( vol ` S ) + 1 ) <-> ( r x. ( vol ` S ) ) < ( r x. ( ( vol ` S ) + 1 ) ) ) )
99 65 95 61 97 98 syl112anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( vol ` S ) < ( ( vol ` S ) + 1 ) <-> ( r x. ( vol ` S ) ) < ( r x. ( ( vol ` S ) + 1 ) ) ) )
100 93 99 mpbid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( r x. ( vol ` S ) ) < ( r x. ( ( vol ` S ) + 1 ) ) )
101 61 65 remulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( r x. ( vol ` S ) ) e. RR )
102 101 61 89 ltdivmul2d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( ( r x. ( vol ` S ) ) / ( ( vol ` S ) + 1 ) ) < r <-> ( r x. ( vol ` S ) ) < ( r x. ( ( vol ` S ) + 1 ) ) ) )
103 100 102 mpbird 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( r x. ( vol ` S ) ) / ( ( vol ` S ) + 1 ) ) < r )
104 92 103 eqbrtrrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( ( r / ( ( vol ` S ) + 1 ) ) x. ( vol ` S ) ) < r )
105 59 66 61 86 104 lelttrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> S. S ( abs ` ( ( ( F ` n ) ` x ) - ( G ` x ) ) ) _d x < r )
106 56 59 61 62 105 lelttrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( abs ` S. S ( ( ( F ` n ) ` x ) - ( G ` x ) ) _d x ) < r )
107 52 106 eqbrtrrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. Z /\ A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) ) ) -> ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r )
108 107 expr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ n e. Z ) -> ( A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) -> ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r ) )
109 34 108 sylan2 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) -> ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r ) )
110 109 anassrs 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ j e. Z ) /\ n e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) -> ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r ) )
111 110 ralimdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ j e. Z ) -> ( A. n e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) -> A. n e. ( ZZ>= ` j ) ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r ) )
112 111 reximdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. j e. Z A. n e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` n ) ` z ) - ( G ` z ) ) ) < ( r / ( ( vol ` S ) + 1 ) ) -> E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r ) )
113 33 112 mpd 
 |-  ( ( ph /\ r e. RR+ ) -> E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r )
114 113 ralrimiva 
 |-  ( ph -> A. r e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r )
115 1 fvexi 
 |-  Z e. _V
116 115 mptex 
 |-  ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) e. _V
117 116 a1i 
 |-  ( ph -> ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) e. _V )
118 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
119 118 fveq1d 
 |-  ( k = n -> ( ( F ` k ) ` x ) = ( ( F ` n ) ` x ) )
120 119 adantr 
 |-  ( ( k = n /\ x e. S ) -> ( ( F ` k ) ` x ) = ( ( F ` n ) ` x ) )
121 120 itgeq2dv 
 |-  ( k = n -> S. S ( ( F ` k ) ` x ) _d x = S. S ( ( F ` n ) ` x ) _d x )
122 eqid 
 |-  ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) = ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x )
123 itgex 
 |-  S. S ( ( F ` n ) ` x ) _d x e. _V
124 121 122 123 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) ` n ) = S. S ( ( F ` n ) ` x ) _d x )
125 124 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) ` n ) = S. S ( ( F ` n ) ` x ) _d x )
126 46 49 itgcl 
 |-  ( ph -> S. S ( G ` x ) _d x e. CC )
127 38 43 itgcl 
 |-  ( ( ph /\ n e. Z ) -> S. S ( ( F ` n ) ` x ) _d x e. CC )
128 1 2 117 125 126 127 clim2c 
 |-  ( ph -> ( ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) ~~> S. S ( G ` x ) _d x <-> A. r e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( S. S ( ( F ` n ) ` x ) _d x - S. S ( G ` x ) _d x ) ) < r ) )
129 114 128 mpbird 
 |-  ( ph -> ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) ~~> S. S ( G ` x ) _d x )