Proof of Theorem fourierdlem2
Step | Hyp | Ref
| Expression |
1 | | oveq2 6918 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀)) |
2 | 1 | oveq2d 6926 |
. . . . 5
⊢ (𝑚 = 𝑀 → (ℝ ↑𝑚
(0...𝑚)) = (ℝ
↑𝑚 (0...𝑀))) |
3 | | fveq2 6437 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑝‘𝑚) = (𝑝‘𝑀)) |
4 | 3 | eqeq1d 2827 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑝‘𝑚) = 𝐵 ↔ (𝑝‘𝑀) = 𝐵)) |
5 | 4 | anbi2d 622 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵))) |
6 | | oveq2 6918 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀)) |
7 | 6 | raleqdv 3356 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))) |
8 | 5, 7 | anbi12d 624 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))))) |
9 | 2, 8 | rabeqbidv 3408 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑𝑚
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
10 | | fourierdlem2.1 |
. . . 4
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
11 | | ovex 6942 |
. . . . 5
⊢ (ℝ
↑𝑚 (0...𝑀)) ∈ V |
12 | 11 | rabex 5039 |
. . . 4
⊢ {𝑝 ∈ (ℝ
↑𝑚 (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V |
13 | 9, 10, 12 | fvmpt 6533 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑃‘𝑀) = {𝑝 ∈ (ℝ ↑𝑚
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
14 | 13 | eleq2d 2892 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ 𝑄 ∈ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})) |
15 | | fveq1 6436 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0)) |
16 | 15 | eqeq1d 2827 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘0) = 𝐴 ↔ (𝑄‘0) = 𝐴)) |
17 | | fveq1 6436 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑀) = (𝑄‘𝑀)) |
18 | 17 | eqeq1d 2827 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑀) = 𝐵 ↔ (𝑄‘𝑀) = 𝐵)) |
19 | 16, 18 | anbi12d 624 |
. . . 4
⊢ (𝑝 = 𝑄 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ↔ ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))) |
20 | | fveq1 6436 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑖) = (𝑄‘𝑖)) |
21 | | fveq1 6436 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1))) |
22 | 20, 21 | breq12d 4888 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
23 | 22 | ralbidv 3195 |
. . . 4
⊢ (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
24 | 19, 23 | anbi12d 624 |
. . 3
⊢ (𝑝 = 𝑄 → ((((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
25 | 24 | elrab 3585 |
. 2
⊢ (𝑄 ∈ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
26 | 14, 25 | syl6bb 279 |
1
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |