Metamath Proof Explorer


Theorem fourierdlem33

Description: Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem33.1 φA
fourierdlem33.2 φB
fourierdlem33.3 φA<B
fourierdlem33.4 φF:ABcn
fourierdlem33.5 φLFlimB
fourierdlem33.6 φC
fourierdlem33.7 φD
fourierdlem33.8 φC<D
fourierdlem33.ss φCDAB
fourierdlem33.y Y=ifD=BLFD
fourierdlem33.10 J=TopOpenfld𝑡ABB
Assertion fourierdlem33 φYFCDlimD

Proof

Step Hyp Ref Expression
1 fourierdlem33.1 φA
2 fourierdlem33.2 φB
3 fourierdlem33.3 φA<B
4 fourierdlem33.4 φF:ABcn
5 fourierdlem33.5 φLFlimB
6 fourierdlem33.6 φC
7 fourierdlem33.7 φD
8 fourierdlem33.8 φC<D
9 fourierdlem33.ss φCDAB
10 fourierdlem33.y Y=ifD=BLFD
11 fourierdlem33.10 J=TopOpenfld𝑡ABB
12 5 adantr φD=BLFlimB
13 iftrue D=BifD=BLFD=L
14 10 13 eqtr2id D=BL=Y
15 14 adantl φD=BL=Y
16 oveq2 D=BFCDlimD=FCDlimB
17 16 adantl φD=BFCDlimD=FCDlimB
18 cncff F:ABcnF:AB
19 4 18 syl φF:AB
20 19 adantr φD=BF:AB
21 9 adantr φD=BCDAB
22 ioosscn AB
23 22 a1i φD=BAB
24 eqid TopOpenfld=TopOpenfld
25 7 leidd φDD
26 6 rexrd φC*
27 elioc2 C*DDCDDC<DDD
28 26 7 27 syl2anc φDCDDC<DDD
29 7 8 25 28 mpbir3and φDCD
30 29 adantr φD=BDCD
31 eqcom D=BB=D
32 31 biimpi D=BB=D
33 32 adantl φD=BB=D
34 24 cnfldtop TopOpenfldTop
35 1 rexrd φA*
36 2 rexrd φB*
37 ioounsn A*B*A<BABB=AB
38 35 36 3 37 syl3anc φABB=AB
39 ovex ABV
40 39 a1i φABV
41 38 40 eqeltrd φABBV
42 resttop TopOpenfldTopABBVTopOpenfld𝑡ABBTop
43 34 41 42 sylancr φTopOpenfld𝑡ABBTop
44 11 43 eqeltrid φJTop
45 44 adantr φD=BJTop
46 oveq2 D=BCD=CB
47 46 adantl φD=BCD=CB
48 26 adantr φxCBC*
49 pnfxr +∞*
50 49 a1i φxCB+∞*
51 simpr φxCBxCB
52 2 adantr φxCBB
53 elioc2 C*BxCBxC<xxB
54 48 52 53 syl2anc φxCBxCBxC<xxB
55 51 54 mpbid φxCBxC<xxB
56 55 simp1d φxCBx
57 55 simp2d φxCBC<x
58 56 ltpnfd φxCBx<+∞
59 48 50 56 57 58 eliood φxCBxC+∞
60 1 adantr φxCBA
61 6 adantr φxCBC
62 1 2 6 7 8 9 fourierdlem10 φACDB
63 62 simpld φAC
64 63 adantr φxCBAC
65 60 61 56 64 57 lelttrd φxCBA<x
66 55 simp3d φxCBxB
67 35 adantr φxCBA*
68 elioc2 A*BxABxA<xxB
69 67 52 68 syl2anc φxCBxABxA<xxB
70 56 65 66 69 mpbir3and φxCBxAB
71 59 70 elind φxCBxC+∞AB
72 elinel1 xC+∞ABxC+∞
73 elioore xC+∞x
74 72 73 syl xC+∞ABx
75 74 adantl φxC+∞ABx
76 26 adantr φxC+∞ABC*
77 49 a1i φxC+∞AB+∞*
78 72 adantl φxC+∞ABxC+∞
79 ioogtlb C*+∞*xC+∞C<x
80 76 77 78 79 syl3anc φxC+∞ABC<x
81 elinel2 xC+∞ABxAB
82 81 adantl φxC+∞ABxAB
83 35 adantr φxC+∞ABA*
84 2 adantr φxC+∞ABB
85 83 84 68 syl2anc φxC+∞ABxABxA<xxB
86 82 85 mpbid φxC+∞ABxA<xxB
87 86 simp3d φxC+∞ABxB
88 76 84 53 syl2anc φxC+∞ABxCBxC<xxB
89 75 80 87 88 mpbir3and φxC+∞ABxCB
90 71 89 impbida φxCBxC+∞AB
91 90 eqrdv φCB=C+∞AB
92 retop topGenran.Top
93 92 a1i φtopGenran.Top
94 iooretop C+∞topGenran.
95 94 a1i φC+∞topGenran.
96 elrestr topGenran.TopABVC+∞topGenran.C+∞ABtopGenran.𝑡AB
97 93 40 95 96 syl3anc φC+∞ABtopGenran.𝑡AB
98 91 97 eqeltrd φCBtopGenran.𝑡AB
99 98 adantr φD=BCBtopGenran.𝑡AB
100 47 99 eqeltrd φD=BCDtopGenran.𝑡AB
101 11 a1i φJ=TopOpenfld𝑡ABB
102 38 oveq2d φTopOpenfld𝑡ABB=TopOpenfld𝑡AB
103 34 a1i φTopOpenfldTop
104 iocssre A*BAB
105 35 2 104 syl2anc φAB
106 reex V
107 106 a1i φV
108 restabs TopOpenfldTopABVTopOpenfld𝑡𝑡AB=TopOpenfld𝑡AB
109 103 105 107 108 syl3anc φTopOpenfld𝑡𝑡AB=TopOpenfld𝑡AB
110 24 tgioo2 topGenran.=TopOpenfld𝑡
111 110 eqcomi TopOpenfld𝑡=topGenran.
112 111 oveq1i TopOpenfld𝑡𝑡AB=topGenran.𝑡AB
113 109 112 eqtr3di φTopOpenfld𝑡AB=topGenran.𝑡AB
114 101 102 113 3eqtrrd φtopGenran.𝑡AB=J
115 114 adantr φD=BtopGenran.𝑡AB=J
116 100 115 eleqtrd φD=BCDJ
117 isopn3i JTopCDJintJCD=CD
118 45 116 117 syl2anc φD=BintJCD=CD
119 30 33 118 3eltr4d φD=BBintJCD
120 sneq D=BD=B
121 120 eqcomd D=BB=D
122 121 uneq2d D=BCDB=CDD
123 122 adantl φD=BCDB=CDD
124 7 rexrd φD*
125 ioounsn C*D*C<DCDD=CD
126 26 124 8 125 syl3anc φCDD=CD
127 126 adantr φD=BCDD=CD
128 123 127 eqtr2d φD=BCD=CDB
129 128 fveq2d φD=BintJCD=intJCDB
130 119 129 eleqtrd φD=BBintJCDB
131 20 21 23 24 11 130 limcres φD=BFCDlimB=FlimB
132 17 131 eqtr2d φD=BFlimB=FCDlimD
133 12 15 132 3eltr3d φD=BYFCDlimD
134 limcresi FlimDFCDlimD
135 iffalse ¬D=BifD=BLFD=FD
136 10 135 eqtrid ¬D=BY=FD
137 136 adantl φ¬D=BY=FD
138 ssid
139 138 a1i φ
140 eqid TopOpenfld𝑡AB=TopOpenfld𝑡AB
141 unicntop =TopOpenfld
142 141 restid TopOpenfldTopTopOpenfld𝑡=TopOpenfld
143 34 142 ax-mp TopOpenfld𝑡=TopOpenfld
144 143 eqcomi TopOpenfld=TopOpenfld𝑡
145 24 140 144 cncfcn ABABcn=TopOpenfld𝑡ABCnTopOpenfld
146 22 139 145 sylancr φABcn=TopOpenfld𝑡ABCnTopOpenfld
147 4 146 eleqtrd φFTopOpenfld𝑡ABCnTopOpenfld
148 24 cnfldtopon TopOpenfldTopOn
149 22 a1i φAB
150 resttopon TopOpenfldTopOnABTopOpenfld𝑡ABTopOnAB
151 148 149 150 sylancr φTopOpenfld𝑡ABTopOnAB
152 148 a1i φTopOpenfldTopOn
153 cncnp TopOpenfld𝑡ABTopOnABTopOpenfldTopOnFTopOpenfld𝑡ABCnTopOpenfldF:ABxABFTopOpenfld𝑡ABCnPTopOpenfldx
154 151 152 153 syl2anc φFTopOpenfld𝑡ABCnTopOpenfldF:ABxABFTopOpenfld𝑡ABCnPTopOpenfldx
155 147 154 mpbid φF:ABxABFTopOpenfld𝑡ABCnPTopOpenfldx
156 155 simprd φxABFTopOpenfld𝑡ABCnPTopOpenfldx
157 156 adantr φ¬D=BxABFTopOpenfld𝑡ABCnPTopOpenfldx
158 35 adantr φ¬D=BA*
159 36 adantr φ¬D=BB*
160 7 adantr φ¬D=BD
161 1 6 7 63 8 lelttrd φA<D
162 161 adantr φ¬D=BA<D
163 2 adantr φ¬D=BB
164 62 simprd φDB
165 164 adantr φ¬D=BDB
166 neqne ¬D=BDB
167 166 necomd ¬D=BBD
168 167 adantl φ¬D=BBD
169 160 163 165 168 leneltd φ¬D=BD<B
170 158 159 160 162 169 eliood φ¬D=BDAB
171 fveq2 x=DTopOpenfld𝑡ABCnPTopOpenfldx=TopOpenfld𝑡ABCnPTopOpenfldD
172 171 eleq2d x=DFTopOpenfld𝑡ABCnPTopOpenfldxFTopOpenfld𝑡ABCnPTopOpenfldD
173 172 rspccva xABFTopOpenfld𝑡ABCnPTopOpenfldxDABFTopOpenfld𝑡ABCnPTopOpenfldD
174 157 170 173 syl2anc φ¬D=BFTopOpenfld𝑡ABCnPTopOpenfldD
175 24 140 cnplimc ABDABFTopOpenfld𝑡ABCnPTopOpenfldDF:ABFDFlimD
176 22 170 175 sylancr φ¬D=BFTopOpenfld𝑡ABCnPTopOpenfldDF:ABFDFlimD
177 174 176 mpbid φ¬D=BF:ABFDFlimD
178 177 simprd φ¬D=BFDFlimD
179 137 178 eqeltrd φ¬D=BYFlimD
180 134 179 sselid φ¬D=BYFCDlimD
181 133 180 pm2.61dan φYFCDlimD