Step | Hyp | Ref
| Expression |
1 | | fourierdlem54.n |
. . 3
⊢ 𝑁 = ((#‘𝐻) − 1) |
2 | | 2z 11409 |
. . . . . 6
⊢ 2 ∈
ℤ |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℤ) |
4 | | fourierdlem54.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℝ) |
5 | | prid1g 4295 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷}) |
6 | | elun1 3780 |
. . . . . . . . . 10
⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
7 | 4, 5, 6 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
8 | | fourierdlem54.h |
. . . . . . . . 9
⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
9 | 7, 8 | syl6eleqr 2712 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝐻) |
10 | | ne0i 3921 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐻 → 𝐻 ≠ ∅) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ≠ ∅) |
12 | | prfi 8235 |
. . . . . . . . . 10
⊢ {𝐶, 𝐷} ∈ Fin |
13 | | fourierdlem54.p |
. . . . . . . . . . . . 13
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
14 | | fourierdlem54.m |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) |
15 | | fourierdlem54.q |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
16 | 13, 14, 15 | fourierdlem11 40335 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
17 | 16 | simp1d 1073 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
18 | 16 | simp2d 1074 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
19 | 16 | simp3d 1075 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
20 | | fourierdlem54.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝐵 − 𝐴) |
21 | 13, 14, 15 | fourierdlem15 40339 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |
22 | | frn 6053 |
. . . . . . . . . . . 12
⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵)) |
24 | 13 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
25 | 14, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
26 | 15, 25 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
27 | 26 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑𝑚
(0...𝑀))) |
28 | | elmapi 7879 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (ℝ
↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
29 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀)) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) |
31 | | fzfid 12772 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
32 | | fnfi 8238 |
. . . . . . . . . . . . 13
⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin) |
33 | 30, 31, 32 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ Fin) |
34 | | rnfi 8249 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ Fin → ran 𝑄 ∈ Fin) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝑄 ∈ Fin) |
36 | 26 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
37 | 36 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
38 | 37 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
39 | 14 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
40 | | nn0uz 11722 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
41 | 39, 40 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
42 | | eluzfz1 12348 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
44 | | fnfvelrn 6356 |
. . . . . . . . . . . . 13
⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄) |
45 | 30, 43, 44 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄) |
46 | 38, 45 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ran 𝑄) |
47 | 37 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
48 | | eluzfz2 12349 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) |
49 | 41, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
50 | | fnfvelrn 6356 |
. . . . . . . . . . . . 13
⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄) |
51 | 30, 49, 50 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄) |
52 | 47, 51 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ran 𝑄) |
53 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
54 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ((ran
𝑄 × ran 𝑄) ∖ I ) = ((ran 𝑄 × ran 𝑄) ∖ I ) |
55 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ran ((abs
∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )) = ran ((abs ∘ − )
↾ ((ran 𝑄 × ran
𝑄) ∖ I
)) |
56 | | eqid 2622 |
. . . . . . . . . . 11
⊢ inf(ran
((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < ) = inf(ran
((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, <
) |
57 | | fourierdlem54.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℝ) |
58 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
59 | | eqid 2622 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t (𝐶[,]𝐷)) = ((topGen‘ran (,))
↾t (𝐶[,]𝐷)) |
60 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇))) |
61 | 60 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
62 | 61 | rexbidv 3052 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
63 | 62 | cbvrabv 3199 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} |
64 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇)) |
65 | 64 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇))) |
66 | 65 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)) |
67 | 66 | anbi1d 741 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄))) |
68 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇)) |
69 | 68 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇))) |
70 | 69 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
71 | 70 | anbi2d 740 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))) |
72 | 67, 71 | cbvrex2v 3180 |
. . . . . . . . . . . 12
⊢
(∃𝑖 ∈
ℤ ∃𝑙 ∈
ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
73 | 72 | anbi2i 730 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧)) ∧ ∃𝑖 ∈ ℤ ∃𝑙 ∈ ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)) ↔ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧)) ∧ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))) |
74 | 17, 18, 19, 20, 23, 35, 46, 52, 53, 54, 55, 56, 4, 57, 58, 59, 63, 73 | fourierdlem42 40366 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) |
75 | | unfi 8227 |
. . . . . . . . . 10
⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin) |
76 | 12, 74, 75 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin) |
77 | 8, 76 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Fin) |
78 | | hashnncl 13157 |
. . . . . . . 8
⊢ (𝐻 ∈ Fin →
((#‘𝐻) ∈ ℕ
↔ 𝐻 ≠
∅)) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅)) |
80 | 11, 79 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (#‘𝐻) ∈ ℕ) |
81 | 80 | nnzd 11481 |
. . . . 5
⊢ (𝜑 → (#‘𝐻) ∈ ℤ) |
82 | | fourierdlem54.cd |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 < 𝐷) |
83 | 4, 82 | ltned 10173 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≠ 𝐷) |
84 | | hashprg 13182 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (#‘{𝐶, 𝐷}) = 2)) |
85 | 4, 57, 84 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (#‘{𝐶, 𝐷}) = 2)) |
86 | 83, 85 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (#‘{𝐶, 𝐷}) = 2) |
87 | 86 | eqcomd 2628 |
. . . . . 6
⊢ (𝜑 → 2 = (#‘{𝐶, 𝐷})) |
88 | | ssun1 3776 |
. . . . . . . . 9
⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
89 | 88 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
90 | 89, 8 | syl6sseqr 3652 |
. . . . . . 7
⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻) |
91 | | hashssle 39512 |
. . . . . . 7
⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (#‘{𝐶, 𝐷}) ≤ (#‘𝐻)) |
92 | 77, 90, 91 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (#‘{𝐶, 𝐷}) ≤ (#‘𝐻)) |
93 | 87, 92 | eqbrtrd 4675 |
. . . . 5
⊢ (𝜑 → 2 ≤ (#‘𝐻)) |
94 | | eluz2 11693 |
. . . . 5
⊢
((#‘𝐻) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝐻) ∈ ℤ ∧ 2 ≤
(#‘𝐻))) |
95 | 3, 81, 93, 94 | syl3anbrc 1246 |
. . . 4
⊢ (𝜑 → (#‘𝐻) ∈
(ℤ≥‘2)) |
96 | | uz2m1nn 11763 |
. . . 4
⊢
((#‘𝐻) ∈
(ℤ≥‘2) → ((#‘𝐻) − 1) ∈
ℕ) |
97 | 95, 96 | syl 17 |
. . 3
⊢ (𝜑 → ((#‘𝐻) − 1) ∈
ℕ) |
98 | 1, 97 | syl5eqel 2705 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
99 | | prssg 4350 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ)) |
100 | 4, 57, 99 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ)) |
101 | 4, 57, 100 | mpbi2and 956 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ) |
102 | | ssrab2 3687 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷) |
103 | 4, 57 | iccssred 39727 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ) |
104 | 102, 103 | syl5ss 3614 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ) |
105 | 101, 104 | unssd 3789 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ) |
106 | 8, 105 | syl5eqss 3649 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ⊆ ℝ) |
107 | | fourierdlem54.s |
. . . . . . . . 9
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) |
108 | 77, 106, 107, 1 | fourierdlem36 40360 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
109 | | df-isom 5897 |
. . . . . . . 8
⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))) |
110 | 108, 109 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))) |
111 | 110 | simpld 475 |
. . . . . 6
⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
112 | | f1of 6137 |
. . . . . 6
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)⟶𝐻) |
113 | 111, 112 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻) |
114 | 113, 106 | fssd 6057 |
. . . 4
⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ) |
115 | | reex 10027 |
. . . . 5
⊢ ℝ
∈ V |
116 | | ovex 6678 |
. . . . . 6
⊢
(0...𝑁) ∈
V |
117 | 116 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ∈ V) |
118 | | elmapg 7870 |
. . . . 5
⊢ ((ℝ
∈ V ∧ (0...𝑁)
∈ V) → (𝑆 ∈
(ℝ ↑𝑚 (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ)) |
119 | 115, 117,
118 | sylancr 695 |
. . . 4
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ)) |
120 | 114, 119 | mpbird 247 |
. . 3
⊢ (𝜑 → 𝑆 ∈ (ℝ ↑𝑚
(0...𝑁))) |
121 | | df-f1o 5895 |
. . . . . . . . . . 11
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 ↔ (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻)) |
122 | 111, 121 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻)) |
123 | 122 | simprd 479 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻) |
124 | | dffo3 6374 |
. . . . . . . . 9
⊢ (𝑆:(0...𝑁)–onto→𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))) |
125 | 123, 124 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))) |
126 | 125 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)) |
127 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦))) |
128 | | eqcom 2629 |
. . . . . . . . . 10
⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶) |
129 | 127, 128 | syl6bb 276 |
. . . . . . . . 9
⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)) |
130 | 129 | rexbidv 3052 |
. . . . . . . 8
⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)) |
131 | 130 | rspcv 3305 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)) |
132 | 9, 126, 131 | sylc 65 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶) |
133 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0)) |
134 | 133 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦)) |
135 | 134 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦)) |
136 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶) |
137 | 135, 136 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶) |
138 | 4 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ) |
139 | 137, 138 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ) |
140 | 139, 137 | eqled 10140 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶) |
141 | 140 | 3adantl2 1218 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶) |
142 | 4 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
143 | 57 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
144 | 4, 57, 82 | ltled 10185 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ≤ 𝐷) |
145 | | lbicc2 12288 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝐶
≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷)) |
146 | 142, 143,
144, 145 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷)) |
147 | | ubicc2 12289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝐶
≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷)) |
148 | 142, 143,
144, 147 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷)) |
149 | | prssg 4350 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))) |
150 | 146, 148,
149 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))) |
151 | 146, 148,
150 | mpbi2and 956 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)) |
152 | 102 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)) |
153 | 151, 152 | unssd 3789 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷)) |
154 | 8, 153 | syl5eqss 3649 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷)) |
155 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐻) ∈
ℕ → ((#‘𝐻)
− 1) ∈ ℕ0) |
156 | 80, 155 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((#‘𝐻) − 1) ∈
ℕ0) |
157 | 1, 156 | syl5eqel 2705 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
158 | 157, 40 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
159 | | eluzfz1 12348 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
161 | 113, 160 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘0) ∈ 𝐻) |
162 | 154, 161 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷)) |
163 | 103, 162 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆‘0) ∈ ℝ) |
164 | 163 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ) |
165 | 164 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ) |
166 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ) |
167 | 166 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ) |
168 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ) |
169 | 168 | zred 11482 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ) |
171 | | elfzle1 12344 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦) |
172 | 171 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦) |
173 | | neqne 2802 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑦 = 0 → 𝑦 ≠ 0) |
174 | 173 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0) |
175 | 170, 172,
174 | ne0gt0d 10174 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 < 𝑦) |
176 | 175 | 3ad2antl2 1224 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 0 < 𝑦) |
177 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝜑) |
178 | | simpl2 1065 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ (0...𝑁)) |
179 | 110 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))) |
180 | | breq1 4656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦)) |
181 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0)) |
182 | 181 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦))) |
183 | 180, 182 | bibi12d 335 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))) |
184 | 183 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))) |
185 | 184 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
(0...𝑁) →
(∀𝑥 ∈
(0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))) |
186 | 160, 179,
185 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))) |
187 | 186 | r19.21bi 2932 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))) |
188 | 177, 178,
187 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))) |
189 | 176, 188 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < (𝑆‘𝑦)) |
190 | | simpl3 1066 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶) |
191 | 189, 190 | breqtrd 4679 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶) |
192 | 165, 167,
191 | ltled 10185 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶) |
193 | 141, 192 | pm2.61dan 832 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶) |
194 | 193 | rexlimdv3a 3033 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶)) |
195 | 132, 194 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝑆‘0) ≤ 𝐶) |
196 | | elicc2 12238 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))) |
197 | 4, 57, 196 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))) |
198 | 162, 197 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)) |
199 | 198 | simp2d 1074 |
. . . . 5
⊢ (𝜑 → 𝐶 ≤ (𝑆‘0)) |
200 | 163, 4 | letri3d 10179 |
. . . . 5
⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0)))) |
201 | 195, 199,
200 | mpbir2and 957 |
. . . 4
⊢ (𝜑 → (𝑆‘0) = 𝐶) |
202 | | eluzfz2 12349 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
203 | 158, 202 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
204 | 113, 203 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻) |
205 | 154, 204 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷)) |
206 | | elicc2 12238 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))) |
207 | 4, 57, 206 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))) |
208 | 205, 207 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)) |
209 | 208 | simp3d 1075 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷) |
210 | | prid2g 4296 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷}) |
211 | | elun1 3780 |
. . . . . . . . 9
⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
212 | 57, 210, 211 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
213 | 212, 8 | syl6eleqr 2712 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝐻) |
214 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦))) |
215 | | eqcom 2629 |
. . . . . . . . . 10
⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷) |
216 | 214, 215 | syl6bb 276 |
. . . . . . . . 9
⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)) |
217 | 216 | rexbidv 3052 |
. . . . . . . 8
⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)) |
218 | 217 | rspcv 3305 |
. . . . . . 7
⊢ (𝐷 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)) |
219 | 213, 126,
218 | sylc 65 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷) |
220 | 215 | biimpri 218 |
. . . . . . . . 9
⊢ ((𝑆‘𝑦) = 𝐷 → 𝐷 = (𝑆‘𝑦)) |
221 | 220 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 = (𝑆‘𝑦)) |
222 | 114 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ) |
223 | 103, 205 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ) |
224 | 223 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ) |
225 | 169 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ) |
226 | | elfzel2 12340 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
227 | 226 | zred 11482 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ) |
228 | 227 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) |
229 | | elfzle2 12345 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁) |
230 | 229 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁) |
231 | 225, 228,
230 | lensymd 10188 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦) |
232 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦)) |
233 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁)) |
234 | 233 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦))) |
235 | 232, 234 | bibi12d 335 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))) |
236 | 235 | ralbidv 2986 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))) |
237 | 236 | rspcv 3305 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))) |
238 | 203, 179,
237 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))) |
239 | 238 | r19.21bi 2932 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))) |
240 | 231, 239 | mtbid 314 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦)) |
241 | 222, 224,
240 | nltled 10187 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁)) |
242 | 241 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁)) |
243 | 221, 242 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁)) |
244 | 243 | rexlimdv3a 3033 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁))) |
245 | 219, 244 | mpd 15 |
. . . . 5
⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁)) |
246 | 223, 57 | letri3d 10179 |
. . . . 5
⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁)))) |
247 | 209, 245,
246 | mpbir2and 957 |
. . . 4
⊢ (𝜑 → (𝑆‘𝑁) = 𝐷) |
248 | | elfzoelz 12470 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ) |
249 | 248 | zred 11482 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ) |
250 | 249 | ltp1d 10954 |
. . . . . . 7
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1)) |
251 | 250 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1)) |
252 | 179 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))) |
253 | | elfzofz 12485 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁)) |
254 | 253 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁)) |
255 | | fzofzp1 12565 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁)) |
256 | 255 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁)) |
257 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦)) |
258 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖)) |
259 | 258 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦))) |
260 | 257, 259 | bibi12d 335 |
. . . . . . . . 9
⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))) |
261 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1))) |
262 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1))) |
263 | 262 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))) |
264 | 261, 263 | bibi12d 335 |
. . . . . . . . 9
⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
265 | 260, 264 | rspc2v 3322 |
. . . . . . . 8
⊢ ((𝑖 ∈ (0...𝑁) ∧ (𝑖 + 1) ∈ (0...𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
266 | 254, 256,
265 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
267 | 252, 266 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))) |
268 | 251, 267 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))) |
269 | 268 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))) |
270 | 201, 247,
269 | jca31 557 |
. . 3
⊢ (𝜑 → (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))) |
271 | | fourierdlem54.o |
. . . . 5
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
272 | 271 | fourierdlem2 40326 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
273 | 98, 272 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
274 | 120, 270,
273 | mpbir2and 957 |
. 2
⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁)) |
275 | 98, 274, 108 | jca31 557 |
1
⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) |