Proof of Theorem fourierdlem3
Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀)) |
2 | 1 | oveq2d 6666 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((-π[,]π)
↑𝑚 (0...𝑚)) = ((-π[,]π)
↑𝑚 (0...𝑀))) |
3 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑝‘𝑚) = (𝑝‘𝑀)) |
4 | 3 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑝‘𝑚) = π ↔ (𝑝‘𝑀) = π)) |
5 | 4 | anbi2d 740 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ↔ ((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π))) |
6 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀)) |
7 | 6 | raleqdv 3144 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))) |
8 | 5, 7 | anbi12d 747 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))))) |
9 | 2, 8 | rabeqbidv 3195 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
10 | | fourierdlem3.1 |
. . . 4
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
11 | | ovex 6678 |
. . . . 5
⊢
((-π[,]π) ↑𝑚 (0...𝑀)) ∈ V |
12 | 11 | rabex 4813 |
. . . 4
⊢ {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V |
13 | 9, 10, 12 | fvmpt 6282 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑃‘𝑀) = {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
14 | 13 | eleq2d 2687 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ 𝑄 ∈ {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})) |
15 | | fveq1 6190 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0)) |
16 | 15 | eqeq1d 2624 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘0) = -π ↔ (𝑄‘0) = -π)) |
17 | | fveq1 6190 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑀) = (𝑄‘𝑀)) |
18 | 17 | eqeq1d 2624 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑀) = π ↔ (𝑄‘𝑀) = π)) |
19 | 16, 18 | anbi12d 747 |
. . . 4
⊢ (𝑝 = 𝑄 → (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ↔ ((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π))) |
20 | | fveq1 6190 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑖) = (𝑄‘𝑖)) |
21 | | fveq1 6190 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1))) |
22 | 20, 21 | breq12d 4666 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
23 | 22 | ralbidv 2986 |
. . . 4
⊢ (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
24 | 19, 23 | anbi12d 747 |
. . 3
⊢ (𝑝 = 𝑄 → ((((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
25 | 24 | elrab 3363 |
. 2
⊢ (𝑄 ∈ {𝑝 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
26 | 14, 25 | syl6bb 276 |
1
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ ((-π[,]π)
↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |