Metamath Proof Explorer


Theorem limcleqr

Description: If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcleqr.k K=TopOpenfld
limcleqr.a φA
limcleqr.j J=topGenran.
limcleqr.f φF:A
limcleqr.b φB
limcleqr.l φLF−∞BlimB
limcleqr.r φRFB+∞limB
limcleqr.leqr φL=R
Assertion limcleqr φLFlimB

Proof

Step Hyp Ref Expression
1 limcleqr.k K=TopOpenfld
2 limcleqr.a φA
3 limcleqr.j J=topGenran.
4 limcleqr.f φF:A
5 limcleqr.b φB
6 limcleqr.l φLF−∞BlimB
7 limcleqr.r φRFB+∞limB
8 limcleqr.leqr φL=R
9 limccl F−∞BlimB
10 9 6 sselid φL
11 simp-4r φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xa+
12 simplr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xb+
13 11 12 ifcld φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xifabab+
14 nfv zφx+
15 nfv za+
16 14 15 nfan zφx+a+
17 nfra1 zzA−∞BzBzB<aF−∞BzL<x
18 16 17 nfan zφx+a+zA−∞BzBzB<aF−∞BzL<x
19 nfv zb+
20 18 19 nfan zφx+a+zA−∞BzBzB<aF−∞BzL<xb+
21 nfra1 zzAB+∞zBzB<bFB+∞zL<x
22 20 21 nfan zφx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<x
23 simp-6l φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xz<Bφ
24 23 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<Bφ
25 simpl2 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzA
26 simpr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<Bz<B
27 mnfxr −∞*
28 27 a1i φzAz<B−∞*
29 5 rexrd φB*
30 29 3ad2ant1 φzAz<BB*
31 2 sselda φzAz
32 31 3adant3 φzAz<Bz
33 32 mnfltd φzAz<B−∞<z
34 simp3 φzAz<Bz<B
35 28 30 32 33 34 eliood φzAz<Bz−∞B
36 24 25 26 35 syl3anc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<Bz−∞B
37 fvres z−∞BF−∞Bz=Fz
38 37 oveq1d z−∞BF−∞BzL=FzL
39 38 eqcomd z−∞BFzL=F−∞BzL
40 39 fveq2d z−∞BFzL=F−∞BzL
41 36 40 syl φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BFzL=F−∞BzL
42 simp-4r φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xz<BzA−∞BzBzB<aF−∞BzL<x
43 42 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzA−∞BzBzB<aF−∞BzL<x
44 25 36 elind φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzA−∞B
45 43 44 jca φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzA−∞BzBzB<aF−∞BzL<xzA−∞B
46 simpl3l φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzB
47 11 adantr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xz<Ba+
48 47 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<Ba+
49 12 adantr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xz<Bb+
50 49 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<Bb+
51 simpl3r φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzB<ifabab
52 simpl1 φa+b+zB<ifababzAφ
53 simprr φa+b+zB<ifababzAzA
54 31 recnd φzAz
55 5 recnd φB
56 55 adantr φzAB
57 54 56 subcld φzAzB
58 57 abscld φzAzB
59 52 53 58 syl2anc φa+b+zB<ifababzAzB
60 rpre a+a
61 60 adantr a+b+a
62 rpre b+b
63 62 adantl a+b+b
64 61 63 ifcld a+b+ifabab
65 64 3adant1 φa+b+ifabab
66 65 adantr φa+b+zB<ifababzAifabab
67 61 3adant1 φa+b+a
68 67 adantr φa+b+zB<ifababzAa
69 simprl φa+b+zB<ifababzAzB<ifabab
70 63 3adant1 φa+b+b
71 min1 abifababa
72 67 70 71 syl2anc φa+b+ifababa
73 72 adantr φa+b+zB<ifababzAifababa
74 59 66 68 69 73 ltletrd φa+b+zB<ifababzAzB<a
75 24 48 50 51 25 74 syl32anc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzB<a
76 46 75 jca φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BzBzB<a
77 rspa zA−∞BzBzB<aF−∞BzL<xzA−∞BzBzB<aF−∞BzL<x
78 45 76 77 sylc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BF−∞BzL<x
79 41 78 eqbrtrd φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababz<BFzL<x
80 simp-6l φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<x¬z<Bφ
81 80 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<Bφ
82 81 5 syl φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<BB
83 simpl2 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<BzA
84 81 83 31 syl2anc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<Bz
85 id zBzB
86 85 necomd zBBz
87 86 ad2antrr zBzB<ifabab¬z<BBz
88 87 3ad2antl3 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<BBz
89 simpr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<B¬z<B
90 82 84 88 89 lttri5d φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<BB<z
91 simp-6l φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xB<zφ
92 91 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zφ
93 simpl2 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzA
94 simpr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zB<z
95 29 3ad2ant1 φzAB<zB*
96 pnfxr +∞*
97 96 a1i φzAB<z+∞*
98 31 3adant3 φzAB<zz
99 simp3 φzAB<zB<z
100 98 ltpnfd φzAB<zz<+∞
101 95 97 98 99 100 eliood φzAB<zzB+∞
102 92 93 94 101 syl3anc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzB+∞
103 fvres zB+∞FB+∞z=Fz
104 103 eqcomd zB+∞Fz=FB+∞z
105 104 fvoveq1d zB+∞FzL=FB+∞zL
106 102 105 syl φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zFzL=FB+∞zL
107 simpl1r φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzAB+∞zBzB<bFB+∞zL<x
108 93 102 elind φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzAB+∞
109 107 108 jca φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzAB+∞zBzB<bFB+∞zL<xzAB+∞
110 simpl3l φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzB
111 11 adantr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xB<za+
112 111 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<za+
113 12 adantr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xB<zb+
114 113 3ad2antl1 φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zb+
115 simpl3r φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzB<ifabab
116 70 adantr φa+b+zB<ifababzAb
117 min2 abifababb
118 67 70 117 syl2anc φa+b+ifababb
119 118 adantr φa+b+zB<ifababzAifababb
120 59 66 116 69 119 ltletrd φa+b+zB<ifababzAzB<b
121 92 112 114 115 93 120 syl32anc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzB<b
122 110 121 jca φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zzBzB<b
123 rspa zAB+∞zBzB<bFB+∞zL<xzAB+∞zBzB<bFB+∞zL<x
124 109 122 123 sylc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zFB+∞zL<x
125 106 124 eqbrtrd φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababB<zFzL<x
126 90 125 syldan φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifabab¬z<BFzL<x
127 79 126 pm2.61dan φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababFzL<x
128 127 3exp φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababFzL<x
129 22 128 ralrimi φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xzAzBzB<ifababFzL<x
130 brimralrspcev ifabab+zAzBzB<ifababFzL<xy+zAzBzB<yFzL<x
131 13 129 130 syl2anc φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<xy+zAzBzB<yFzL<x
132 fresin F:AFB+∞:AB+∞
133 4 132 syl φFB+∞:AB+∞
134 inss2 AB+∞B+∞
135 ioosscn B+∞
136 134 135 sstri AB+∞
137 136 a1i φAB+∞
138 133 137 55 ellimc3 φRFB+∞limBRx+b+zAB+∞zBzB<bFB+∞zR<x
139 7 138 mpbid φRx+b+zAB+∞zBzB<bFB+∞zR<x
140 139 simprd φx+b+zAB+∞zBzB<bFB+∞zR<x
141 140 r19.21bi φx+b+zAB+∞zBzB<bFB+∞zR<x
142 8 oveq2d φFB+∞zL=FB+∞zR
143 142 fveq2d φFB+∞zL=FB+∞zR
144 143 breq1d φFB+∞zL<xFB+∞zR<x
145 144 imbi2d φzBzB<bFB+∞zL<xzBzB<bFB+∞zR<x
146 145 rexralbidv φb+zAB+∞zBzB<bFB+∞zL<xb+zAB+∞zBzB<bFB+∞zR<x
147 146 adantr φx+b+zAB+∞zBzB<bFB+∞zL<xb+zAB+∞zBzB<bFB+∞zR<x
148 141 147 mpbird φx+b+zAB+∞zBzB<bFB+∞zL<x
149 148 ad2antrr φx+a+zA−∞BzBzB<aF−∞BzL<xb+zAB+∞zBzB<bFB+∞zL<x
150 131 149 r19.29a φx+a+zA−∞BzBzB<aF−∞BzL<xy+zAzBzB<yFzL<x
151 fresin F:AF−∞B:A−∞B
152 4 151 syl φF−∞B:A−∞B
153 inss2 A−∞B−∞B
154 ioossre −∞B
155 153 154 sstri A−∞B
156 ax-resscn
157 156 a1i φ
158 155 157 sstrid φA−∞B
159 152 158 55 ellimc3 φLF−∞BlimBLx+a+zA−∞BzBzB<aF−∞BzL<x
160 6 159 mpbid φLx+a+zA−∞BzBzB<aF−∞BzL<x
161 160 simprd φx+a+zA−∞BzBzB<aF−∞BzL<x
162 161 r19.21bi φx+a+zA−∞BzBzB<aF−∞BzL<x
163 150 162 r19.29a φx+y+zAzBzB<yFzL<x
164 163 ralrimiva φx+y+zAzBzB<yFzL<x
165 2 156 sstrdi φA
166 4 165 55 ellimc3 φLFlimBLx+y+zAzBzB<yFzL<x
167 10 164 166 mpbir2and φLFlimB