Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem32 Structured version   Visualization version   GIF version

Theorem fourierdlem32 45697
Description: Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
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
Ref Expression
fourierdlem32 (𝜑𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶))

Proof of Theorem fourierdlem32
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem32.l . . . 4 (𝜑𝑅 ∈ (𝐹 lim 𝐴))
21adantr 479 . . 3 ((𝜑𝐶 = 𝐴) → 𝑅 ∈ (𝐹 lim 𝐴))
3 fourierdlem32.y . . . . 5 𝑌 = if(𝐶 = 𝐴, 𝑅, (𝐹𝐶))
4 iftrue 4538 . . . . 5 (𝐶 = 𝐴 → if(𝐶 = 𝐴, 𝑅, (𝐹𝐶)) = 𝑅)
53, 4eqtr2id 2778 . . . 4 (𝐶 = 𝐴𝑅 = 𝑌)
65adantl 480 . . 3 ((𝜑𝐶 = 𝐴) → 𝑅 = 𝑌)
7 oveq2 7431 . . . . 5 (𝐶 = 𝐴 → ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶) = ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐴))
87adantl 480 . . . 4 ((𝜑𝐶 = 𝐴) → ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶) = ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐴))
9 fourierdlem32.f . . . . . . 7 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
10 cncff 24896 . . . . . . 7 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
119, 10syl 17 . . . . . 6 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
1211adantr 479 . . . . 5 ((𝜑𝐶 = 𝐴) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
13 fourierdlem32.ss . . . . . 6 (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))
1413adantr 479 . . . . 5 ((𝜑𝐶 = 𝐴) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))
15 ioosscn 13435 . . . . . 6 (𝐴(,)𝐵) ⊆ ℂ
1615a1i 11 . . . . 5 ((𝜑𝐶 = 𝐴) → (𝐴(,)𝐵) ⊆ ℂ)
17 eqid 2725 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
18 eqid 2725 . . . . 5 ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴})) = ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴}))
19 fourierdlem32.c . . . . . . . . 9 (𝜑𝐶 ∈ ℝ)
2019leidd 11826 . . . . . . . . 9 (𝜑𝐶𝐶)
21 fourierdlem32.cltd . . . . . . . . 9 (𝜑𝐶 < 𝐷)
22 fourierdlem32.d . . . . . . . . . . 11 (𝜑𝐷 ∈ ℝ)
2322rexrd 11310 . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ*)
24 elico2 13437 . . . . . . . . . 10 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ*) → (𝐶 ∈ (𝐶[,)𝐷) ↔ (𝐶 ∈ ℝ ∧ 𝐶𝐶𝐶 < 𝐷)))
2519, 23, 24syl2anc 582 . . . . . . . . 9 (𝜑 → (𝐶 ∈ (𝐶[,)𝐷) ↔ (𝐶 ∈ ℝ ∧ 𝐶𝐶𝐶 < 𝐷)))
2619, 20, 21, 25mpbir3and 1339 . . . . . . . 8 (𝜑𝐶 ∈ (𝐶[,)𝐷))
2726adantr 479 . . . . . . 7 ((𝜑𝐶 = 𝐴) → 𝐶 ∈ (𝐶[,)𝐷))
28 fourierdlem32.j . . . . . . . . 9 𝐽 = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵))
2917cnfldtop 24783 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ Top
30 ovex 7456 . . . . . . . . . . 11 (𝐴[,)𝐵) ∈ V
3130a1i 11 . . . . . . . . . 10 ((𝜑𝐶 = 𝐴) → (𝐴[,)𝐵) ∈ V)
32 resttop 23147 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,)𝐵) ∈ V) → ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵)) ∈ Top)
3329, 31, 32sylancr 585 . . . . . . . . 9 ((𝜑𝐶 = 𝐴) → ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵)) ∈ Top)
3428, 33eqeltrid 2829 . . . . . . . 8 ((𝜑𝐶 = 𝐴) → 𝐽 ∈ Top)
35 mnfxr 11317 . . . . . . . . . . . . . . . 16 -∞ ∈ ℝ*
3635a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → -∞ ∈ ℝ*)
3723adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐷 ∈ ℝ*)
38 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 ∈ (𝐴[,)𝐷))
39 fourierdlem32.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
4039adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐴 ∈ ℝ)
41 elico2 13437 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ*) → (𝑥 ∈ (𝐴[,)𝐷) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐷)))
4240, 37, 41syl2anc 582 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → (𝑥 ∈ (𝐴[,)𝐷) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐷)))
4338, 42mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐷))
4443simp1d 1139 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 ∈ ℝ)
4544mnfltd 13153 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → -∞ < 𝑥)
4643simp3d 1141 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 < 𝐷)
4736, 37, 44, 45, 46eliood 45053 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 ∈ (-∞(,)𝐷))
4843simp2d 1140 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐴𝑥)
4922adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐷 ∈ ℝ)
50 fourierdlem32.b . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ)
5150adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐵 ∈ ℝ)
5239, 50, 19, 22, 21, 13fourierdlem10 45675 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝐶𝐷𝐵))
5352simprd 494 . . . . . . . . . . . . . . . . 17 (𝜑𝐷𝐵)
5453adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐷𝐵)
5544, 49, 51, 46, 54ltletrd 11420 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 < 𝐵)
5650rexrd 11310 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
5756adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝐵 ∈ ℝ*)
58 elico2 13437 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐵)))
5940, 57, 58syl2anc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐵)))
6044, 48, 55, 59mpbir3and 1339 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 ∈ (𝐴[,)𝐵))
6147, 60elind 4194 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,)𝐷)) → 𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)))
62 elinel1 4195 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ (-∞(,)𝐷))
63 elioore 13403 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-∞(,)𝐷) → 𝑥 ∈ ℝ)
6462, 63syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ ℝ)
6564adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ ℝ)
66 elinel2 4196 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ (𝐴[,)𝐵))
6766adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐵))
6839adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝐴 ∈ ℝ)
6956adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝐵 ∈ ℝ*)
7068, 69, 58syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐵)))
7167, 70mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐵))
7271simp2d 1140 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝐴𝑥)
7362adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (-∞(,)𝐷))
7423adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝐷 ∈ ℝ*)
75 elioo2 13414 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ*𝐷 ∈ ℝ*) → (𝑥 ∈ (-∞(,)𝐷) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 < 𝐷)))
7635, 74, 75sylancr 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → (𝑥 ∈ (-∞(,)𝐷) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 < 𝐷)))
7773, 76mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → (𝑥 ∈ ℝ ∧ -∞ < 𝑥𝑥 < 𝐷))
7877simp3d 1141 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝑥 < 𝐷)
7968, 74, 41syl2anc 582 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → (𝑥 ∈ (𝐴[,)𝐷) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥 < 𝐷)))
8065, 72, 78, 79mpbir3and 1339 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐷))
8161, 80impbida 799 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝐴[,)𝐷) ↔ 𝑥 ∈ ((-∞(,)𝐷) ∩ (𝐴[,)𝐵))))
8281eqrdv 2723 . . . . . . . . . . 11 (𝜑 → (𝐴[,)𝐷) = ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)))
83 retop 24761 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Top
8483a1i 11 . . . . . . . . . . . 12 (𝜑 → (topGen‘ran (,)) ∈ Top)
8530a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐴[,)𝐵) ∈ V)
86 iooretop 24765 . . . . . . . . . . . . 13 (-∞(,)𝐷) ∈ (topGen‘ran (,))
8786a1i 11 . . . . . . . . . . . 12 (𝜑 → (-∞(,)𝐷) ∈ (topGen‘ran (,)))
88 elrestr 17438 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,)𝐵) ∈ V ∧ (-∞(,)𝐷) ∈ (topGen‘ran (,))) → ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)) ∈ ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
8984, 85, 87, 88syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((-∞(,)𝐷) ∩ (𝐴[,)𝐵)) ∈ ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
9082, 89eqeltrd 2825 . . . . . . . . . 10 (𝜑 → (𝐴[,)𝐷) ∈ ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
9190adantr 479 . . . . . . . . 9 ((𝜑𝐶 = 𝐴) → (𝐴[,)𝐷) ∈ ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
92 simpr 483 . . . . . . . . . 10 ((𝜑𝐶 = 𝐴) → 𝐶 = 𝐴)
9392oveq1d 7438 . . . . . . . . 9 ((𝜑𝐶 = 𝐴) → (𝐶[,)𝐷) = (𝐴[,)𝐷))
9428a1i 11 . . . . . . . . . . 11 (𝜑𝐽 = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵)))
9529a1i 11 . . . . . . . . . . . 12 (𝜑 → (TopOpen‘ℂfld) ∈ Top)
96 icossre 13454 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ)
9739, 56, 96syl2anc 582 . . . . . . . . . . . 12 (𝜑 → (𝐴[,)𝐵) ⊆ ℝ)
98 reex 11245 . . . . . . . . . . . . 13 ℝ ∈ V
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
100 restabs 23152 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,)𝐵) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵)))
10195, 97, 99, 100syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵)))
10217tgioo2 24802 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
103102eqcomi 2734 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t ℝ) = (topGen‘ran (,))
104103oveq1i 7433 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,)𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,)𝐵))
105104a1i 11 . . . . . . . . . . 11 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,)𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
10694, 101, 1053eqtr2d 2771 . . . . . . . . . 10 (𝜑𝐽 = ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
107106adantr 479 . . . . . . . . 9 ((𝜑𝐶 = 𝐴) → 𝐽 = ((topGen‘ran (,)) ↾t (𝐴[,)𝐵)))
10891, 93, 1073eltr4d 2840 . . . . . . . 8 ((𝜑𝐶 = 𝐴) → (𝐶[,)𝐷) ∈ 𝐽)
109 isopn3i 23069 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐶[,)𝐷) ∈ 𝐽) → ((int‘𝐽)‘(𝐶[,)𝐷)) = (𝐶[,)𝐷))
11034, 108, 109syl2anc 582 . . . . . . 7 ((𝜑𝐶 = 𝐴) → ((int‘𝐽)‘(𝐶[,)𝐷)) = (𝐶[,)𝐷))
11127, 110eleqtrrd 2828 . . . . . 6 ((𝜑𝐶 = 𝐴) → 𝐶 ∈ ((int‘𝐽)‘(𝐶[,)𝐷)))
112 id 22 . . . . . . . 8 (𝐶 = 𝐴𝐶 = 𝐴)
113112eqcomd 2731 . . . . . . 7 (𝐶 = 𝐴𝐴 = 𝐶)
114113adantl 480 . . . . . 6 ((𝜑𝐶 = 𝐴) → 𝐴 = 𝐶)
115 uncom 4152 . . . . . . . . . . . 12 ((𝐴(,)𝐵) ∪ {𝐴}) = ({𝐴} ∪ (𝐴(,)𝐵))
11639rexrd 11310 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ*)
117 fourierdlem32.altb . . . . . . . . . . . . 13 (𝜑𝐴 < 𝐵)
118 snunioo 13504 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
119116, 56, 117, 118syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
120115, 119eqtrid 2777 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵))
121120adantr 479 . . . . . . . . . 10 ((𝜑𝐶 = 𝐴) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵))
122121oveq2d 7439 . . . . . . . . 9 ((𝜑𝐶 = 𝐴) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴})) = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵)))
123122, 28eqtr4di 2783 . . . . . . . 8 ((𝜑𝐶 = 𝐴) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴})) = 𝐽)
124123fveq2d 6904 . . . . . . 7 ((𝜑𝐶 = 𝐴) → (int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴}))) = (int‘𝐽))
125 uncom 4152 . . . . . . . . 9 ((𝐶(,)𝐷) ∪ {𝐴}) = ({𝐴} ∪ (𝐶(,)𝐷))
126 sneq 4642 . . . . . . . . . . 11 (𝐶 = 𝐴 → {𝐶} = {𝐴})
127126eqcomd 2731 . . . . . . . . . 10 (𝐶 = 𝐴 → {𝐴} = {𝐶})
128127uneq1d 4161 . . . . . . . . 9 (𝐶 = 𝐴 → ({𝐴} ∪ (𝐶(,)𝐷)) = ({𝐶} ∪ (𝐶(,)𝐷)))
129125, 128eqtrid 2777 . . . . . . . 8 (𝐶 = 𝐴 → ((𝐶(,)𝐷) ∪ {𝐴}) = ({𝐶} ∪ (𝐶(,)𝐷)))
13019rexrd 11310 . . . . . . . . 9 (𝜑𝐶 ∈ ℝ*)
131 snunioo 13504 . . . . . . . . 9 ((𝐶 ∈ ℝ*𝐷 ∈ ℝ*𝐶 < 𝐷) → ({𝐶} ∪ (𝐶(,)𝐷)) = (𝐶[,)𝐷))
132130, 23, 21, 131syl3anc 1368 . . . . . . . 8 (𝜑 → ({𝐶} ∪ (𝐶(,)𝐷)) = (𝐶[,)𝐷))
133129, 132sylan9eqr 2787 . . . . . . 7 ((𝜑𝐶 = 𝐴) → ((𝐶(,)𝐷) ∪ {𝐴}) = (𝐶[,)𝐷))
134124, 133fveq12d 6907 . . . . . 6 ((𝜑𝐶 = 𝐴) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴})))‘((𝐶(,)𝐷) ∪ {𝐴})) = ((int‘𝐽)‘(𝐶[,)𝐷)))
135111, 114, 1343eltr4d 2840 . . . . 5 ((𝜑𝐶 = 𝐴) → 𝐴 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐴})))‘((𝐶(,)𝐷) ∪ {𝐴})))
13612, 14, 16, 17, 18, 135limcres 25898 . . . 4 ((𝜑𝐶 = 𝐴) → ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐴) = (𝐹 lim 𝐴))
1378, 136eqtr2d 2766 . . 3 ((𝜑𝐶 = 𝐴) → (𝐹 lim 𝐴) = ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶))
1382, 6, 1373eltr3d 2839 . 2 ((𝜑𝐶 = 𝐴) → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶))
139 limcresi 25897 . . 3 (𝐹 lim 𝐶) ⊆ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶)
140 iffalse 4541 . . . . . 6 𝐶 = 𝐴 → if(𝐶 = 𝐴, 𝑅, (𝐹𝐶)) = (𝐹𝐶))
1413, 140eqtrid 2777 . . . . 5 𝐶 = 𝐴𝑌 = (𝐹𝐶))
142141adantl 480 . . . 4 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝑌 = (𝐹𝐶))
143 ssid 4001 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
144143a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
145 eqid 2725 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
146 unicntop 24785 . . . . . . . . . . . . . . . 16 ℂ = (TopOpen‘ℂfld)
147146restid 17443 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
14829, 147ax-mp 5 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
149148eqcomi 2734 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
15017, 145, 149cncfcn 24913 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
15115, 144, 150sylancr 585 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
1529, 151eleqtrd 2827 . . . . . . . . . 10 (𝜑𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
15317cnfldtopon 24782 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
154 resttopon 23148 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
155153, 15, 154mp2an 690 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))
156 cncnp 23267 . . . . . . . . . . 11 ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥))))
157155, 153, 156mp2an 690 . . . . . . . . . 10 (𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥)))
158152, 157sylib 217 . . . . . . . . 9 (𝜑 → (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥)))
159158simprd 494 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥))
160159adantr 479 . . . . . . 7 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥))
161116adantr 479 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐴 ∈ ℝ*)
16256adantr 479 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐵 ∈ ℝ*)
16319adantr 479 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐶 ∈ ℝ)
16439adantr 479 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐴 ∈ ℝ)
16552simpld 493 . . . . . . . . . 10 (𝜑𝐴𝐶)
166165adantr 479 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐴𝐶)
167112eqcoms 2733 . . . . . . . . . . . 12 (𝐴 = 𝐶𝐶 = 𝐴)
168167necon3bi 2956 . . . . . . . . . . 11 𝐶 = 𝐴𝐴𝐶)
169168adantl 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐴𝐶)
170169necomd 2985 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐶𝐴)
171164, 163, 166, 170leneltd 11414 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐴 < 𝐶)
17219, 22, 50, 21, 53ltletrd 11420 . . . . . . . . 9 (𝜑𝐶 < 𝐵)
173172adantr 479 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐶 < 𝐵)
174161, 162, 163, 171, 173eliood 45053 . . . . . . 7 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐶 ∈ (𝐴(,)𝐵))
175 fveq2 6900 . . . . . . . . 9 (𝑥 = 𝐶 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝐶))
176175eleq2d 2811 . . . . . . . 8 (𝑥 = 𝐶 → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥) ↔ 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝐶)))
177176rspccva 3606 . . . . . . 7 ((∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑥) ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝐶))
178160, 174, 177syl2anc 582 . . . . . 6 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝐶))
17917, 145cnplimc 25899 . . . . . . 7 (((𝐴(,)𝐵) ⊆ ℂ ∧ 𝐶 ∈ (𝐴(,)𝐵)) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝐶) ↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐹𝐶) ∈ (𝐹 lim 𝐶))))
18015, 174, 179sylancr 585 . . . . . 6 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝐶) ↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐹𝐶) ∈ (𝐹 lim 𝐶))))
181178, 180mpbid 231 . . . . 5 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐹𝐶) ∈ (𝐹 lim 𝐶)))
182181simprd 494 . . . 4 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → (𝐹𝐶) ∈ (𝐹 lim 𝐶))
183142, 182eqeltrd 2825 . . 3 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝑌 ∈ (𝐹 lim 𝐶))
184139, 183sselid 3976 . 2 ((𝜑 ∧ ¬ 𝐶 = 𝐴) → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶))
185138, 184pm2.61dan 811 1 (𝜑𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wne 2929  wral 3050  Vcvv 3461  cun 3944  cin 3945  wss 3946  ifcif 4532  {csn 4632   class class class wbr 5152  ran crn 5682  cres 5683  wf 6549  cfv 6553  (class class class)co 7423  cc 11152  cr 11153  -∞cmnf 11292  *cxr 11293   < clt 11294  cle 11295  (,)cioo 13373  [,)cico 13375  t crest 17430  TopOpenctopn 17431  topGenctg 17447  fldccnfld 21335  Topctop 22878  TopOnctopon 22895  intcnt 23004   Cn ccn 23211   CnP ccnp 23212  cnccncf 24879   lim climc 25874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-1st 8002  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-er 8733  df-map 8856  df-pm 8857  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fi 9450  df-sup 9481  df-inf 9482  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12520  df-z 12606  df-dec 12725  df-uz 12870  df-q 12980  df-rp 13024  df-xneg 13141  df-xadd 13142  df-xmul 13143  df-ioo 13377  df-ico 13379  df-icc 13380  df-fz 13534  df-seq 14017  df-exp 14077  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-struct 17144  df-slot 17179  df-ndx 17191  df-base 17209  df-plusg 17274  df-mulr 17275  df-starv 17276  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-rest 17432  df-topn 17433  df-topgen 17453  df-psmet 21327  df-xmet 21328  df-met 21329  df-bl 21330  df-mopn 21331  df-cnfld 21336  df-top 22879  df-topon 22896  df-topsp 22918  df-bases 22932  df-ntr 23007  df-cn 23214  df-cnp 23215  df-xms 24309  df-ms 24310  df-cncf 24881  df-limc 25878
This theorem is referenced by:  fourierdlem48  45712  fourierdlem76  45740  fourierdlem89  45753
  Copyright terms: Public domain W3C validator