Proof of Theorem fourierdlem3
Step | Hyp | Ref
| Expression |
1 | | oveq2 7172 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀)) |
2 | 1 | oveq2d 7180 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((-π[,]π) ↑m
(0...𝑚)) = ((-π[,]π)
↑m (0...𝑀))) |
3 | | fveqeq2 6677 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑝‘𝑚) = π ↔ (𝑝‘𝑀) = π)) |
4 | 3 | anbi2d 632 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ↔ ((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π))) |
5 | | oveq2 7172 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀)) |
6 | 5 | raleqdv 3315 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))) |
7 | 4, 6 | anbi12d 634 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))))) |
8 | 2, 7 | rabeqbidv 3386 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑝 ∈ ((-π[,]π) ↑m
(0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ ((-π[,]π) ↑m
(0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
9 | | fourierdlem3.1 |
. . . 4
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ ((-π[,]π) ↑m
(0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
10 | | ovex 7197 |
. . . . 5
⊢
((-π[,]π) ↑m (0...𝑀)) ∈ V |
11 | 10 | rabex 5197 |
. . . 4
⊢ {𝑝 ∈ ((-π[,]π)
↑m (0...𝑀))
∣ (((𝑝‘0) =
-π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V |
12 | 8, 9, 11 | fvmpt 6769 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑃‘𝑀) = {𝑝 ∈ ((-π[,]π) ↑m
(0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
13 | 12 | eleq2d 2818 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ 𝑄 ∈ {𝑝 ∈ ((-π[,]π) ↑m
(0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})) |
14 | | fveq1 6667 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0)) |
15 | 14 | eqeq1d 2740 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘0) = -π ↔ (𝑄‘0) = -π)) |
16 | | fveq1 6667 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑀) = (𝑄‘𝑀)) |
17 | 16 | eqeq1d 2740 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑀) = π ↔ (𝑄‘𝑀) = π)) |
18 | 15, 17 | anbi12d 634 |
. . . 4
⊢ (𝑝 = 𝑄 → (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ↔ ((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π))) |
19 | | fveq1 6667 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑖) = (𝑄‘𝑖)) |
20 | | fveq1 6667 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1))) |
21 | 19, 20 | breq12d 5040 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
22 | 21 | ralbidv 3109 |
. . . 4
⊢ (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
23 | 18, 22 | anbi12d 634 |
. . 3
⊢ (𝑝 = 𝑄 → ((((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
24 | 23 | elrab 3585 |
. 2
⊢ (𝑄 ∈ {𝑝 ∈ ((-π[,]π) ↑m
(0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ ((-π[,]π) ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
25 | 13, 24 | bitrdi 290 |
1
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ ((-π[,]π) ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |