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 43650 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
6 | 1, 5 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
7 | 6 | simprd 496 |
. . . . 5
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
8 | 7 | simpld 495 |
. . . 4
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
9 | 8 | simpld 495 |
. . 3
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
10 | 6 | simpld 495 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
11 | | elmapi 8637 |
. . . . 5
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
13 | | 0zd 12331 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
14 | 2 | nnzd 12425 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
15 | | 0red 10978 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
16 | 15 | leidd 11541 |
. . . . 5
⊢ (𝜑 → 0 ≤ 0) |
17 | 2 | nnred 11988 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
18 | 2 | nngt0d 12022 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑀) |
19 | 15, 17, 18 | ltled 11123 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑀) |
20 | 13, 14, 13, 16, 19 | elfzd 13247 |
. . . 4
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
21 | 12, 20 | ffvelrnd 6962 |
. . 3
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
22 | 9, 21 | eqeltrrd 2840 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℝ) |
23 | 8 | simprd 496 |
. . 3
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
24 | 17 | leidd 11541 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
25 | 13, 14, 14, 19, 24 | elfzd 13247 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
26 | 12, 25 | ffvelrnd 6962 |
. . 3
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) |
27 | 23, 26 | eqeltrrd 2840 |
. 2
⊢ (𝜑 → 𝐵 ∈ ℝ) |
28 | | 1zzd 12351 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
29 | | 0le1 11498 |
. . . . . 6
⊢ 0 ≤
1 |
30 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≤ 1) |
31 | 2 | nnge1d 12021 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝑀) |
32 | 13, 14, 28, 30, 31 | elfzd 13247 |
. . . 4
⊢ (𝜑 → 1 ∈ (0...𝑀)) |
33 | 12, 32 | ffvelrnd 6962 |
. . 3
⊢ (𝜑 → (𝑄‘1) ∈ ℝ) |
34 | | elfzo 13389 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 <
𝑀))) |
35 | 13, 13, 14, 34 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 <
𝑀))) |
36 | 16, 18, 35 | mpbir2and 710 |
. . . . 5
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
37 | | 0re 10977 |
. . . . . 6
⊢ 0 ∈
ℝ |
38 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀))) |
39 | 38 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀)))) |
40 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) |
41 | | oveq1 7282 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
42 | 41 | fveq2d 6778 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1))) |
43 | 40, 42 | breq12d 5087 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1)))) |
44 | 39, 43 | imbi12d 345 |
. . . . . . 7
⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))) |
45 | 7 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
46 | 45 | r19.21bi 3134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
47 | 44, 46 | vtoclg 3505 |
. . . . . 6
⊢ (0 ∈
ℝ → ((𝜑 ∧ 0
∈ (0..^𝑀)) →
(𝑄‘0) < (𝑄‘(0 +
1)))) |
48 | 37, 47 | ax-mp 5 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))) |
49 | 36, 48 | mpdan 684 |
. . . 4
⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1))) |
50 | | 0p1e1 12095 |
. . . . . 6
⊢ (0 + 1) =
1 |
51 | 50 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0 + 1) =
1) |
52 | 51 | fveq2d 6778 |
. . . 4
⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1)) |
53 | 49, 9, 52 | 3brtr3d 5105 |
. . 3
⊢ (𝜑 → 𝐴 < (𝑄‘1)) |
54 | | nnuz 12621 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
55 | 2, 54 | eleqtrdi 2849 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
56 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
57 | | 0zd 12331 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ) |
58 | | elfzel2 13254 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ) |
59 | | elfzelz 13256 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ) |
60 | | 0red 10978 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ) |
61 | 59 | zred 12426 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ) |
62 | | 1red 10976 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ) |
63 | | 0lt1 11497 |
. . . . . . . . . . 11
⊢ 0 <
1 |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 0 < 1) |
65 | | elfzle1 13259 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖) |
66 | 60, 62, 61, 64, 65 | ltletrd 11135 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖) |
67 | 60, 61, 66 | ltled 11123 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖) |
68 | | elfzle2 13260 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀) |
69 | 57, 58, 59, 67, 68 | elfzd 13247 |
. . . . . . 7
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ (0...𝑀)) |
70 | 69 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀)) |
71 | 56, 70 | ffvelrnd 6962 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
72 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ) |
73 | | 0zd 12331 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈
ℤ) |
74 | 14 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
75 | | elfzelz 13256 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ) |
76 | 75 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ) |
77 | | 0red 10978 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈
ℝ) |
78 | 75 | zred 12426 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ) |
79 | | 1red 10976 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈
ℝ) |
80 | 63 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 <
1) |
81 | | elfzle1 13259 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖) |
82 | 77, 79, 78, 80, 81 | ltletrd 11135 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖) |
83 | 77, 78, 82 | ltled 11123 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ≤ 𝑖) |
84 | 83 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ 𝑖) |
85 | 78 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ) |
86 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ) |
87 | | peano2rem 11288 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈
ℝ) |
88 | 86, 87 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ) |
89 | | elfzle2 13260 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1)) |
90 | 89 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1)) |
91 | 86 | ltm1d 11907 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀) |
92 | 85, 88, 86, 90, 91 | lelttrd 11133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀) |
93 | 85, 86, 92 | ltled 11123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀) |
94 | 73, 74, 76, 84, 93 | elfzd 13247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0...𝑀)) |
95 | 72, 94 | ffvelrnd 6962 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ) |
96 | 76 | peano2zd 12429 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ) |
97 | | 0red 10978 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈
ℝ) |
98 | | peano2re 11148 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈
ℝ) |
99 | 85, 98 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ) |
100 | | 1red 10976 |
. . . . . . . . . 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 11905 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1)) |
104 | 79, 78, 102, 81, 103 | lelttrd 11133 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1)) |
105 | 104 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1)) |
106 | 97, 100, 99, 101, 105 | lttrd 11136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1)) |
107 | 97, 99, 106 | ltled 11123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1)) |
108 | 85, 88, 100, 90 | leadd1dd 11589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1)) |
109 | 2 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) |
110 | | 1cnd 10970 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
111 | 109, 110 | npcand 11336 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
112 | 111 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀) |
113 | 108, 112 | breqtrd 5100 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀) |
114 | 73, 74, 96, 107, 113 | elfzd 13247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ (0...𝑀)) |
115 | 72, 114 | ffvelrnd 6962 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
116 | | elfzo 13389 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (𝑖 ∈
(0..^𝑀) ↔ (0 ≤
𝑖 ∧ 𝑖 < 𝑀))) |
117 | 76, 73, 74, 116 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
118 | 84, 92, 117 | mpbir2and 710 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀)) |
119 | 118, 46 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
120 | 95, 115, 119 | ltled 11123 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1))) |
121 | 55, 71, 120 | monoord 13753 |
. . . 4
⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀)) |
122 | 121, 23 | breqtrd 5100 |
. . 3
⊢ (𝜑 → (𝑄‘1) ≤ 𝐵) |
123 | 22, 33, 27, 53, 122 | ltletrd 11135 |
. 2
⊢ (𝜑 → 𝐴 < 𝐵) |
124 | 22, 27, 123 | 3jca 1127 |
1
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |