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