Metamath Proof Explorer

Theorem fourierdlem32

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

Ref Expression
Hypotheses fourierdlem32.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem32.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem32.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem32.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
fourierdlem32.l ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
fourierdlem32.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem32.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem32.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
fourierdlem32.ss ⊢ ( 𝜑 → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
fourierdlem32.y ⊢ 𝑌 = if ( 𝐶 = 𝐴 , 𝑅 , ( 𝐹 ‘ 𝐶 ) )
fourierdlem32.j ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,) 𝐵 ) )
Assertion fourierdlem32 ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝐶 (,) 𝐷 ) ) limℂ 𝐶 ) )

Proof

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