Proof of Theorem fourierdlem11
Step | Hyp | Ref
| Expression |
1 | | fourierdlem11.q |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
2 | | fourierdlem11.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | | fourierdlem11.p |
. . . . . . . . 9
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
4 | 3 | fourierdlem2 43233 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
6 | 1, 5 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
7 | 6 | simprd 499 |
. . . . 5
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
8 | 7 | simpld 498 |
. . . 4
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
9 | 8 | simpld 498 |
. . 3
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
10 | 6 | simpld 498 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
11 | | elmapi 8472 |
. . . . 5
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
13 | | 0zd 12087 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
14 | 2 | nnzd 12180 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
15 | | 0red 10735 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
16 | 15 | leidd 11297 |
. . . . 5
⊢ (𝜑 → 0 ≤ 0) |
17 | 2 | nnred 11744 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
18 | 2 | nngt0d 11778 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑀) |
19 | 15, 17, 18 | ltled 10879 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑀) |
20 | 13, 14, 13, 16, 19 | elfzd 13002 |
. . . 4
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
21 | 12, 20 | ffvelrnd 6875 |
. . 3
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
22 | 9, 21 | eqeltrrd 2835 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℝ) |
23 | 8 | simprd 499 |
. . 3
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
24 | 17 | leidd 11297 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
25 | 13, 14, 14, 19, 24 | elfzd 13002 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
26 | 12, 25 | ffvelrnd 6875 |
. . 3
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) |
27 | 23, 26 | eqeltrrd 2835 |
. 2
⊢ (𝜑 → 𝐵 ∈ ℝ) |
28 | | 1zzd 12107 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
29 | | 0le1 11254 |
. . . . . 6
⊢ 0 ≤
1 |
30 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≤ 1) |
31 | 2 | nnge1d 11777 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝑀) |
32 | 13, 14, 28, 30, 31 | elfzd 13002 |
. . . 4
⊢ (𝜑 → 1 ∈ (0...𝑀)) |
33 | 12, 32 | ffvelrnd 6875 |
. . 3
⊢ (𝜑 → (𝑄‘1) ∈ ℝ) |
34 | | elfzo 13144 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 <
𝑀))) |
35 | 13, 13, 14, 34 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 <
𝑀))) |
36 | 16, 18, 35 | mpbir2and 713 |
. . . . 5
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
37 | | 0re 10734 |
. . . . . 6
⊢ 0 ∈
ℝ |
38 | | eleq1 2821 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀))) |
39 | 38 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀)))) |
40 | | fveq2 6687 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) |
41 | | oveq1 7190 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
42 | 41 | fveq2d 6691 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1))) |
43 | 40, 42 | breq12d 5053 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1)))) |
44 | 39, 43 | imbi12d 348 |
. . . . . . 7
⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))) |
45 | 7 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
46 | 45 | r19.21bi 3122 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
47 | 44, 46 | vtoclg 3473 |
. . . . . 6
⊢ (0 ∈
ℝ → ((𝜑 ∧ 0
∈ (0..^𝑀)) →
(𝑄‘0) < (𝑄‘(0 +
1)))) |
48 | 37, 47 | ax-mp 5 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))) |
49 | 36, 48 | mpdan 687 |
. . . 4
⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1))) |
50 | | 0p1e1 11851 |
. . . . . 6
⊢ (0 + 1) =
1 |
51 | 50 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0 + 1) =
1) |
52 | 51 | fveq2d 6691 |
. . . 4
⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1)) |
53 | 49, 9, 52 | 3brtr3d 5071 |
. . 3
⊢ (𝜑 → 𝐴 < (𝑄‘1)) |
54 | | nnuz 12376 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
55 | 2, 54 | eleqtrdi 2844 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
56 | 12 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
57 | | 0zd 12087 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ) |
58 | | elfzel2 13009 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ) |
59 | | elfzelz 13011 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ) |
60 | | 0red 10735 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ) |
61 | 59 | zred 12181 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ) |
62 | | 1red 10733 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ) |
63 | | 0lt1 11253 |
. . . . . . . . . . 11
⊢ 0 <
1 |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 0 < 1) |
65 | | elfzle1 13014 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖) |
66 | 60, 62, 61, 64, 65 | ltletrd 10891 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖) |
67 | 60, 61, 66 | ltled 10879 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖) |
68 | | elfzle2 13015 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀) |
69 | 57, 58, 59, 67, 68 | elfzd 13002 |
. . . . . . 7
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ (0...𝑀)) |
70 | 69 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀)) |
71 | 56, 70 | ffvelrnd 6875 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
72 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ) |
73 | | 0zd 12087 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈
ℤ) |
74 | 14 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
75 | | elfzelz 13011 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ) |
76 | 75 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ) |
77 | | 0red 10735 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈
ℝ) |
78 | 75 | zred 12181 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ) |
79 | | 1red 10733 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈
ℝ) |
80 | 63 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 <
1) |
81 | | elfzle1 13014 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖) |
82 | 77, 79, 78, 80, 81 | ltletrd 10891 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖) |
83 | 77, 78, 82 | ltled 10879 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ≤ 𝑖) |
84 | 83 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ 𝑖) |
85 | 78 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ) |
86 | 17 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ) |
87 | | peano2rem 11044 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈
ℝ) |
88 | 86, 87 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ) |
89 | | elfzle2 13015 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1)) |
90 | 89 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1)) |
91 | 86 | ltm1d 11663 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀) |
92 | 85, 88, 86, 90, 91 | lelttrd 10889 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀) |
93 | 85, 86, 92 | ltled 10879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀) |
94 | 73, 74, 76, 84, 93 | elfzd 13002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0...𝑀)) |
95 | 72, 94 | ffvelrnd 6875 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ) |
96 | 76 | peano2zd 12184 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ) |
97 | | 0red 10735 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈
ℝ) |
98 | | peano2re 10904 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈
ℝ) |
99 | 85, 98 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ) |
100 | | 1red 10733 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 ∈
ℝ) |
101 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 <
1) |
102 | 78, 98 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → (𝑖 + 1) ∈ ℝ) |
103 | 78 | ltp1d 11661 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1)) |
104 | 79, 78, 102, 81, 103 | lelttrd 10889 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1)) |
105 | 104 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1)) |
106 | 97, 100, 99, 101, 105 | lttrd 10892 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1)) |
107 | 97, 99, 106 | ltled 10879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1)) |
108 | 85, 88, 100, 90 | leadd1dd 11345 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1)) |
109 | 2 | nncnd 11745 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) |
110 | | 1cnd 10727 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
111 | 109, 110 | npcand 11092 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
112 | 111 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀) |
113 | 108, 112 | breqtrd 5066 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀) |
114 | 73, 74, 96, 107, 113 | elfzd 13002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ (0...𝑀)) |
115 | 72, 114 | ffvelrnd 6875 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
116 | | elfzo 13144 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (𝑖 ∈
(0..^𝑀) ↔ (0 ≤
𝑖 ∧ 𝑖 < 𝑀))) |
117 | 76, 73, 74, 116 | syl3anc 1372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
118 | 84, 92, 117 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀)) |
119 | 118, 46 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
120 | 95, 115, 119 | ltled 10879 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1))) |
121 | 55, 71, 120 | monoord 13505 |
. . . 4
⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀)) |
122 | 121, 23 | breqtrd 5066 |
. . 3
⊢ (𝜑 → (𝑄‘1) ≤ 𝐵) |
123 | 22, 33, 27, 53, 122 | ltletrd 10891 |
. 2
⊢ (𝜑 → 𝐴 < 𝐵) |
124 | 22, 27, 123 | 3jca 1129 |
1
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |