| Step | Hyp | Ref
| Expression |
| 1 | | pire 26500 |
. . . . 5
⊢ π
∈ ℝ |
| 2 | 1 | renegcli 11570 |
. . . 4
⊢ -π
∈ ℝ |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → -π ∈
ℝ) |
| 4 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → π ∈
ℝ) |
| 5 | | negpilt0 45292 |
. . . . 5
⊢ -π
< 0 |
| 6 | | pipos 26502 |
. . . . 5
⊢ 0 <
π |
| 7 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 8 | 2, 7, 1 | lttri 11387 |
. . . . 5
⊢ ((-π
< 0 ∧ 0 < π) → -π < π) |
| 9 | 5, 6, 8 | mp2an 692 |
. . . 4
⊢ -π
< π |
| 10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → -π <
π) |
| 11 | | fourierdlem94.p |
. . 3
⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 12 | | picn 26501 |
. . . . 5
⊢ π
∈ ℂ |
| 13 | 12 | 2timesi 12404 |
. . . 4
⊢ (2
· π) = (π + π) |
| 14 | | fourierdlem94.t |
. . . 4
⊢ 𝑇 = (2 ·
π) |
| 15 | 12, 12 | subnegi 11588 |
. . . 4
⊢ (π
− -π) = (π + π) |
| 16 | 13, 14, 15 | 3eqtr4i 2775 |
. . 3
⊢ 𝑇 = (π −
-π) |
| 17 | | fourierdlem94.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 18 | | fourierdlem94.q |
. . 3
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
| 19 | | ssid 4006 |
. . . 4
⊢ ℝ
⊆ ℝ |
| 20 | 19 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ⊆
ℝ) |
| 21 | | fourierdlem94.f |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 22 | | simp2 1138 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℝ) |
| 23 | | zre 12617 |
. . . . . 6
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
| 24 | 23 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ) |
| 25 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 26 | 25, 1 | remulcli 11277 |
. . . . . . . . 9
⊢ (2
· π) ∈ ℝ |
| 27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (2 · π) ∈
ℝ) |
| 28 | 14, 27 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ) |
| 30 | 29 | 3adant2 1132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ) |
| 31 | 24, 30 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ) |
| 32 | 22, 31 | readdcld 11290 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ) |
| 33 | | simp1 1137 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → 𝜑) |
| 34 | | simp3 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ) |
| 35 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 36 | 35 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 37 | 21, 36 | fssd 6753 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
| 38 | 37 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ) |
| 39 | 38 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶ℂ) |
| 40 | 29 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) |
| 41 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℤ) |
| 42 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
| 43 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ)) |
| 44 | 43 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑦 ∈ ℝ))) |
| 45 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇)) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇))) |
| 47 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 48 | 46, 47 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))) |
| 49 | 44, 48 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))) |
| 50 | | fourierdlem94.per |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
| 51 | 49, 50 | chvarvv 1998 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) |
| 52 | 51 | ad4ant14 752 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) |
| 53 | 39, 40, 41, 42, 52 | fperiodmul 45316 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) |
| 54 | 33, 34, 22, 53 | syl21anc 838 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) |
| 55 | 35 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆
ℂ) |
| 56 | | ioossre 13448 |
. . . . . . . 8
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ |
| 57 | 56 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) |
| 58 | 21, 57 | fssresd 6775 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ) |
| 59 | 58, 36 | fssd 6753 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
| 60 | 59 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
| 61 | 56 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) |
| 62 | 37 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ) |
| 63 | 19 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆
ℝ) |
| 64 | | eqid 2737 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 65 | | tgioo4 24826 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 66 | 64, 65 | dvres 25946 |
. . . . . . 7
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D
(𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))) |
| 67 | 55, 62, 63, 61, 66 | syl22anc 839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))) |
| 68 | 67 | dmeqd 5916 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))) |
| 69 | | ioontr 45524 |
. . . . . . . 8
⊢
((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) |
| 70 | 69 | reseq2i 5994 |
. . . . . . 7
⊢ ((ℝ
D 𝐹) ↾
((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 71 | 70 | dmeqi 5915 |
. . . . . 6
⊢ dom
((ℝ D 𝐹) ↾
((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 72 | 71 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
| 73 | | fourierdlem94.dvcn |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
| 74 | | cncff 24919 |
. . . . . 6
⊢
(((ℝ D 𝐹)
↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
| 75 | | fdm 6745 |
. . . . . 6
⊢
(((ℝ D 𝐹)
↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom ((ℝ D
𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 76 | 73, 74, 75 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 77 | 68, 72, 76 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 78 | | dvcn 25957 |
. . . 4
⊢
(((ℝ ⊆ ℂ ∧ (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) ∧ dom (ℝ D
(𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
| 79 | 55, 60, 61, 77, 78 | syl31anc 1375 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
| 80 | 61, 35 | sstrdi 3996 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ) |
| 81 | 11 | fourierdlem2 46124 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
| 82 | 17, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
| 83 | 18, 82 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
| 84 | 83 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
| 85 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) |
| 86 | 84, 85 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
| 87 | 86 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
| 88 | | elfzofz 13715 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
| 89 | 88 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
| 90 | 87, 89 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
| 91 | 90 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈
ℝ*) |
| 92 | | fzofzp1 13803 |
. . . . . . 7
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
| 93 | 92 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
| 94 | 87, 93 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
| 95 | 83 | simprrd 774 |
. . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
| 96 | 95 | r19.21bi 3251 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
| 97 | 64, 91, 94, 96 | lptioo2cn 45660 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈
((limPt‘(TopOpen‘ℂfld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
| 98 | 58 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ) |
| 99 | 36, 37, 20 | dvbss 25936 |
. . . . . . . 8
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆
ℝ) |
| 100 | | dvfre 25989 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶ℝ ∧
ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 101 | 21, 20, 100 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 102 | 83 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
| 103 | 102 | simplld 768 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) = -π) |
| 104 | 102 | simplrd 770 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘𝑀) = π) |
| 105 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
| 106 | 94 | rexrd 11311 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈
ℝ*) |
| 107 | 64, 106, 90, 96 | lptioo1cn 45661 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈
((limPt‘(TopOpen‘ℂfld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
| 108 | | fourierdlem94.dvlb |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) |
| 109 | 105, 80, 107, 108, 64 | ellimciota 45629 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
| 110 | | fourierdlem94.dvub |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) |
| 111 | 105, 80, 97, 110, 64 | ellimciota 45629 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
| 112 | 23 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ) |
| 113 | 112, 29 | remulcld 11291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ) |
| 114 | 38 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℂ) |
| 115 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℝ) |
| 116 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑘 ∈ ℤ) |
| 117 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ) |
| 118 | 50 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
| 119 | 114, 115,
116, 117, 118 | fperiodmul 45316 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡)) |
| 120 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (ℝ
D 𝐹) = (ℝ D 𝐹) |
| 121 | 38, 113, 119, 120 | fperdvper 45934 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡))) |
| 122 | 121 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡))) |
| 123 | 122 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹)) |
| 124 | 122 | simprd 495 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)) |
| 125 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖)) |
| 126 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1)) |
| 127 | 126 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) |
| 128 | 125, 127 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 129 | 128 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑀) ↦ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 130 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π
− 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) |
| 131 | 99, 101, 3, 4, 10, 16, 17, 86, 103, 104, 73, 109, 111, 123, 124, 129, 130 | fourierdlem71 46192 |
. . . . . . 7
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) |
| 132 | 131 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) |
| 133 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀)) |
| 134 | | nfra1 3284 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 |
| 135 | 133, 134 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) |
| 136 | 67, 70 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
| 137 | 136 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡)) |
| 138 | | fvres 6925 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
| 139 | 137, 138 | sylan9eq 2797 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
| 140 | 139 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡))) |
| 141 | 140 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡))) |
| 142 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) |
| 143 | | ssdmres 6031 |
. . . . . . . . . . . . . . 15
⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 144 | 76, 143 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹)) |
| 145 | 144 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹)) |
| 146 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 147 | 145, 146 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹)) |
| 148 | | rspa 3248 |
. . . . . . . . . . . 12
⊢
((∀𝑡 ∈
dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) |
| 149 | 142, 147,
148 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) |
| 150 | 141, 149 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧) |
| 151 | 150 | ex 412 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)) |
| 152 | 135, 151 | ralrimi 3257 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧) |
| 153 | 152 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)) |
| 154 | 153 | reximdv 3170 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)) |
| 155 | 132, 154 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧) |
| 156 | 90, 94, 98, 77, 155 | ioodvbdlimc2 45950 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) |
| 157 | 60, 80, 97, 156, 64 | ellimciota 45629 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
| 158 | | fourierdlem94.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 159 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥)) |
| 160 | 159 | oveq1d 7446 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇)) |
| 161 | 160 | fveq2d 6910 |
. . . . 5
⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇))) |
| 162 | 161 | oveq1d 7446 |
. . . 4
⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)) |
| 163 | 162 | cbvmptv 5255 |
. . 3
⊢ (𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦
((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)) |
| 164 | | id 22 |
. . . . 5
⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥) |
| 165 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)) |
| 166 | 164, 165 | oveq12d 7449 |
. . . 4
⊢ (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))) |
| 167 | 166 | cbvmptv 5255 |
. . 3
⊢ (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))) |
| 168 | 3, 4, 10, 11, 16, 17, 18, 20, 21, 32, 54, 79, 157, 158, 163, 167 | fourierdlem49 46170 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅) |
| 169 | 90, 94, 98, 77, 155 | ioodvbdlimc1 45948 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) |
| 170 | 60, 80, 107, 169, 64 | ellimciota 45629 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
| 171 | | biid 261 |
. . 3
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))) ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇)))) |
| 172 | 3, 4, 10, 11, 16, 17, 18, 21, 32, 54, 79, 170, 158, 163, 167, 171 | fourierdlem48 46169 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅) |
| 173 | 168, 172 | jca 511 |
1
⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠
∅)) |