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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem33.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem33.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem33.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
fourierdlem33.5 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
fourierdlem33.6 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem33.7 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem33.8 ⊢ ( 𝜑 → 𝐶 < 𝐷 )
fourierdlem33.ss ⊢ ( 𝜑 → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
fourierdlem33.y ⊢ 𝑌 = if ( 𝐷 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐷 ) )
fourierdlem33.10 ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) )
Assertion fourierdlem33 ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem33.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem33.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem33.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 fourierdlem33.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
5 fourierdlem33.5 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
6 fourierdlem33.6 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7 fourierdlem33.7 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
8 fourierdlem33.8 ⊢ ( 𝜑 → 𝐶 < 𝐷 )
9 fourierdlem33.ss ⊢ ( 𝜑 → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
10 fourierdlem33.y ⊢ 𝑌 = if ( 𝐷 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐷 ) )
11 fourierdlem33.10 ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
13 iftrue ⊢ ( 𝐷 = 𝐵 → if ( 𝐷 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐷 ) ) = 𝐿 )
14 10 13 eqtr2id ⊢ ( 𝐷 = 𝐵 → 𝐿 = 𝑌 )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐿 = 𝑌 )
16 oveq2 ⊢ ( 𝐷 = 𝐵 → ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) = ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐵 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) = ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐵 ) )
18 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
19 4 18 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
21 9 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
22 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
24 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
25 7 leidd ⊢ ( 𝜑 → 𝐷 ≤ 𝐷 )
26 6 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
27 elioc2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ ) → ( 𝐷 ∈ ( 𝐶 (,] 𝐷 ) ↔ ( 𝐷 ∈ ℝ ∧ 𝐶 < 𝐷 ∧ 𝐷 ≤ 𝐷 ) ) )
28 26 7 27 syl2anc ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐶 (,] 𝐷 ) ↔ ( 𝐷 ∈ ℝ ∧ 𝐶 < 𝐷 ∧ 𝐷 ≤ 𝐷 ) ) )
29 7 8 25 28 mpbir3and ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,] 𝐷 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐷 ∈ ( 𝐶 (,] 𝐷 ) )
31 eqcom ⊢ ( 𝐷 = 𝐵 ↔ 𝐵 = 𝐷 )
32 31 biimpi ⊢ ( 𝐷 = 𝐵 → 𝐵 = 𝐷 )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐵 = 𝐷 )
34 24 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
35 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
36 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
37 ioounsn ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
38 35 36 3 37 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
39 ovex ⊢ ( 𝐴 (,] 𝐵 ) ∈ V
40 39 a1i ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ∈ V )
41 38 40 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ V )
42 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ Top )
43 34 41 42 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ Top )
44 11 43 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ Top )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐽 ∈ Top )
46 oveq2 ⊢ ( 𝐷 = 𝐵 → ( 𝐶 (,] 𝐷 ) = ( 𝐶 (,] 𝐵 ) )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐶 (,] 𝐷 ) = ( 𝐶 (,] 𝐵 ) )
48 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐶 ∈ ℝ* )
49 pnfxr ⊢ +∞ ∈ ℝ*
50 49 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → +∞ ∈ ℝ* )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐶 (,] 𝐵 ) )
52 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐵 ∈ ℝ )
53 elioc2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
54 48 52 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → ( 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
55 51 54 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
56 55 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ℝ )
57 55 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐶 < 𝑥 )
58 56 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 < +∞ )
59 48 50 56 57 58 eliood ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐶 (,) +∞ ) )
60 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 ∈ ℝ )
61 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐶 ∈ ℝ )
62 1 2 6 7 8 9 fourierdlem10 ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) )
63 62 simpld ⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 ≤ 𝐶 )
65 60 61 56 64 57 lelttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 < 𝑥 )
66 55 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
67 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 ∈ ℝ* )
68 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
69 67 52 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
70 56 65 66 69 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) )
71 59 70 elind ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) )
72 elinel1 ⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐶 (,) +∞ ) )
73 elioore ⊢ ( 𝑥 ∈ ( 𝐶 (,) +∞ ) → 𝑥 ∈ ℝ )
74 72 73 syl ⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ℝ )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ℝ )
76 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐶 ∈ ℝ* )
77 49 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → +∞ ∈ ℝ* )
78 72 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐶 (,) +∞ ) )
79 ioogtlb ⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ ( 𝐶 (,) +∞ ) ) → 𝐶 < 𝑥 )
80 76 77 78 79 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐶 < 𝑥 )
81 elinel2 ⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) )
83 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐴 ∈ ℝ* )
84 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐵 ∈ ℝ )
85 83 84 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
86 82 85 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
87 86 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ≤ 𝐵 )
88 76 84 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
89 75 80 87 88 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐶 (,] 𝐵 ) )
90 71 89 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ↔ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) )
91 90 eqrdv ⊢ ( 𝜑 → ( 𝐶 (,] 𝐵 ) = ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) )
92 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
93 92 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
94 iooretop ⊢ ( 𝐶 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
95 94 a1i ⊢ ( 𝜑 → ( 𝐶 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) )
96 elrestr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,] 𝐵 ) ∈ V ∧ ( 𝐶 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) )
97 93 40 95 96 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) )
98 91 97 eqeltrd ⊢ ( 𝜑 → ( 𝐶 (,] 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐶 (,] 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) )
100 47 99 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐶 (,] 𝐷 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) )
101 11 a1i ⊢ ( 𝜑 → 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) )
102 38 oveq2d ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) )
103 34 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
104 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
105 35 2 104 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
106 reex ⊢ ℝ ∈ V
107 106 a1i ⊢ ( 𝜑 → ℝ ∈ V )
108 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 (,] 𝐵 ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐴 (,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) )
109 103 105 107 108 syl3anc ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐴 (,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) )
110 24 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
111 110 eqcomi ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) )
112 111 oveq1i ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐴 (,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) )
113 109 112 eqtr3di ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) )
114 101 102 113 3eqtrrd ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) = 𝐽 )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,] 𝐵 ) ) = 𝐽 )
116 100 115 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐶 (,] 𝐷 ) ∈ 𝐽 )
117 isopn3i ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐶 (,] 𝐷 ) ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐶 (,] 𝐷 ) ) = ( 𝐶 (,] 𝐷 ) )
118 45 116 117 syl2anc ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐶 (,] 𝐷 ) ) = ( 𝐶 (,] 𝐷 ) )
119 30 33 118 3eltr4d ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐵 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐶 (,] 𝐷 ) ) )
120 sneq ⊢ ( 𝐷 = 𝐵 → { 𝐷 } = { 𝐵 } )
121 120 eqcomd ⊢ ( 𝐷 = 𝐵 → { 𝐵 } = { 𝐷 } )
122 121 uneq2d ⊢ ( 𝐷 = 𝐵 → ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐵 } ) = ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐷 } ) )
123 122 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐵 } ) = ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐷 } ) )
124 7 rexrd ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
125 ioounsn ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷 ) → ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐷 } ) = ( 𝐶 (,] 𝐷 ) )
126 26 124 8 125 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐷 } ) = ( 𝐶 (,] 𝐷 ) )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐷 } ) = ( 𝐶 (,] 𝐷 ) )
128 123 127 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐶 (,] 𝐷 ) = ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐵 } ) )
129 128 fveq2d ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐶 (,] 𝐷 ) ) = ( ( int ‘ 𝐽 ) ‘ ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐵 } ) ) )
130 119 129 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝐵 ∈ ( ( int ‘ 𝐽 ) ‘ ( ( 𝐶 (,) 𝐷 ) ∪ { 𝐵 } ) ) )
131 20 21 23 24 11 130 limcres ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )
132 17 131 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) )
133 12 15 132 3eltr3d ⊢ ( ( 𝜑 ∧ 𝐷 = 𝐵 ) → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) )
134 limcresi ⊢ ( 𝐹 limℂ 𝐷 ) ⊆ ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 )
135 iffalse ⊢ ( ¬ 𝐷 = 𝐵 → if ( 𝐷 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐷 ) ) = ( 𝐹 ‘ 𝐷 ) )
136 10 135 syl5eq ⊢ ( ¬ 𝐷 = 𝐵 → 𝑌 = ( 𝐹 ‘ 𝐷 ) )
137 136 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝑌 = ( 𝐹 ‘ 𝐷 ) )
138 ssid ⊢ ℂ ⊆ ℂ
139 138 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
140 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
141 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
142 141 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
143 34 142 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
144 143 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
145 24 140 144 cncfcn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
146 22 139 145 sylancr ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
147 4 146 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
148 24 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
149 22 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
150 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
151 148 149 150 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
152 148 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
153 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
154 151 152 153 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
155 147 154 mpbid ⊢ ( 𝜑 → ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
156 155 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
157 156 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
158 35 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐴 ∈ ℝ* )
159 36 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐵 ∈ ℝ* )
160 7 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐷 ∈ ℝ )
161 1 6 7 63 8 lelttrd ⊢ ( 𝜑 → 𝐴 < 𝐷 )
162 161 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐴 < 𝐷 )
163 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐵 ∈ ℝ )
164 62 simprd ⊢ ( 𝜑 → 𝐷 ≤ 𝐵 )
165 164 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐷 ≤ 𝐵 )
166 neqne ⊢ ( ¬ 𝐷 = 𝐵 → 𝐷 ≠ 𝐵 )
167 166 necomd ⊢ ( ¬ 𝐷 = 𝐵 → 𝐵 ≠ 𝐷 )
168 167 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐵 ≠ 𝐷 )
169 160 163 165 168 leneltd ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐷 < 𝐵 )
170 158 159 160 162 169 eliood ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐷 ∈ ( 𝐴 (,) 𝐵 ) )
171 fveq2 ⊢ ( 𝑥 = 𝐷 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) )
172 171 eleq2d ⊢ ( 𝑥 = 𝐷 → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) ) )
173 172 rspccva ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) )
174 157 170 173 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) )
175 24 140 cnplimc ⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) ↔ ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 limℂ 𝐷 ) ) ) )
176 22 170 175 sylancr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) ↔ ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 limℂ 𝐷 ) ) ) )
177 174 176 mpbid ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 limℂ 𝐷 ) ) )
178 177 simprd ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 limℂ 𝐷 ) )
179 137 178 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝑌 ∈ ( 𝐹 limℂ 𝐷 ) )
180 134 179 sseldi ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = 𝐵 ) → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) )
181 133 180 pm2.61dan ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐷 ) )