Step | Hyp | Ref
| Expression |
1 | | fourierdlem14.v |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) |
2 | | fourierdlem14.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | | fourierdlem14.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
4 | 3 | fourierdlem2 43619 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))) |
6 | 1, 5 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))) |
7 | 6 | simpld 495 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ (ℝ ↑m
(0...𝑀))) |
8 | | elmapi 8618 |
. . . . . . . 8
⊢ (𝑉 ∈ (ℝ
↑m (0...𝑀))
→ 𝑉:(0...𝑀)⟶ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ) |
10 | 9 | ffvelrnda 6956 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ) |
11 | | fourierdlem14.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) |
12 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ) |
13 | 10, 12 | resubcld 11401 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ) |
14 | | fourierdlem14.q |
. . . . 5
⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) |
15 | 13, 14 | fmptd 6983 |
. . . 4
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
16 | | reex 10961 |
. . . . . 6
⊢ ℝ
∈ V |
17 | 16 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
18 | | ovex 7302 |
. . . . . 6
⊢
(0...𝑀) ∈
V |
19 | 18 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0...𝑀) ∈ V) |
20 | 17, 19 | elmapd 8610 |
. . . 4
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)) |
21 | 15, 20 | mpbird 256 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
22 | 14 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))) |
23 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑉‘𝑖) = (𝑉‘0)) |
24 | 23 | oveq1d 7284 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘0) − 𝑋)) |
25 | 24 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘0) − 𝑋)) |
26 | | 0zd 12329 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
27 | 2 | nnzd 12422 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
28 | | 0le0 12072 |
. . . . . . . 8
⊢ 0 ≤
0 |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 0) |
30 | | 0red 10977 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
31 | 2 | nnred 11986 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
32 | 2 | nngt0d 12020 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑀) |
33 | 30, 31, 32 | ltled 11121 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑀) |
34 | 26, 27, 26, 29, 33 | elfzd 13244 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
35 | 9, 34 | ffvelrnd 6957 |
. . . . . . 7
⊢ (𝜑 → (𝑉‘0) ∈ ℝ) |
36 | 35, 11 | resubcld 11401 |
. . . . . 6
⊢ (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ) |
37 | 22, 25, 34, 36 | fvmptd 6877 |
. . . . 5
⊢ (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋)) |
38 | 6 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))) |
39 | 38 | simpld 495 |
. . . . . . 7
⊢ (𝜑 → ((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋))) |
40 | 39 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝑉‘0) = (𝐴 + 𝑋)) |
41 | 40 | oveq1d 7284 |
. . . . 5
⊢ (𝜑 → ((𝑉‘0) − 𝑋) = ((𝐴 + 𝑋) − 𝑋)) |
42 | | fourierdlem14.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
43 | 42 | recnd 11002 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
44 | 11 | recnd 11002 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℂ) |
45 | 43, 44 | pncand 11331 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑋) − 𝑋) = 𝐴) |
46 | 37, 41, 45 | 3eqtrd 2784 |
. . . 4
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
47 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 𝑀 → (𝑉‘𝑖) = (𝑉‘𝑀)) |
48 | 47 | oveq1d 7284 |
. . . . . . 7
⊢ (𝑖 = 𝑀 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑀) − 𝑋)) |
49 | 48 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑀) − 𝑋)) |
50 | 31 | leidd 11539 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
51 | 26, 27, 27, 33, 50 | elfzd 13244 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
52 | 9, 51 | ffvelrnd 6957 |
. . . . . . 7
⊢ (𝜑 → (𝑉‘𝑀) ∈ ℝ) |
53 | 52, 11 | resubcld 11401 |
. . . . . 6
⊢ (𝜑 → ((𝑉‘𝑀) − 𝑋) ∈ ℝ) |
54 | 22, 49, 51, 53 | fvmptd 6877 |
. . . . 5
⊢ (𝜑 → (𝑄‘𝑀) = ((𝑉‘𝑀) − 𝑋)) |
55 | 39 | simprd 496 |
. . . . . 6
⊢ (𝜑 → (𝑉‘𝑀) = (𝐵 + 𝑋)) |
56 | 55 | oveq1d 7284 |
. . . . 5
⊢ (𝜑 → ((𝑉‘𝑀) − 𝑋) = ((𝐵 + 𝑋) − 𝑋)) |
57 | | fourierdlem14.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
58 | 57 | recnd 11002 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
59 | 58, 44 | pncand 11331 |
. . . . 5
⊢ (𝜑 → ((𝐵 + 𝑋) − 𝑋) = 𝐵) |
60 | 54, 56, 59 | 3eqtrd 2784 |
. . . 4
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
61 | 46, 60 | jca 512 |
. . 3
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
62 | | elfzofz 13399 |
. . . . . . 7
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
63 | 62, 10 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ) |
64 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ) |
65 | | fzofzp1 13480 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
66 | 65 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
67 | 64, 66 | ffvelrnd 6957 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
68 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ) |
69 | 38 | simprd 496 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
70 | 69 | r19.21bi 3135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
71 | 63, 67, 68, 70 | ltsub1dd 11585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋)) |
72 | 62 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
73 | 62, 13 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ) |
74 | 14 | fvmpt2 6881 |
. . . . . 6
⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
75 | 72, 73, 74 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
76 | | fveq2 6769 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗)) |
77 | 76 | oveq1d 7284 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋)) |
78 | 77 | cbvmptv 5192 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)) |
79 | 14, 78 | eqtri 2768 |
. . . . . . 7
⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)) |
80 | 79 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))) |
81 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1))) |
82 | 81 | oveq1d 7284 |
. . . . . . 7
⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
83 | 82 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
84 | 67, 68 | resubcld 11401 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) |
85 | 80, 83, 66, 84 | fvmptd 6877 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
86 | 71, 75, 85 | 3brtr4d 5111 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
87 | 86 | ralrimiva 3110 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
88 | 21, 61, 87 | jca32 516 |
. 2
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
89 | | fourierdlem14.o |
. . . 4
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
90 | 89 | fourierdlem2 43619 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑂‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
91 | 2, 90 | syl 17 |
. 2
⊢ (𝜑 → (𝑄 ∈ (𝑂‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
92 | 88, 91 | mpbird 256 |
1
⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀)) |