Step | Hyp | Ref
| Expression |
1 | | fourierdlem75.xre |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℝ) |
2 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℝ) |
3 | | fourierdlem75.v |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) |
4 | | fourierdlem75.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
5 | | fourierdlem75.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
6 | 5 | fourierdlem2 43333 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))) |
7 | 4, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))) |
8 | 3, 7 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))) |
9 | 8 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ (ℝ ↑m
(0...𝑀))) |
10 | | elmapi 8535 |
. . . . . . . 8
⊢ (𝑉 ∈ (ℝ
↑m (0...𝑀))
→ 𝑉:(0...𝑀)⟶ℝ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ) |
12 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ) |
13 | | fzofzp1 13344 |
. . . . . . 7
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
14 | 13 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
15 | 12, 14 | ffvelrnd 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
16 | 15 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
17 | | eqcom 2744 |
. . . . . . 7
⊢ ((𝑉‘𝑖) = 𝑋 ↔ 𝑋 = (𝑉‘𝑖)) |
18 | 17 | biimpi 219 |
. . . . . 6
⊢ ((𝑉‘𝑖) = 𝑋 → 𝑋 = (𝑉‘𝑖)) |
19 | 18 | adantl 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 = (𝑉‘𝑖)) |
20 | 8 | simprrd 774 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
21 | 20 | r19.21bi 3130 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
22 | 21 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
23 | 19, 22 | eqbrtrd 5080 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1))) |
24 | | fourierdlem75.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
25 | 24 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ) |
26 | | ioossre 13001 |
. . . . . . 7
⊢ (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ |
27 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ) |
28 | 25, 27 | fssresd 6591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℝ) |
29 | 28 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℝ) |
30 | | limcresi 24787 |
. . . . . . . 8
⊢ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ⊆ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋) |
31 | | fourierdlem75.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
32 | 30, 31 | sseldi 3904 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
33 | 32 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
34 | | pnfxr 10892 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
35 | 34 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → +∞ ∈
ℝ*) |
36 | 15 | rexrd 10888 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈
ℝ*) |
37 | 15 | ltpnfd 12718 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) < +∞) |
38 | 36, 35, 37 | xrltled 12745 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ≤ +∞) |
39 | | iooss2 12976 |
. . . . . . . . 9
⊢
((+∞ ∈ ℝ* ∧ (𝑉‘(𝑖 + 1)) ≤ +∞) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ (𝑋(,)+∞)) |
40 | 35, 38, 39 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ (𝑋(,)+∞)) |
41 | 40 | resabs1d 5887 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
42 | 41 | oveq1d 7233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
43 | 33, 42 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
44 | 43 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
45 | | eqid 2737 |
. . . 4
⊢ (ℝ
D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
46 | | ax-resscn 10791 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
48 | 24, 47 | fssd 6568 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
49 | | ssid 3928 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ |
50 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℝ) |
51 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ) |
52 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
53 | 52 | tgioo2 23705 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
54 | 52, 53 | dvres 24813 |
. . . . . . . . . 10
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D
(𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑋(,)(𝑉‘(𝑖 + 1)))))) |
55 | 47, 48, 50, 51, 54 | syl22anc 839 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑋(,)(𝑉‘(𝑖 + 1)))))) |
56 | | fourierdlem75.g |
. . . . . . . . . . 11
⊢ 𝐺 = (ℝ D 𝐹) |
57 | 56 | eqcomi 2746 |
. . . . . . . . . 10
⊢ (ℝ
D 𝐹) = 𝐺 |
58 | | ioontr 42732 |
. . . . . . . . . 10
⊢
((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1))) |
59 | 57, 58 | reseq12i 5854 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹) ↾
((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) |
60 | 55, 59 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
61 | 60 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑉‘𝑖) = 𝑋) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
62 | 61 | dmeqd 5779 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
63 | 62 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
64 | | fourierdlem75.gcn |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ) |
65 | 64 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ) |
66 | | oveq1 7225 |
. . . . . . . . . . 11
⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = (𝑋(,)(𝑉‘(𝑖 + 1)))) |
67 | 66 | reseq2d 5856 |
. . . . . . . . . 10
⊢ ((𝑉‘𝑖) = 𝑋 → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
68 | 67 | feq1d 6535 |
. . . . . . . . 9
⊢ ((𝑉‘𝑖) = 𝑋 → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)) |
69 | 68 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)) |
70 | 65, 69 | mpbid 235 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ) |
71 | 66 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = (𝑋(,)(𝑉‘(𝑖 + 1)))) |
72 | 71 | feq2d 6536 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ)) |
73 | 70, 72 | mpbid 235 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ) |
74 | | fdm 6559 |
. . . . . 6
⊢ ((𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ → dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1)))) |
75 | 73, 74 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1)))) |
76 | 63, 75 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝑋(,)(𝑉‘(𝑖 + 1)))) |
77 | | limcresi 24787 |
. . . . . . . 8
⊢ ((𝐺 ↾ (𝑋(,)+∞)) limℂ 𝑋) ⊆ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋) |
78 | | fourierdlem75.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
79 | 77, 78 | sseldi 3904 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
80 | 79 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋)) |
81 | 40 | resabs1d 5887 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
82 | 60 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) |
83 | 81, 82 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))) |
84 | 83 | oveq1d 7233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) limℂ 𝑋) = ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) limℂ 𝑋)) |
85 | 80, 84 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) limℂ 𝑋)) |
86 | 85 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) limℂ 𝑋)) |
87 | | eqid 2737 |
. . . 4
⊢ (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) |
88 | | oveq2 7226 |
. . . . . . 7
⊢ (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠)) |
89 | 88 | fveq2d 6726 |
. . . . . 6
⊢ (𝑥 = 𝑠 → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) |
90 | 89 | oveq1d 7233 |
. . . . 5
⊢ (𝑥 = 𝑠 → (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) − 𝑌) = (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌)) |
91 | 90 | cbvmptv 5163 |
. . . 4
⊢ (𝑥 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) − 𝑌)) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌)) |
92 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝑠 → 𝑥 = 𝑠) |
93 | 92 | cbvmptv 5163 |
. . . 4
⊢ (𝑥 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ 𝑥) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ 𝑠) |
94 | 2, 16, 23, 29, 44, 45, 76, 86, 87, 91, 93 | fourierdlem61 43391 |
. . 3
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) limℂ 0)) |
95 | | fourierdlem75.a |
. . . . 5
⊢ 𝐴 = if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) |
96 | | iftrue 4450 |
. . . . 5
⊢ ((𝑉‘𝑖) = 𝑋 → if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) = 𝐸) |
97 | 95, 96 | syl5eq 2790 |
. . . 4
⊢ ((𝑉‘𝑖) = 𝑋 → 𝐴 = 𝐸) |
98 | 97 | adantl 485 |
. . 3
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐴 = 𝐸) |
99 | | fourierdlem75.h |
. . . . . . 7
⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
100 | 99 | reseq1i 5852 |
. . . . . 6
⊢ (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
101 | 100 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
102 | | ioossicc 13026 |
. . . . . . . 8
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) |
103 | | pire 25353 |
. . . . . . . . . . . 12
⊢ π
∈ ℝ |
104 | 103 | renegcli 11144 |
. . . . . . . . . . 11
⊢ -π
∈ ℝ |
105 | 104 | rexri 10896 |
. . . . . . . . . 10
⊢ -π
∈ ℝ* |
106 | 105 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈
ℝ*) |
107 | 103 | rexri 10896 |
. . . . . . . . . 10
⊢ π
∈ ℝ* |
108 | 107 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈
ℝ*) |
109 | 104 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ∈
ℝ) |
110 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈
ℝ) |
111 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -π ∈
ℝ) |
112 | 111, 1 | readdcld 10867 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (-π + 𝑋) ∈ ℝ) |
113 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → π ∈
ℝ) |
114 | 113, 1 | readdcld 10867 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (π + 𝑋) ∈ ℝ) |
115 | 112, 114 | iccssred 13027 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ) |
116 | 115 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ) |
117 | 5, 4, 3 | fourierdlem15 43346 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋))) |
118 | 117 | ffvelrnda 6909 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋))) |
119 | 116, 118 | sseldd 3907 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ) |
120 | 1 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ) |
121 | 119, 120 | resubcld 11265 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ) |
122 | 111 | recnd 10866 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -π ∈
ℂ) |
123 | 1 | recnd 10866 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ ℂ) |
124 | 122, 123 | pncand 11195 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π) |
125 | 124 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -π = ((-π + 𝑋) − 𝑋)) |
126 | 125 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋)) |
127 | 112 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ) |
128 | 114 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ) |
129 | | elicc2 13005 |
. . . . . . . . . . . . . . . . 17
⊢ (((-π
+ 𝑋) ∈ ℝ ∧
(π + 𝑋) ∈ ℝ)
→ ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))) |
130 | 127, 128,
129 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))) |
131 | 118, 130 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))) |
132 | 131 | simp2d 1145 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉‘𝑖)) |
133 | 127, 119,
120, 132 | lesub1dd 11453 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋)) |
134 | 126, 133 | eqbrtrd 5080 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉‘𝑖) − 𝑋)) |
135 | 131 | simp3d 1146 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ≤ (π + 𝑋)) |
136 | 119, 128,
120, 135 | lesub1dd 11453 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋)) |
137 | 110 | recnd 10866 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈
ℂ) |
138 | 123 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ) |
139 | 137, 138 | pncand 11195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π) |
140 | 136, 139 | breqtrd 5084 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ π) |
141 | 109, 110,
121, 134, 140 | eliccd 42725 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) |
142 | | fourierdlem75.q |
. . . . . . . . . . 11
⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) |
143 | 141, 142 | fmptd 6936 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π)) |
144 | 143 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π)) |
145 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) |
146 | 106, 108,
144, 145 | fourierdlem8 43339 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆
(-π[,]π)) |
147 | 102, 146 | sstrid 3917 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆
(-π[,]π)) |
148 | 147 | resmptd 5913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))) |
149 | 148 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))) |
150 | | elfzofz 13263 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
151 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀)) |
152 | 142 | fvmpt2 6834 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
153 | 151, 141,
152 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
154 | 153 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
155 | | oveq1 7225 |
. . . . . . . . . 10
⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋)) |
156 | 155 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋)) |
157 | 123 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℂ) |
158 | 157 | subidd 11182 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑋 − 𝑋) = 0) |
159 | 154, 156,
158 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0) |
160 | 150, 159 | sylanl2 681 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0) |
161 | | fveq2 6722 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗)) |
162 | 161 | oveq1d 7233 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋)) |
163 | 162 | cbvmptv 5163 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)) |
164 | 142, 163 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)) |
165 | 164 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))) |
166 | | fveq2 6722 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1))) |
167 | 166 | oveq1d 7233 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
168 | 167 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
169 | 1 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ) |
170 | 15, 169 | resubcld 11265 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) |
171 | 165, 168,
14, 170 | fvmptd 6830 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
172 | 171 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
173 | 160, 172 | oveq12d 7236 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (0(,)((𝑉‘(𝑖 + 1)) − 𝑋))) |
174 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
175 | | fourierdlem75.o |
. . . . . . . . . . . . 13
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
176 | 4 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑀 ∈ ℕ) |
177 | 111, 113,
1, 5, 175, 4, 3, 142 | fourierdlem14 43345 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀)) |
178 | 177 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑄 ∈ (𝑂‘𝑀)) |
179 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 = 0) |
180 | | fourierdlem75.x |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ∈ ran 𝑉) |
181 | | ffn 6550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀)) |
182 | | fvelrnb 6778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)) |
183 | 117, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)) |
184 | 180, 183 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋) |
185 | 159 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) = 𝑋 → (𝑄‘𝑖) = 0)) |
186 | 185 | reximdva 3198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)) |
187 | 184, 186 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0) |
188 | 121, 142 | fmptd 6936 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
189 | | ffn 6550 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀)) |
190 | | fvelrnb 6778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)) |
191 | 188, 189,
190 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)) |
192 | 187, 191 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈ ran 𝑄) |
193 | 192 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 = 0) → 0 ∈ ran 𝑄) |
194 | 179, 193 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 ∈ ran 𝑄) |
195 | 175, 176,
178, 194 | fourierdlem12 43343 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
196 | 195 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
197 | 196 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
198 | 174, 197 | pm2.65da 817 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0) |
199 | 198 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0) |
200 | 199 | iffalsed 4455 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) |
201 | 160 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 0 = (𝑄‘𝑖)) |
202 | 201 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 = (𝑄‘𝑖)) |
203 | | elioo3g 12969 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ℝ*)
∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1))))) |
204 | 203 | biimpi 219 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ℝ*)
∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1))))) |
205 | 204 | simprld 772 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑠) |
206 | 205 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠) |
207 | 202, 206 | eqbrtrd 5080 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠) |
208 | 207 | iftrued 4452 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌) |
209 | 208 | oveq2d 7234 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) |
210 | 209 | oveq1d 7233 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) |
211 | 1 | rexrd 10888 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
212 | 211 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈
ℝ*) |
213 | 36 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈
ℝ*) |
214 | 169 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ) |
215 | | elioore 12970 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ) |
216 | 215 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ) |
217 | 214, 216 | readdcld 10867 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ) |
218 | 216, 207 | elrpd 12630 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ+) |
219 | 214, 218 | ltaddrpd 12666 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 < (𝑋 + 𝑠)) |
220 | 215 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ) |
221 | 188 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
222 | 221, 14 | ffvelrnd 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
223 | 222 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
224 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ) |
225 | 204 | simprrd 774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1))) |
226 | 225 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1))) |
227 | 220, 223,
224, 226 | ltadd2dd 10996 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1)))) |
228 | 171 | oveq2d 7234 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋))) |
229 | 123 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ) |
230 | 15 | recnd 10866 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ) |
231 | 229, 230 | pncan3d 11197 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1))) |
232 | 228, 231 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1))) |
233 | 232 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1))) |
234 | 227, 233 | breqtrd 5084 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1))) |
235 | 234 | adantlr 715 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1))) |
236 | 212, 213,
217, 219, 235 | eliood 42719 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ (𝑋(,)(𝑉‘(𝑖 + 1)))) |
237 | | fvres 6741 |
. . . . . . . . . . 11
⊢ ((𝑋 + 𝑠) ∈ (𝑋(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠))) |
238 | 236, 237 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠))) |
239 | 238 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) |
240 | 239 | oveq1d 7233 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑌) = (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌)) |
241 | 240 | oveq1d 7233 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑌) / 𝑠) = ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) |
242 | 200, 210,
241 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) |
243 | 173, 242 | mpteq12dva 5144 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))) |
244 | 101, 149,
243 | 3eqtrd 2781 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))) |
245 | 244, 160 | oveq12d 7236 |
. . 3
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) limℂ 0)) |
246 | 94, 98, 245 | 3eltr4d 2853 |
. 2
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
247 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) |
248 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) |
249 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) |
250 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ) |
251 | 1 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ) |
252 | 215 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ) |
253 | 251, 252 | readdcld 10867 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ) |
254 | 250, 253 | ffvelrnd 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) |
255 | 254 | recnd 10866 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
256 | 255 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
257 | 256 | 3adantl3 1170 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
258 | | limccl 24777 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ⊆
ℂ |
259 | 258, 31 | sseldi 3904 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℂ) |
260 | | fourierdlem75.w |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℝ) |
261 | 260 | recnd 10866 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ ℂ) |
262 | 259, 261 | ifcld 4490 |
. . . . . . . 8
⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) |
263 | 262 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) |
264 | 263 | 3ad2antl1 1187 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) |
265 | 257, 264 | subcld 11194 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ) |
266 | 215 | recnd 10866 |
. . . . . . 7
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ) |
267 | 266 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ) |
268 | | velsn 4562 |
. . . . . . . 8
⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0) |
269 | 198, 268 | sylnibr 332 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0}) |
270 | 269 | 3adantl3 1170 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0}) |
271 | 267, 270 | eldifd 3882 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖
{0})) |
272 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) |
273 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) |
274 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) |
275 | 261 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ) |
276 | | ioossre 13001 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ |
277 | 276 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) |
278 | 150, 119 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ) |
279 | 278 | rexrd 10888 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈
ℝ*) |
280 | 279 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈
ℝ*) |
281 | 36 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈
ℝ*) |
282 | 253 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ) |
283 | | iccssre 13022 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
284 | 104, 103,
283 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢
(-π[,]π) ⊆ ℝ |
285 | 284, 46 | sstri 3915 |
. . . . . . . . . . . . . . . . 17
⊢
(-π[,]π) ⊆ ℂ |
286 | 153, 141 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π)) |
287 | 150, 286 | sylan2 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π)) |
288 | 285, 287 | sseldi 3904 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ) |
289 | 229, 288 | addcomd 11039 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘𝑖)) = ((𝑄‘𝑖) + 𝑋)) |
290 | 150 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
291 | 150, 121 | sylan2 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ) |
292 | 142 | fvmpt2 6834 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
293 | 290, 291,
292 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
294 | 293 | oveq1d 7233 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑋) = (((𝑉‘𝑖) − 𝑋) + 𝑋)) |
295 | 278 | recnd 10866 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℂ) |
296 | 295, 229 | npcand 11198 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑉‘𝑖) − 𝑋) + 𝑋) = (𝑉‘𝑖)) |
297 | 289, 294,
296 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖))) |
298 | 297 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖))) |
299 | 293, 291 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
300 | 299 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ) |
301 | 205 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠) |
302 | 300, 220,
224, 301 | ltadd2dd 10996 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠)) |
303 | 298, 302 | eqbrtrd 5080 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠)) |
304 | 280, 281,
282, 303, 234 | eliood 42719 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) |
305 | | ioossre 13001 |
. . . . . . . . . . . 12
⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ |
306 | 305 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ) |
307 | 300, 301 | gtned 10972 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖)) |
308 | | fourierdlem75.r |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) |
309 | 297 | oveq2d 7234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑋 + (𝑄‘𝑖)))) |
310 | 308, 309 | eleqtrd 2840 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑋 + (𝑄‘𝑖)))) |
311 | 25, 169, 277, 272, 304, 306, 307, 310, 288 | fourierdlem53 43383 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) limℂ (𝑄‘𝑖))) |
312 | | ioosscn 13002 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ |
313 | 312 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ) |
314 | 261 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ) |
315 | 273, 313,
314, 288 | constlimc 42848 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) limℂ (𝑄‘𝑖))) |
316 | 272, 273,
274, 256, 275, 311, 315 | sublimc 42876 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) limℂ (𝑄‘𝑖))) |
317 | 316 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) limℂ (𝑄‘𝑖))) |
318 | | iftrue 4450 |
. . . . . . . . . 10
⊢ ((𝑉‘𝑖) < 𝑋 → if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌) = 𝑊) |
319 | 318 | oveq2d 7234 |
. . . . . . . . 9
⊢ ((𝑉‘𝑖) < 𝑋 → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊)) |
320 | 319 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊)) |
321 | 215 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ) |
322 | | 0red 10841 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈
ℝ) |
323 | 222 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
324 | 225 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1))) |
325 | 171 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
326 | 279 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘𝑖) ∈
ℝ*) |
327 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘(𝑖 + 1)) ∈
ℝ*) |
328 | 169 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ℝ) |
329 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘𝑖) < 𝑋) |
330 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) |
331 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ℝ) |
332 | 15 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
333 | 331, 332 | ltnled 10984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑋 < (𝑉‘(𝑖 + 1)) ↔ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋)) |
334 | 330, 333 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1))) |
335 | 334 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1))) |
336 | 326, 327,
328, 329, 335 | eliood 42719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) |
337 | 5, 4, 3, 180 | fourierdlem12 43343 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) |
338 | 337 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) |
339 | 336, 338 | condan 818 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋) |
340 | 15 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
341 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → 𝑋 ∈ ℝ) |
342 | 340, 341 | suble0d 11428 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋)) |
343 | 339, 342 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0) |
344 | 325, 343 | eqbrtrd 5080 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0) |
345 | 344 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0) |
346 | 321, 323,
322, 324, 345 | ltletrd 10997 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0) |
347 | 321, 322,
346 | ltnsymd 10986 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠) |
348 | 347 | iffalsed 4455 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊) |
349 | 348 | oveq2d 7234 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) |
350 | 349 | mpteq2dva 5155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))) |
351 | 350 | oveq1d 7233 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) limℂ (𝑄‘𝑖))) |
352 | 317, 320,
351 | 3eltr4d 2853 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖))) |
353 | 352 | 3adantl3 1170 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖))) |
354 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) |
355 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) |
356 | 259 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑌 ∈ ℂ) |
357 | 259 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ) |
358 | 354, 313,
357, 288 | constlimc 42848 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) limℂ (𝑄‘𝑖))) |
359 | 272, 354,
355, 256, 356, 311, 358 | sublimc 42876 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) limℂ (𝑄‘𝑖))) |
360 | 359 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) limℂ (𝑄‘𝑖))) |
361 | | iffalse 4453 |
. . . . . . . . . 10
⊢ (¬
(𝑉‘𝑖) < 𝑋 → if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌) = 𝑌) |
362 | 361 | oveq2d 7234 |
. . . . . . . . 9
⊢ (¬
(𝑉‘𝑖) < 𝑋 → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑌)) |
363 | 362 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑌)) |
364 | | 0red 10841 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈
ℝ) |
365 | 299 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ) |
366 | 215 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ) |
367 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 𝑋 ∈ ℝ) |
368 | 278 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑉‘𝑖) ∈ ℝ) |
369 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ¬ (𝑉‘𝑖) < 𝑋) |
370 | 367, 368,
369 | nltled 10987 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 𝑋 ≤ (𝑉‘𝑖)) |
371 | 368, 367 | subge0d 11427 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (0 ≤ ((𝑉‘𝑖) − 𝑋) ↔ 𝑋 ≤ (𝑉‘𝑖))) |
372 | 370, 371 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 0 ≤ ((𝑉‘𝑖) − 𝑋)) |
373 | 293 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖)) |
374 | 373 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖)) |
375 | 372, 374 | breqtrd 5084 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 0 ≤ (𝑄‘𝑖)) |
376 | 375 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄‘𝑖)) |
377 | 205 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠) |
378 | 364, 365,
366, 376, 377 | lelttrd 10995 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠) |
379 | 378 | iftrued 4452 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌) |
380 | 379 | oveq2d 7234 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) |
381 | 380 | mpteq2dva 5155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌))) |
382 | 381 | oveq1d 7233 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) limℂ (𝑄‘𝑖))) |
383 | 360, 363,
382 | 3eltr4d 2853 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖))) |
384 | 383 | 3adantl3 1170 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖))) |
385 | 353, 384 | pm2.61dan 813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) limℂ (𝑄‘𝑖))) |
386 | 313, 248,
288 | idlimc 42850 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) limℂ (𝑄‘𝑖))) |
387 | 386 | 3adant3 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) limℂ (𝑄‘𝑖))) |
388 | 293 | 3adant3 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
389 | 295 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) ∈ ℂ) |
390 | 229 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℂ) |
391 | | neqne 2948 |
. . . . . . . 8
⊢ (¬
(𝑉‘𝑖) = 𝑋 → (𝑉‘𝑖) ≠ 𝑋) |
392 | 391 | 3ad2ant3 1137 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) ≠ 𝑋) |
393 | 389, 390,
392 | subne0d 11203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) ≠ 0) |
394 | 388, 393 | eqnetrd 3008 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) ≠ 0) |
395 | 198 | 3adantl3 1170 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0) |
396 | 395 | neqned 2947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0) |
397 | 247, 248,
249, 265, 271, 385, 387, 394, 396 | divlimc 42880 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) limℂ (𝑄‘𝑖))) |
398 | | iffalse 4453 |
. . . . . 6
⊢ (¬
(𝑉‘𝑖) = 𝑋 → if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) |
399 | 95, 398 | syl5eq 2790 |
. . . . 5
⊢ (¬
(𝑉‘𝑖) = 𝑋 → 𝐴 = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) |
400 | 399 | 3ad2ant3 1137 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) |
401 | | ioossre 13001 |
. . . . . . . . . . . . 13
⊢ (𝑋(,)+∞) ⊆
ℝ |
402 | 401 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋(,)+∞) ⊆
ℝ) |
403 | 24, 402 | fssresd 6591 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ (𝑋(,)+∞)):(𝑋(,)+∞)⟶ℝ) |
404 | 401, 47 | sstrid 3917 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋(,)+∞) ⊆
ℂ) |
405 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → +∞ ∈
ℝ*) |
406 | 1 | ltpnfd 12718 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 < +∞) |
407 | 52, 405, 1, 406 | lptioo1cn 42870 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)+∞))) |
408 | 403, 404,
407, 31 | limcrecl 42853 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
409 | 24, 1, 408, 260, 99 | fourierdlem9 43340 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ) |
410 | 409 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ) |
411 | 410, 147 | feqresmpt 6786 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠))) |
412 | 147 | sselda 3906 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π)) |
413 | | 0cnd 10831 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈
ℂ) |
414 | 262 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) |
415 | 256, 414 | subcld 11194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ) |
416 | 266 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ) |
417 | 198 | neqned 2947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0) |
418 | 415, 416,
417 | divcld 11613 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ) |
419 | 413, 418 | ifcld 4490 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) |
420 | 99 | fvmpt2 6834 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (-π[,]π) ∧
if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
421 | 412, 419,
420 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
422 | 198 | iffalsed 4455 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) |
423 | 421, 422 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) |
424 | 423 | mpteq2dva 5155 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
425 | 411, 424 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
426 | 425 | 3adant3 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
427 | 426 | oveq1d 7233 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) limℂ (𝑄‘𝑖))) |
428 | 397, 400,
427 | 3eltr4d 2853 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
429 | 428 | 3expa 1120 |
. 2
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
430 | 246, 429 | pm2.61dan 813 |
1
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |