Metamath Proof Explorer

Theorem rlimsqzlem

Description: Lemma for rlimsqz and rlimsqz2 . (Contributed by Mario Carneiro, 18-Sep-2014) (Revised by Mario Carneiro, 20-May-2016)

Ref Expression
Hypotheses rlimsqzlem.m 
|- ( ph -> M e. RR )
rlimsqzlem.e 
|- ( ph -> E e. CC )
rlimsqzlem.1 
|- ( ph -> ( x e. A |-> B ) ~~>r D )
rlimsqzlem.2 
|- ( ( ph /\ x e. A ) -> B e. CC )
rlimsqzlem.3 
|- ( ( ph /\ x e. A ) -> C e. CC )
rlimsqzlem.4 
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )
Assertion rlimsqzlem 
|- ( ph -> ( x e. A |-> C ) ~~>r E )

Proof

Step Hyp Ref Expression
1 rlimsqzlem.m 
 |-  ( ph -> M e. RR )
2 rlimsqzlem.e 
 |-  ( ph -> E e. CC )
3 rlimsqzlem.1 
 |-  ( ph -> ( x e. A |-> B ) ~~>r D )
4 rlimsqzlem.2 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 rlimsqzlem.3 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
6 rlimsqzlem.4 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )
7 1 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> M e. RR )
8 1 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. A ) -> M e. RR )
9 elicopnf 
 |-  ( M e. RR -> ( z e. ( M [,) +oo ) <-> ( z e. RR /\ M <_ z ) ) )
10 8 9 syl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. A ) -> ( z e. ( M [,) +oo ) <-> ( z e. RR /\ M <_ z ) ) )
11 10 simprbda 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ z e. ( M [,) +oo ) ) -> z e. RR )
12 11 adantrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> z e. RR )
13 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
14 13 4 dmmptd 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
15 rlimss 
 |-  ( ( x e. A |-> B ) ~~>r D -> dom ( x e. A |-> B ) C_ RR )
16 3 15 syl 
 |-  ( ph -> dom ( x e. A |-> B ) C_ RR )
17 14 16 eqsstrrd 
 |-  ( ph -> A C_ RR )
18 17 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> A C_ RR )
19 18 sselda 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. A ) -> x e. RR )
20 19 adantr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> x e. RR )
21 10 simplbda 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ z e. ( M [,) +oo ) ) -> M <_ z )
22 21 adantrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> M <_ z )
23 simprr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> z <_ x )
24 7 12 20 22 23 letrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> M <_ x )
25 6 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ M <_ x ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )
26 25 adantllr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ M <_ x ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )
27 24 26 syldan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )
28 2 adantr 
 |-  ( ( ph /\ x e. A ) -> E e. CC )
29 5 28 subcld 
 |-  ( ( ph /\ x e. A ) -> ( C - E ) e. CC )
30 29 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( C - E ) ) e. RR )
31 30 ad4ant13 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> ( abs ` ( C - E ) ) e. RR )
32 rlimcl 
 |-  ( ( x e. A |-> B ) ~~>r D -> D e. CC )
33 3 32 syl 
 |-  ( ph -> D e. CC )
34 33 adantr 
 |-  ( ( ph /\ x e. A ) -> D e. CC )
35 4 34 subcld 
 |-  ( ( ph /\ x e. A ) -> ( B - D ) e. CC )
36 35 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( B - D ) ) e. RR )
37 36 ad4ant13 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> ( abs ` ( B - D ) ) e. RR )
38 rpre 
 |-  ( y e. RR+ -> y e. RR )
39 38 ad3antlr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> y e. RR )
40 lelttr 
 |-  ( ( ( abs ` ( C - E ) ) e. RR /\ ( abs ` ( B - D ) ) e. RR /\ y e. RR ) -> ( ( ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) /\ ( abs ` ( B - D ) ) < y ) -> ( abs ` ( C - E ) ) < y ) )
41 31 37 39 40 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> ( ( ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) /\ ( abs ` ( B - D ) ) < y ) -> ( abs ` ( C - E ) ) < y ) )
42 27 41 mpand 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ ( z e. ( M [,) +oo ) /\ z <_ x ) ) -> ( ( abs ` ( B - D ) ) < y -> ( abs ` ( C - E ) ) < y ) )
43 42 expr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ x e. A ) /\ z e. ( M [,) +oo ) ) -> ( z <_ x -> ( ( abs ` ( B - D ) ) < y -> ( abs ` ( C - E ) ) < y ) ) )
44 43 an32s 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ z e. ( M [,) +oo ) ) /\ x e. A ) -> ( z <_ x -> ( ( abs ` ( B - D ) ) < y -> ( abs ` ( C - E ) ) < y ) ) )
45 44 a2d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ z e. ( M [,) +oo ) ) /\ x e. A ) -> ( ( z <_ x -> ( abs ` ( B - D ) ) < y ) -> ( z <_ x -> ( abs ` ( C - E ) ) < y ) ) )
46 45 ralimdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ z e. ( M [,) +oo ) ) -> ( A. x e. A ( z <_ x -> ( abs ` ( B - D ) ) < y ) -> A. x e. A ( z <_ x -> ( abs ` ( C - E ) ) < y ) ) )
47 46 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. z e. ( M [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( B - D ) ) < y ) -> E. z e. ( M [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( C - E ) ) < y ) ) )
48 47 ralimdva 
 |-  ( ph -> ( A. y e. RR+ E. z e. ( M [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( B - D ) ) < y ) -> A. y e. RR+ E. z e. ( M [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( C - E ) ) < y ) ) )
49 4 ralrimiva 
 |-  ( ph -> A. x e. A B e. CC )
50 49 17 33 1 rlim3 
 |-  ( ph -> ( ( x e. A |-> B ) ~~>r D <-> A. y e. RR+ E. z e. ( M [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( B - D ) ) < y ) ) )
51 5 ralrimiva 
 |-  ( ph -> A. x e. A C e. CC )
52 51 17 2 1 rlim3 
 |-  ( ph -> ( ( x e. A |-> C ) ~~>r E <-> A. y e. RR+ E. z e. ( M [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( C - E ) ) < y ) ) )
53 48 50 52 3imtr4d 
 |-  ( ph -> ( ( x e. A |-> B ) ~~>r D -> ( x e. A |-> C ) ~~>r E ) )
54 3 53 mpd 
 |-  ( ph -> ( x e. A |-> C ) ~~>r E )