| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem33.5 | . . . 4
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐿 ∈ (𝐹 limℂ 𝐵)) | 
| 3 |  | fourierdlem33.y | . . . . 5
⊢ 𝑌 = if(𝐷 = 𝐵, 𝐿, (𝐹‘𝐷)) | 
| 4 |  | iftrue 4531 | . . . . 5
⊢ (𝐷 = 𝐵 → if(𝐷 = 𝐵, 𝐿, (𝐹‘𝐷)) = 𝐿) | 
| 5 | 3, 4 | eqtr2id 2790 | . . . 4
⊢ (𝐷 = 𝐵 → 𝐿 = 𝑌) | 
| 6 | 5 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐿 = 𝑌) | 
| 7 |  | oveq2 7439 | . . . . 5
⊢ (𝐷 = 𝐵 → ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷) = ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐵)) | 
| 8 | 7 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷) = ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐵)) | 
| 9 |  | fourierdlem33.4 | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 10 |  | cncff 24919 | . . . . . . 7
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) | 
| 11 | 9, 10 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) | 
| 12 | 11 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐹:(𝐴(,)𝐵)⟶ℂ) | 
| 13 |  | fourierdlem33.ss | . . . . . 6
⊢ (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | 
| 14 | 13 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | 
| 15 |  | ioosscn 13449 | . . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ | 
| 16 | 15 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐴(,)𝐵) ⊆ ℂ) | 
| 17 |  | eqid 2737 | . . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 18 |  | fourierdlem33.10 | . . . . 5
⊢ 𝐽 =
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) | 
| 19 |  | fourierdlem33.7 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 20 |  | fourierdlem33.8 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 < 𝐷) | 
| 21 | 19 | leidd 11829 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ≤ 𝐷) | 
| 22 |  | fourierdlem33.6 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 23 | 22 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ*) | 
| 24 |  | elioc2 13450 | . . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈ ℝ)
→ (𝐷 ∈ (𝐶(,]𝐷) ↔ (𝐷 ∈ ℝ ∧ 𝐶 < 𝐷 ∧ 𝐷 ≤ 𝐷))) | 
| 25 | 23, 19, 24 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 ∈ (𝐶(,]𝐷) ↔ (𝐷 ∈ ℝ ∧ 𝐶 < 𝐷 ∧ 𝐷 ≤ 𝐷))) | 
| 26 | 19, 20, 21, 25 | mpbir3and 1343 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (𝐶(,]𝐷)) | 
| 27 | 26 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐷 ∈ (𝐶(,]𝐷)) | 
| 28 |  | eqcom 2744 | . . . . . . . . 9
⊢ (𝐷 = 𝐵 ↔ 𝐵 = 𝐷) | 
| 29 | 28 | biimpi 216 | . . . . . . . 8
⊢ (𝐷 = 𝐵 → 𝐵 = 𝐷) | 
| 30 | 29 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐵 = 𝐷) | 
| 31 | 17 | cnfldtop 24804 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 32 |  | fourierdlem33.1 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 33 | 32 | rexrd 11311 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 34 |  | fourierdlem33.2 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 35 | 34 | rexrd 11311 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 36 |  | fourierdlem33.3 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 37 |  | ioounsn 13517 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) | 
| 38 | 33, 35, 36, 37 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) | 
| 39 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢ (𝐴(,]𝐵) ∈ V | 
| 40 | 39 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,]𝐵) ∈ V) | 
| 41 | 38, 40 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V) | 
| 42 |  | resttop 23168 | . . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top) | 
| 43 | 31, 41, 42 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top) | 
| 44 | 18, 43 | eqeltrid 2845 | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 45 | 44 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐽 ∈ Top) | 
| 46 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝐷 = 𝐵 → (𝐶(,]𝐷) = (𝐶(,]𝐵)) | 
| 47 | 46 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐶(,]𝐷) = (𝐶(,]𝐵)) | 
| 48 | 23 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 ∈
ℝ*) | 
| 49 |  | pnfxr 11315 | . . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* | 
| 50 | 49 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → +∞ ∈
ℝ*) | 
| 51 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐶(,]𝐵)) | 
| 52 | 34 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐵 ∈ ℝ) | 
| 53 |  | elioc2 13450 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝑥 ∈ (𝐶(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 54 | 48, 52, 53 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → (𝑥 ∈ (𝐶(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 55 | 51, 54 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵)) | 
| 56 | 55 | simp1d 1143 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ℝ) | 
| 57 | 55 | simp2d 1144 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 < 𝑥) | 
| 58 | 56 | ltpnfd 13163 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 < +∞) | 
| 59 | 48, 50, 56, 57, 58 | eliood 45511 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐶(,)+∞)) | 
| 60 | 32 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ∈ ℝ) | 
| 61 | 22 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 ∈ ℝ) | 
| 62 | 32, 34, 22, 19, 20, 13 | fourierdlem10 46132 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) | 
| 63 | 62 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ≤ 𝐶) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ≤ 𝐶) | 
| 65 | 60, 61, 56, 64, 57 | lelttrd 11419 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 < 𝑥) | 
| 66 | 55 | simp3d 1145 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ≤ 𝐵) | 
| 67 | 33 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ∈
ℝ*) | 
| 68 |  | elioc2 13450 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 69 | 67, 52, 68 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 70 | 56, 65, 66, 69 | mpbir3and 1343 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐴(,]𝐵)) | 
| 71 | 59, 70 | elind 4200 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) | 
| 72 |  | elinel1 4201 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ (𝐶(,)+∞)) | 
| 73 |  | elioore 13417 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐶(,)+∞) → 𝑥 ∈ ℝ) | 
| 74 | 72, 73 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ ℝ) | 
| 76 | 23 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐶 ∈
ℝ*) | 
| 77 | 49 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → +∞ ∈
ℝ*) | 
| 78 | 72 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐶(,)+∞)) | 
| 79 |  | ioogtlb 45508 | . . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ (𝐶(,)+∞)) → 𝐶 < 𝑥) | 
| 80 | 76, 77, 78, 79 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐶 < 𝑥) | 
| 81 |  | elinel2 4202 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ (𝐴(,]𝐵)) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐴(,]𝐵)) | 
| 83 | 33 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐴 ∈
ℝ*) | 
| 84 | 34 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐵 ∈ ℝ) | 
| 85 | 83, 84, 68 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 86 | 82, 85 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) | 
| 87 | 86 | simp3d 1145 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ≤ 𝐵) | 
| 88 | 76, 84, 53 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → (𝑥 ∈ (𝐶(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐶 < 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 89 | 75, 80, 87, 88 | mpbir3and 1343 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐶(,]𝐵)) | 
| 90 | 71, 89 | impbida 801 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝐶(,]𝐵) ↔ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)))) | 
| 91 | 90 | eqrdv 2735 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶(,]𝐵) = ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) | 
| 92 |  | retop 24782 | . . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top | 
| 93 | 92 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) | 
| 94 |  | iooretop 24786 | . . . . . . . . . . . . . 14
⊢ (𝐶(,)+∞) ∈
(topGen‘ran (,)) | 
| 95 | 94 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶(,)+∞) ∈ (topGen‘ran
(,))) | 
| 96 |  | elrestr 17473 | . . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴(,]𝐵) ∈ V ∧ (𝐶(,)+∞) ∈ (topGen‘ran (,)))
→ ((𝐶(,)+∞)
∩ (𝐴(,]𝐵)) ∈ ((topGen‘ran
(,)) ↾t (𝐴(,]𝐵))) | 
| 97 | 93, 40, 95, 96 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ∈ ((topGen‘ran (,))
↾t (𝐴(,]𝐵))) | 
| 98 | 91, 97 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶(,]𝐵) ∈ ((topGen‘ran (,))
↾t (𝐴(,]𝐵))) | 
| 99 | 98 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐶(,]𝐵) ∈ ((topGen‘ran (,))
↾t (𝐴(,]𝐵))) | 
| 100 | 47, 99 | eqeltrd 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐶(,]𝐷) ∈ ((topGen‘ran (,))
↾t (𝐴(,]𝐵))) | 
| 101 | 18 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 = ((TopOpen‘ℂfld)
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) | 
| 102 | 38 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t (𝐴(,]𝐵))) | 
| 103 | 31 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) | 
| 104 |  | iocssre 13467 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) | 
| 105 | 33, 34, 104 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ) | 
| 106 |  | reex 11246 | . . . . . . . . . . . . . 14
⊢ ℝ
∈ V | 
| 107 | 106 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) | 
| 108 |  | restabs 23173 | . . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,]𝐵) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴(,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,]𝐵))) | 
| 109 | 103, 105,
107, 108 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴(,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,]𝐵))) | 
| 110 |  | tgioo4 24826 | . . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 111 | 110 | eqcomi 2746 | . . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
(topGen‘ran (,)) | 
| 112 | 111 | oveq1i 7441 | . . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴(,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴(,]𝐵)) | 
| 113 | 109, 112 | eqtr3di 2792 | . . . . . . . . . . 11
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴(,]𝐵))) | 
| 114 | 101, 102,
113 | 3eqtrrd 2782 | . . . . . . . . . 10
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴(,]𝐵)) = 𝐽) | 
| 115 | 114 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((topGen‘ran (,))
↾t (𝐴(,]𝐵)) = 𝐽) | 
| 116 | 100, 115 | eleqtrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐶(,]𝐷) ∈ 𝐽) | 
| 117 |  | isopn3i 23090 | . . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐶(,]𝐷) ∈ 𝐽) → ((int‘𝐽)‘(𝐶(,]𝐷)) = (𝐶(,]𝐷)) | 
| 118 | 45, 116, 117 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((int‘𝐽)‘(𝐶(,]𝐷)) = (𝐶(,]𝐷)) | 
| 119 | 27, 30, 118 | 3eltr4d 2856 | . . . . . 6
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐵 ∈ ((int‘𝐽)‘(𝐶(,]𝐷))) | 
| 120 |  | sneq 4636 | . . . . . . . . . . 11
⊢ (𝐷 = 𝐵 → {𝐷} = {𝐵}) | 
| 121 | 120 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝐷 = 𝐵 → {𝐵} = {𝐷}) | 
| 122 | 121 | uneq2d 4168 | . . . . . . . . 9
⊢ (𝐷 = 𝐵 → ((𝐶(,)𝐷) ∪ {𝐵}) = ((𝐶(,)𝐷) ∪ {𝐷})) | 
| 123 | 122 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((𝐶(,)𝐷) ∪ {𝐵}) = ((𝐶(,)𝐷) ∪ {𝐷})) | 
| 124 | 19 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈
ℝ*) | 
| 125 |  | ioounsn 13517 | . . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝐶
< 𝐷) → ((𝐶(,)𝐷) ∪ {𝐷}) = (𝐶(,]𝐷)) | 
| 126 | 23, 124, 20, 125 | syl3anc 1373 | . . . . . . . . 9
⊢ (𝜑 → ((𝐶(,)𝐷) ∪ {𝐷}) = (𝐶(,]𝐷)) | 
| 127 | 126 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((𝐶(,)𝐷) ∪ {𝐷}) = (𝐶(,]𝐷)) | 
| 128 | 123, 127 | eqtr2d 2778 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐶(,]𝐷) = ((𝐶(,)𝐷) ∪ {𝐵})) | 
| 129 | 128 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((int‘𝐽)‘(𝐶(,]𝐷)) = ((int‘𝐽)‘((𝐶(,)𝐷) ∪ {𝐵}))) | 
| 130 | 119, 129 | eleqtrd 2843 | . . . . 5
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝐵 ∈ ((int‘𝐽)‘((𝐶(,)𝐷) ∪ {𝐵}))) | 
| 131 | 12, 14, 16, 17, 18, 130 | limcres 25921 | . . . 4
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐵) = (𝐹 limℂ 𝐵)) | 
| 132 | 8, 131 | eqtr2d 2778 | . . 3
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → (𝐹 limℂ 𝐵) = ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷)) | 
| 133 | 2, 6, 132 | 3eltr3d 2855 | . 2
⊢ ((𝜑 ∧ 𝐷 = 𝐵) → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷)) | 
| 134 |  | limcresi 25920 | . . 3
⊢ (𝐹 limℂ 𝐷) ⊆ ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷) | 
| 135 |  | iffalse 4534 | . . . . . 6
⊢ (¬
𝐷 = 𝐵 → if(𝐷 = 𝐵, 𝐿, (𝐹‘𝐷)) = (𝐹‘𝐷)) | 
| 136 | 3, 135 | eqtrid 2789 | . . . . 5
⊢ (¬
𝐷 = 𝐵 → 𝑌 = (𝐹‘𝐷)) | 
| 137 | 136 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝑌 = (𝐹‘𝐷)) | 
| 138 |  | ssid 4006 | . . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ | 
| 139 | 138 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 140 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) | 
| 141 |  | unicntop 24806 | . . . . . . . . . . . . . . . 16
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 142 | 141 | restid 17478 | . . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) | 
| 143 | 31, 142 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) | 
| 144 | 143 | eqcomi 2746 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 145 | 17, 140, 144 | cncfcn 24936 | . . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 146 | 15, 139, 145 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 147 | 9, 146 | eleqtrd 2843 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 148 | 17 | cnfldtopon 24803 | . . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 149 | 15 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) | 
| 150 |  | resttopon 23169 | . . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) | 
| 151 | 148, 149,
150 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) | 
| 152 | 148 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) | 
| 153 |  | cncnp 23288 | . . . . . . . . . . 11
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥)))) | 
| 154 | 151, 152,
153 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥)))) | 
| 155 | 147, 154 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥))) | 
| 156 | 155 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 157 | 156 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → ∀𝑥 ∈ (𝐴(,)𝐵)𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 158 | 33 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐴 ∈
ℝ*) | 
| 159 | 35 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐵 ∈
ℝ*) | 
| 160 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐷 ∈ ℝ) | 
| 161 | 32, 22, 19, 63, 20 | lelttrd 11419 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 < 𝐷) | 
| 162 | 161 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐴 < 𝐷) | 
| 163 | 34 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐵 ∈ ℝ) | 
| 164 | 62 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ≤ 𝐵) | 
| 165 | 164 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐷 ≤ 𝐵) | 
| 166 |  | neqne 2948 | . . . . . . . . . . 11
⊢ (¬
𝐷 = 𝐵 → 𝐷 ≠ 𝐵) | 
| 167 | 166 | necomd 2996 | . . . . . . . . . 10
⊢ (¬
𝐷 = 𝐵 → 𝐵 ≠ 𝐷) | 
| 168 | 167 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐵 ≠ 𝐷) | 
| 169 | 160, 163,
165, 168 | leneltd 11415 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐷 < 𝐵) | 
| 170 | 158, 159,
160, 162, 169 | eliood 45511 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐷 ∈ (𝐴(,)𝐵)) | 
| 171 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = 𝐷 →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥) = ((((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝐷)) | 
| 172 | 171 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑥 = 𝐷 → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥) ↔ 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝐷))) | 
| 173 | 172 | rspccva 3621 | . . . . . . 7
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑥) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝐷)) | 
| 174 | 157, 170,
173 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝐷)) | 
| 175 | 17, 140 | cnplimc 25922 | . . . . . . 7
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝐷) ↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐹‘𝐷) ∈ (𝐹 limℂ 𝐷)))) | 
| 176 | 15, 170, 175 | sylancr 587 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝐷) ↔ (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐹‘𝐷) ∈ (𝐹 limℂ 𝐷)))) | 
| 177 | 174, 176 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → (𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐹‘𝐷) ∈ (𝐹 limℂ 𝐷))) | 
| 178 | 177 | simprd 495 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → (𝐹‘𝐷) ∈ (𝐹 limℂ 𝐷)) | 
| 179 | 137, 178 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝑌 ∈ (𝐹 limℂ 𝐷)) | 
| 180 | 134, 179 | sselid 3981 | . 2
⊢ ((𝜑 ∧ ¬ 𝐷 = 𝐵) → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷)) | 
| 181 | 133, 180 | pm2.61dan 813 | 1
⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷)) |