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 φM
rlimsqzlem.e φE
rlimsqzlem.1 φxABD
rlimsqzlem.2 φxAB
rlimsqzlem.3 φxAC
rlimsqzlem.4 φxAMxCEBD
Assertion rlimsqzlem φxACE

Proof

Step Hyp Ref Expression
1 rlimsqzlem.m φM
2 rlimsqzlem.e φE
3 rlimsqzlem.1 φxABD
4 rlimsqzlem.2 φxAB
5 rlimsqzlem.3 φxAC
6 rlimsqzlem.4 φxAMxCEBD
7 1 ad3antrrr φy+xAzM+∞zxM
8 1 ad2antrr φy+xAM
9 elicopnf MzM+∞zMz
10 8 9 syl φy+xAzM+∞zMz
11 10 simprbda φy+xAzM+∞z
12 11 adantrr φy+xAzM+∞zxz
13 eqid xAB=xAB
14 13 4 dmmptd φdomxAB=A
15 rlimss xABDdomxAB
16 3 15 syl φdomxAB
17 14 16 eqsstrrd φA
18 17 adantr φy+A
19 18 sselda φy+xAx
20 19 adantr φy+xAzM+∞zxx
21 10 simplbda φy+xAzM+∞Mz
22 21 adantrr φy+xAzM+∞zxMz
23 simprr φy+xAzM+∞zxzx
24 7 12 20 22 23 letrd φy+xAzM+∞zxMx
25 6 anassrs φxAMxCEBD
26 25 adantllr φy+xAMxCEBD
27 24 26 syldan φy+xAzM+∞zxCEBD
28 2 adantr φxAE
29 5 28 subcld φxACE
30 29 abscld φxACE
31 30 ad4ant13 φy+xAzM+∞zxCE
32 rlimcl xABDD
33 3 32 syl φD
34 33 adantr φxAD
35 4 34 subcld φxABD
36 35 abscld φxABD
37 36 ad4ant13 φy+xAzM+∞zxBD
38 rpre y+y
39 38 ad3antlr φy+xAzM+∞zxy
40 lelttr CEBDyCEBDBD<yCE<y
41 31 37 39 40 syl3anc φy+xAzM+∞zxCEBDBD<yCE<y
42 27 41 mpand φy+xAzM+∞zxBD<yCE<y
43 42 expr φy+xAzM+∞zxBD<yCE<y
44 43 an32s φy+zM+∞xAzxBD<yCE<y
45 44 a2d φy+zM+∞xAzxBD<yzxCE<y
46 45 ralimdva φy+zM+∞xAzxBD<yxAzxCE<y
47 46 reximdva φy+zM+∞xAzxBD<yzM+∞xAzxCE<y
48 47 ralimdva φy+zM+∞xAzxBD<yy+zM+∞xAzxCE<y
49 4 ralrimiva φxAB
50 49 17 33 1 rlim3 φxABDy+zM+∞xAzxBD<y
51 5 ralrimiva φxAC
52 51 17 2 1 rlim3 φxACEy+zM+∞xAzxCE<y
53 48 50 52 3imtr4d φxABDxACE
54 3 53 mpd φxACE