Proof of Theorem fourierdlem2
| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀)) |
| 2 | 1 | oveq2d 7447 |
. . . . 5
⊢ (𝑚 = 𝑀 → (ℝ ↑m
(0...𝑚)) = (ℝ
↑m (0...𝑀))) |
| 3 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑝‘𝑚) = 𝐵 ↔ (𝑝‘𝑀) = 𝐵)) |
| 4 | 3 | anbi2d 630 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵))) |
| 5 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀)) |
| 6 | 5 | raleqdv 3326 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))) |
| 7 | 4, 6 | anbi12d 632 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))))) |
| 8 | 2, 7 | rabeqbidv 3455 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 9 | | fourierdlem2.1 |
. . . 4
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 10 | | ovex 7464 |
. . . . 5
⊢ (ℝ
↑m (0...𝑀))
∈ V |
| 11 | 10 | rabex 5339 |
. . . 4
⊢ {𝑝 ∈ (ℝ
↑m (0...𝑀))
∣ (((𝑝‘0) =
𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V |
| 12 | 8, 9, 11 | fvmpt 7016 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑃‘𝑀) = {𝑝 ∈ (ℝ ↑m
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 13 | 12 | eleq2d 2827 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ 𝑄 ∈ {𝑝 ∈ (ℝ ↑m
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})) |
| 14 | | fveq1 6905 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0)) |
| 15 | 14 | eqeq1d 2739 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘0) = 𝐴 ↔ (𝑄‘0) = 𝐴)) |
| 16 | | fveq1 6905 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑀) = (𝑄‘𝑀)) |
| 17 | 16 | eqeq1d 2739 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑀) = 𝐵 ↔ (𝑄‘𝑀) = 𝐵)) |
| 18 | 15, 17 | anbi12d 632 |
. . . 4
⊢ (𝑝 = 𝑄 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ↔ ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))) |
| 19 | | fveq1 6905 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘𝑖) = (𝑄‘𝑖)) |
| 20 | | fveq1 6905 |
. . . . . 6
⊢ (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1))) |
| 21 | 19, 20 | breq12d 5156 |
. . . . 5
⊢ (𝑝 = 𝑄 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
| 22 | 21 | ralbidv 3178 |
. . . 4
⊢ (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
| 23 | 18, 22 | anbi12d 632 |
. . 3
⊢ (𝑝 = 𝑄 → ((((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
| 24 | 23 | elrab 3692 |
. 2
⊢ (𝑄 ∈ {𝑝 ∈ (ℝ ↑m
(0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
| 25 | 13, 24 | bitrdi 287 |
1
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |