Metamath Proof Explorer

Theorem dvfsumrlim3

Description: Conjoin the statements of dvfsumrlim and dvfsumrlim2 . (This is useful as a target for lemmas, because the hypotheses to this theorem are complex, and we don't want to repeat ourselves.) (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvfsum.s 
|- S = ( T (,) +oo )
dvfsum.z 
|- Z = ( ZZ>= ` M )
dvfsum.m 
|- ( ph -> M e. ZZ )
dvfsum.d 
|- ( ph -> D e. RR )
dvfsum.md 
|- ( ph -> M <_ ( D + 1 ) )
dvfsum.t 
|- ( ph -> T e. RR )
dvfsum.a 
|- ( ( ph /\ x e. S ) -> A e. RR )
dvfsum.b1 
|- ( ( ph /\ x e. S ) -> B e. V )
dvfsum.b2 
|- ( ( ph /\ x e. Z ) -> B e. RR )
dvfsum.b3 
|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
dvfsum.c 
|- ( x = k -> B = C )
dvfsumrlim.l 
|- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )
dvfsumrlim.g 
|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
dvfsumrlim.k 
|- ( ph -> ( x e. S |-> B ) ~~>r 0 )
dvfsumrlim3.1 
|- ( x = X -> B = E )
Assertion dvfsumrlim3 
|- ( ph -> ( G : S --> RR /\ G e. dom ~~>r /\ ( ( G ~~>r L /\ X e. S /\ D <_ X ) -> ( abs ` ( ( G ` X ) - L ) ) <_ E ) ) )

Proof

Step Hyp Ref Expression
1 dvfsum.s 
 |-  S = ( T (,) +oo )
2 dvfsum.z 
 |-  Z = ( ZZ>= ` M )
3 dvfsum.m 
 |-  ( ph -> M e. ZZ )
4 dvfsum.d 
 |-  ( ph -> D e. RR )
5 dvfsum.md 
 |-  ( ph -> M <_ ( D + 1 ) )
6 dvfsum.t 
 |-  ( ph -> T e. RR )
7 dvfsum.a 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
8 dvfsum.b1 
 |-  ( ( ph /\ x e. S ) -> B e. V )
9 dvfsum.b2 
 |-  ( ( ph /\ x e. Z ) -> B e. RR )
10 dvfsum.b3 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
11 dvfsum.c 
 |-  ( x = k -> B = C )
12 dvfsumrlim.l 
 |-  ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )
13 dvfsumrlim.g 
 |-  G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
14 dvfsumrlim.k 
 |-  ( ph -> ( x e. S |-> B ) ~~>r 0 )
15 dvfsumrlim3.1 
 |-  ( x = X -> B = E )
16 1 2 3 4 5 6 7 8 9 10 11 13 dvfsumrlimf 
 |-  ( ph -> G : S --> RR )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dvfsumrlim 
 |-  ( ph -> G e. dom ~~>r )
18 3 adantr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> M e. ZZ )
19 4 adantr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> D e. RR )
20 5 adantr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> M <_ ( D + 1 ) )
21 6 adantr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> T e. RR )
22 7 adantlr 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ x e. S ) -> A e. RR )
23 8 adantlr 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ x e. S ) -> B e. V )
24 9 adantlr 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ x e. Z ) -> B e. RR )
25 10 adantr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
26 12 3adant1r 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )
27 14 adantr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> ( x e. S |-> B ) ~~>r 0 )
28 simprr 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> X e. S )
29 simprl 
 |-  ( ( ph /\ ( D <_ X /\ X e. S ) ) -> D <_ X )
30 1 2 18 19 20 21 22 23 24 25 11 26 13 27 28 29 dvfsumrlim2 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ G ~~>r L ) -> ( abs ` ( ( G ` X ) - L ) ) <_ [_ X / x ]_ B )
31 28 adantr 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ G ~~>r L ) -> X e. S )
32 nfcvd 
 |-  ( X e. S -> F/_ x E )
33 32 15 csbiegf 
 |-  ( X e. S -> [_ X / x ]_ B = E )
34 31 33 syl 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ G ~~>r L ) -> [_ X / x ]_ B = E )
35 30 34 breqtrd 
 |-  ( ( ( ph /\ ( D <_ X /\ X e. S ) ) /\ G ~~>r L ) -> ( abs ` ( ( G ` X ) - L ) ) <_ E )
36 35 exp42 
 |-  ( ph -> ( D <_ X -> ( X e. S -> ( G ~~>r L -> ( abs ` ( ( G ` X ) - L ) ) <_ E ) ) ) )
37 36 com24 
 |-  ( ph -> ( G ~~>r L -> ( X e. S -> ( D <_ X -> ( abs ` ( ( G ` X ) - L ) ) <_ E ) ) ) )
38 37 3impd 
 |-  ( ph -> ( ( G ~~>r L /\ X e. S /\ D <_ X ) -> ( abs ` ( ( G ` X ) - L ) ) <_ E ) )
39 16 17 38 3jca 
 |-  ( ph -> ( G : S --> RR /\ G e. dom ~~>r /\ ( ( G ~~>r L /\ X e. S /\ D <_ X ) -> ( abs ` ( ( G ` X ) - L ) ) <_ E ) ) )