Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem54.t |
⊢ 𝑇 = ( 𝐵 − 𝐴 ) |
2 |
|
fourierdlem54.p |
⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) |
3 |
|
fourierdlem54.m |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
4 |
|
fourierdlem54.q |
⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ) |
5 |
|
fourierdlem54.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
6 |
|
fourierdlem54.d |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
7 |
|
fourierdlem54.cd |
⊢ ( 𝜑 → 𝐶 < 𝐷 ) |
8 |
|
fourierdlem54.o |
⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) |
9 |
|
fourierdlem54.h |
⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) |
10 |
|
fourierdlem54.n |
⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 ) |
11 |
|
fourierdlem54.s |
⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) |
12 |
|
2z |
⊢ 2 ∈ ℤ |
13 |
12
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℤ ) |
14 |
|
prid1g |
⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ { 𝐶 , 𝐷 } ) |
15 |
|
elun1 |
⊢ ( 𝐶 ∈ { 𝐶 , 𝐷 } → 𝐶 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) |
16 |
5 14 15
|
3syl |
⊢ ( 𝜑 → 𝐶 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) |
17 |
16 9
|
eleqtrrdi |
⊢ ( 𝜑 → 𝐶 ∈ 𝐻 ) |
18 |
17
|
ne0d |
⊢ ( 𝜑 → 𝐻 ≠ ∅ ) |
19 |
|
prfi |
⊢ { 𝐶 , 𝐷 } ∈ Fin |
20 |
2 3 4
|
fourierdlem11 |
⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ) |
21 |
20
|
simp1d |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
22 |
20
|
simp2d |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
23 |
20
|
simp3d |
⊢ ( 𝜑 → 𝐴 < 𝐵 ) |
24 |
2 3 4
|
fourierdlem15 |
⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) ) |
25 |
|
frn |
⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) ) |
26 |
24 25
|
syl |
⊢ ( 𝜑 → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) ) |
27 |
2
|
fourierdlem2 |
⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ) |
28 |
3 27
|
syl |
⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ) |
29 |
4 28
|
mpbid |
⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) |
30 |
29
|
simpld |
⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ) |
31 |
|
elmapi |
⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ) |
32 |
|
ffn |
⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) ) |
33 |
30 31 32
|
3syl |
⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) ) |
34 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin ) |
35 |
|
fnfi |
⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ ( 0 ... 𝑀 ) ∈ Fin ) → 𝑄 ∈ Fin ) |
36 |
33 34 35
|
syl2anc |
⊢ ( 𝜑 → 𝑄 ∈ Fin ) |
37 |
|
rnfi |
⊢ ( 𝑄 ∈ Fin → ran 𝑄 ∈ Fin ) |
38 |
36 37
|
syl |
⊢ ( 𝜑 → ran 𝑄 ∈ Fin ) |
39 |
29
|
simprd |
⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
40 |
39
|
simpld |
⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ) |
41 |
40
|
simpld |
⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 ) |
42 |
3
|
nnnn0d |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
43 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
44 |
42 43
|
eleqtrdi |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) ) |
45 |
|
eluzfz1 |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) ) |
46 |
44 45
|
syl |
⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) ) |
47 |
|
fnfvelrn |
⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 0 ) ∈ ran 𝑄 ) |
48 |
33 46 47
|
syl2anc |
⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ran 𝑄 ) |
49 |
41 48
|
eqeltrrd |
⊢ ( 𝜑 → 𝐴 ∈ ran 𝑄 ) |
50 |
40
|
simprd |
⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 ) |
51 |
|
eluzfz2 |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) ) |
52 |
44 51
|
syl |
⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) ) |
53 |
|
fnfvelrn |
⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 ) |
54 |
33 52 53
|
syl2anc |
⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 ) |
55 |
50 54
|
eqeltrrd |
⊢ ( 𝜑 → 𝐵 ∈ ran 𝑄 ) |
56 |
|
eqid |
⊢ ( abs ∘ − ) = ( abs ∘ − ) |
57 |
|
eqid |
⊢ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) = ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) |
58 |
|
eqid |
⊢ ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) = ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) |
59 |
|
eqid |
⊢ inf ( ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) , ℝ , < ) = inf ( ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) , ℝ , < ) |
60 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
61 |
|
eqid |
⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 [,] 𝐷 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 [,] 𝐷 ) ) |
62 |
|
oveq1 |
⊢ ( 𝑥 = 𝑤 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑤 + ( 𝑘 · 𝑇 ) ) ) |
63 |
62
|
eleq1d |
⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) |
64 |
63
|
rexbidv |
⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) |
65 |
64
|
cbvrabv |
⊢ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } |
66 |
|
oveq1 |
⊢ ( 𝑖 = 𝑗 → ( 𝑖 · 𝑇 ) = ( 𝑗 · 𝑇 ) ) |
67 |
66
|
oveq2d |
⊢ ( 𝑖 = 𝑗 → ( 𝑦 + ( 𝑖 · 𝑇 ) ) = ( 𝑦 + ( 𝑗 · 𝑇 ) ) ) |
68 |
67
|
eleq1d |
⊢ ( 𝑖 = 𝑗 → ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) ) |
69 |
68
|
anbi1d |
⊢ ( 𝑖 = 𝑗 → ( ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ) ) |
70 |
|
oveq1 |
⊢ ( 𝑙 = 𝑘 → ( 𝑙 · 𝑇 ) = ( 𝑘 · 𝑇 ) ) |
71 |
70
|
oveq2d |
⊢ ( 𝑙 = 𝑘 → ( 𝑧 + ( 𝑙 · 𝑇 ) ) = ( 𝑧 + ( 𝑘 · 𝑇 ) ) ) |
72 |
71
|
eleq1d |
⊢ ( 𝑙 = 𝑘 → ( ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) |
73 |
72
|
anbi2d |
⊢ ( 𝑙 = 𝑘 → ( ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) ) |
74 |
69 73
|
cbvrex2vw |
⊢ ( ∃ 𝑖 ∈ ℤ ∃ 𝑙 ∈ ℤ ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ ∃ 𝑗 ∈ ℤ ∃ 𝑘 ∈ ℤ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) |
75 |
74
|
anbi2i |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧 ) ) ∧ ∃ 𝑖 ∈ ℤ ∃ 𝑙 ∈ ℤ ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧 ) ) ∧ ∃ 𝑗 ∈ ℤ ∃ 𝑘 ∈ ℤ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) ) |
76 |
21 22 23 1 26 38 49 55 56 57 58 59 5 6 60 61 65 75
|
fourierdlem42 |
⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ∈ Fin ) |
77 |
|
unfi |
⊢ ( ( { 𝐶 , 𝐷 } ∈ Fin ∧ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ∈ Fin ) → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ∈ Fin ) |
78 |
19 76 77
|
sylancr |
⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ∈ Fin ) |
79 |
9 78
|
eqeltrid |
⊢ ( 𝜑 → 𝐻 ∈ Fin ) |
80 |
|
hashnncl |
⊢ ( 𝐻 ∈ Fin → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) ) |
81 |
79 80
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) ) |
82 |
18 81
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ ) |
83 |
82
|
nnzd |
⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℤ ) |
84 |
5 7
|
ltned |
⊢ ( 𝜑 → 𝐶 ≠ 𝐷 ) |
85 |
|
hashprg |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 ≠ 𝐷 ↔ ( ♯ ‘ { 𝐶 , 𝐷 } ) = 2 ) ) |
86 |
5 6 85
|
syl2anc |
⊢ ( 𝜑 → ( 𝐶 ≠ 𝐷 ↔ ( ♯ ‘ { 𝐶 , 𝐷 } ) = 2 ) ) |
87 |
84 86
|
mpbid |
⊢ ( 𝜑 → ( ♯ ‘ { 𝐶 , 𝐷 } ) = 2 ) |
88 |
87
|
eqcomd |
⊢ ( 𝜑 → 2 = ( ♯ ‘ { 𝐶 , 𝐷 } ) ) |
89 |
|
ssun1 |
⊢ { 𝐶 , 𝐷 } ⊆ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) |
90 |
89
|
a1i |
⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) |
91 |
90 9
|
sseqtrrdi |
⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ 𝐻 ) |
92 |
|
hashssle |
⊢ ( ( 𝐻 ∈ Fin ∧ { 𝐶 , 𝐷 } ⊆ 𝐻 ) → ( ♯ ‘ { 𝐶 , 𝐷 } ) ≤ ( ♯ ‘ 𝐻 ) ) |
93 |
79 91 92
|
syl2anc |
⊢ ( 𝜑 → ( ♯ ‘ { 𝐶 , 𝐷 } ) ≤ ( ♯ ‘ 𝐻 ) ) |
94 |
88 93
|
eqbrtrd |
⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐻 ) ) |
95 |
|
eluz2 |
⊢ ( ( ♯ ‘ 𝐻 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝐻 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝐻 ) ) ) |
96 |
13 83 94 95
|
syl3anbrc |
⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ( ℤ≥ ‘ 2 ) ) |
97 |
|
uz2m1nn |
⊢ ( ( ♯ ‘ 𝐻 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ ) |
98 |
96 97
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ ) |
99 |
10 98
|
eqeltrid |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
100 |
|
prssg |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ↔ { 𝐶 , 𝐷 } ⊆ ℝ ) ) |
101 |
5 6 100
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ↔ { 𝐶 , 𝐷 } ⊆ ℝ ) ) |
102 |
5 6 101
|
mpbi2and |
⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ℝ ) |
103 |
|
ssrab2 |
⊢ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ( 𝐶 [,] 𝐷 ) |
104 |
5 6
|
iccssred |
⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ ) |
105 |
103 104
|
sstrid |
⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ℝ ) |
106 |
102 105
|
unssd |
⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ⊆ ℝ ) |
107 |
9 106
|
eqsstrid |
⊢ ( 𝜑 → 𝐻 ⊆ ℝ ) |
108 |
79 107 11 10
|
fourierdlem36 |
⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) |
109 |
|
df-isom |
⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
110 |
108 109
|
sylib |
⊢ ( 𝜑 → ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
111 |
110
|
simpld |
⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ) |
112 |
|
f1of |
⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 ) |
113 |
111 112
|
syl |
⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 ) |
114 |
113 107
|
fssd |
⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ ) |
115 |
|
reex |
⊢ ℝ ∈ V |
116 |
|
ovex |
⊢ ( 0 ... 𝑁 ) ∈ V |
117 |
116
|
a1i |
⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V ) |
118 |
|
elmapg |
⊢ ( ( ℝ ∈ V ∧ ( 0 ... 𝑁 ) ∈ V ) → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ↔ 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ ) ) |
119 |
115 117 118
|
sylancr |
⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ↔ 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ ) ) |
120 |
114 119
|
mpbird |
⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ) |
121 |
|
df-f1o |
⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ↔ ( 𝑆 : ( 0 ... 𝑁 ) –1-1→ 𝐻 ∧ 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ) ) |
122 |
111 121
|
sylib |
⊢ ( 𝜑 → ( 𝑆 : ( 0 ... 𝑁 ) –1-1→ 𝐻 ∧ 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ) ) |
123 |
122
|
simprd |
⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ) |
124 |
|
dffo3 |
⊢ ( 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ↔ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 ∧ ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ) ) |
125 |
123 124
|
sylib |
⊢ ( 𝜑 → ( 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 ∧ ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ) ) |
126 |
125
|
simprd |
⊢ ( 𝜑 → ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ) |
127 |
|
eqeq1 |
⊢ ( ℎ = 𝐶 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ 𝐶 = ( 𝑆 ‘ 𝑦 ) ) ) |
128 |
|
eqcom |
⊢ ( 𝐶 = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) |
129 |
127 128
|
bitrdi |
⊢ ( ℎ = 𝐶 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ) |
130 |
129
|
rexbidv |
⊢ ( ℎ = 𝐶 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ) |
131 |
130
|
rspcv |
⊢ ( 𝐶 ∈ 𝐻 → ( ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ) |
132 |
17 126 131
|
sylc |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 ) |
133 |
|
fveq2 |
⊢ ( 𝑦 = 0 → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 0 ) ) |
134 |
133
|
eqcomd |
⊢ ( 𝑦 = 0 → ( 𝑆 ‘ 0 ) = ( 𝑆 ‘ 𝑦 ) ) |
135 |
134
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) = ( 𝑆 ‘ 𝑦 ) ) |
136 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 𝑦 ) = 𝐶 ) |
137 |
135 136
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) = 𝐶 ) |
138 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → 𝐶 ∈ ℝ ) |
139 |
137 138
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ∈ ℝ ) |
140 |
139 137
|
eqled |
⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) |
141 |
140
|
3adantl2 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) |
142 |
5
|
rexrd |
⊢ ( 𝜑 → 𝐶 ∈ ℝ* ) |
143 |
6
|
rexrd |
⊢ ( 𝜑 → 𝐷 ∈ ℝ* ) |
144 |
5 6 7
|
ltled |
⊢ ( 𝜑 → 𝐶 ≤ 𝐷 ) |
145 |
|
lbicc2 |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 ≤ 𝐷 ) → 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ) |
146 |
142 143 144 145
|
syl3anc |
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ) |
147 |
|
ubicc2 |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 ≤ 𝐷 ) → 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) |
148 |
142 143 144 147
|
syl3anc |
⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) |
149 |
|
prssg |
⊢ ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) → ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) ↔ { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) ) |
150 |
146 148 149
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) ↔ { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) ) |
151 |
146 148 150
|
mpbi2and |
⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) |
152 |
103
|
a1i |
⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ( 𝐶 [,] 𝐷 ) ) |
153 |
151 152
|
unssd |
⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ⊆ ( 𝐶 [,] 𝐷 ) ) |
154 |
9 153
|
eqsstrid |
⊢ ( 𝜑 → 𝐻 ⊆ ( 𝐶 [,] 𝐷 ) ) |
155 |
|
nnm1nn0 |
⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 ) |
156 |
82 155
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 ) |
157 |
10 156
|
eqeltrid |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
158 |
157 43
|
eleqtrdi |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) |
159 |
|
eluzfz1 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑁 ) ) |
160 |
158 159
|
syl |
⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) ) |
161 |
113 160
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ 𝐻 ) |
162 |
154 161
|
sseldd |
⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ( 𝐶 [,] 𝐷 ) ) |
163 |
104 162
|
sseldd |
⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ℝ ) |
164 |
163
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ∈ ℝ ) |
165 |
164
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ∈ ℝ ) |
166 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ 𝑦 = 0 ) → 𝐶 ∈ ℝ ) |
167 |
166
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 𝐶 ∈ ℝ ) |
168 |
|
elfzelz |
⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑦 ∈ ℤ ) |
169 |
168
|
zred |
⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑦 ∈ ℝ ) |
170 |
169
|
adantr |
⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 𝑦 ∈ ℝ ) |
171 |
|
elfzle1 |
⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑦 ) |
172 |
171
|
adantr |
⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 0 ≤ 𝑦 ) |
173 |
|
neqne |
⊢ ( ¬ 𝑦 = 0 → 𝑦 ≠ 0 ) |
174 |
173
|
adantl |
⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 𝑦 ≠ 0 ) |
175 |
170 172 174
|
ne0gt0d |
⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 0 < 𝑦 ) |
176 |
175
|
3ad2antl2 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 0 < 𝑦 ) |
177 |
|
simpl1 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 𝜑 ) |
178 |
|
simpl2 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 𝑦 ∈ ( 0 ... 𝑁 ) ) |
179 |
110
|
simprd |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
180 |
|
breq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 < 𝑦 ↔ 0 < 𝑦 ) ) |
181 |
|
fveq2 |
⊢ ( 𝑥 = 0 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 0 ) ) |
182 |
181
|
breq1d |
⊢ ( 𝑥 = 0 → ( ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
183 |
180 182
|
bibi12d |
⊢ ( 𝑥 = 0 → ( ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
184 |
183
|
ralbidv |
⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
185 |
184
|
rspcv |
⊢ ( 0 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
186 |
160 179 185
|
sylc |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
187 |
186
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
188 |
177 178 187
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
189 |
176 188
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) |
190 |
|
simpl3 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 𝑦 ) = 𝐶 ) |
191 |
189 190
|
breqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) < 𝐶 ) |
192 |
165 167 191
|
ltled |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) |
193 |
141 192
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) |
194 |
193
|
rexlimdv3a |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) ) |
195 |
132 194
|
mpd |
⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) |
196 |
|
elicc2 |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ 0 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 0 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ∧ ( 𝑆 ‘ 0 ) ≤ 𝐷 ) ) ) |
197 |
5 6 196
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 0 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ∧ ( 𝑆 ‘ 0 ) ≤ 𝐷 ) ) ) |
198 |
162 197
|
mpbid |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ∧ ( 𝑆 ‘ 0 ) ≤ 𝐷 ) ) |
199 |
198
|
simp2d |
⊢ ( 𝜑 → 𝐶 ≤ ( 𝑆 ‘ 0 ) ) |
200 |
163 5
|
letri3d |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) = 𝐶 ↔ ( ( 𝑆 ‘ 0 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ) ) ) |
201 |
195 199 200
|
mpbir2and |
⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = 𝐶 ) |
202 |
|
eluzfz2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) ) |
203 |
158 202
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) ) |
204 |
113 203
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ 𝐻 ) |
205 |
154 204
|
sseldd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐶 [,] 𝐷 ) ) |
206 |
|
elicc2 |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑁 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) ) ) |
207 |
5 6 206
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑁 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) ) ) |
208 |
205 207
|
mpbid |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) ) |
209 |
208
|
simp3d |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) |
210 |
|
prid2g |
⊢ ( 𝐷 ∈ ℝ → 𝐷 ∈ { 𝐶 , 𝐷 } ) |
211 |
|
elun1 |
⊢ ( 𝐷 ∈ { 𝐶 , 𝐷 } → 𝐷 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) |
212 |
6 210 211
|
3syl |
⊢ ( 𝜑 → 𝐷 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) |
213 |
212 9
|
eleqtrrdi |
⊢ ( 𝜑 → 𝐷 ∈ 𝐻 ) |
214 |
|
eqeq1 |
⊢ ( ℎ = 𝐷 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ 𝐷 = ( 𝑆 ‘ 𝑦 ) ) ) |
215 |
|
eqcom |
⊢ ( 𝐷 = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) |
216 |
214 215
|
bitrdi |
⊢ ( ℎ = 𝐷 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) ) |
217 |
216
|
rexbidv |
⊢ ( ℎ = 𝐷 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 ) ) |
218 |
217
|
rspcv |
⊢ ( 𝐷 ∈ 𝐻 → ( ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 ) ) |
219 |
213 126 218
|
sylc |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 ) |
220 |
215
|
biimpri |
⊢ ( ( 𝑆 ‘ 𝑦 ) = 𝐷 → 𝐷 = ( 𝑆 ‘ 𝑦 ) ) |
221 |
220
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) → 𝐷 = ( 𝑆 ‘ 𝑦 ) ) |
222 |
114
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑦 ) ∈ ℝ ) |
223 |
104 205
|
sseldd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ ℝ ) |
224 |
223
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑁 ) ∈ ℝ ) |
225 |
169
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → 𝑦 ∈ ℝ ) |
226 |
|
elfzel2 |
⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ ) |
227 |
226
|
zred |
⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ ) |
228 |
227
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ ) |
229 |
|
elfzle2 |
⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑦 ≤ 𝑁 ) |
230 |
229
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → 𝑦 ≤ 𝑁 ) |
231 |
225 228 230
|
lensymd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝑁 < 𝑦 ) |
232 |
|
breq1 |
⊢ ( 𝑥 = 𝑁 → ( 𝑥 < 𝑦 ↔ 𝑁 < 𝑦 ) ) |
233 |
|
fveq2 |
⊢ ( 𝑥 = 𝑁 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑁 ) ) |
234 |
233
|
breq1d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
235 |
232 234
|
bibi12d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
236 |
235
|
ralbidv |
⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
237 |
236
|
rspcv |
⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
238 |
203 179 237
|
sylc |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
239 |
238
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
240 |
231 239
|
mtbid |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) |
241 |
222 224 240
|
nltled |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑦 ) ≤ ( 𝑆 ‘ 𝑁 ) ) |
242 |
241
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) → ( 𝑆 ‘ 𝑦 ) ≤ ( 𝑆 ‘ 𝑁 ) ) |
243 |
221 242
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) → 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) ) |
244 |
243
|
rexlimdv3a |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 → 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) ) ) |
245 |
219 244
|
mpd |
⊢ ( 𝜑 → 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) ) |
246 |
223 6
|
letri3d |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) = 𝐷 ↔ ( ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ∧ 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) ) ) ) |
247 |
209 245 246
|
mpbir2and |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) = 𝐷 ) |
248 |
|
elfzoelz |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℤ ) |
249 |
248
|
zred |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℝ ) |
250 |
249
|
ltp1d |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 < ( 𝑖 + 1 ) ) |
251 |
250
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 < ( 𝑖 + 1 ) ) |
252 |
179
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
253 |
|
elfzofz |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ... 𝑁 ) ) |
254 |
253
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) ) |
255 |
|
fzofzp1 |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) |
256 |
255
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) |
257 |
|
breq1 |
⊢ ( 𝑥 = 𝑖 → ( 𝑥 < 𝑦 ↔ 𝑖 < 𝑦 ) ) |
258 |
|
fveq2 |
⊢ ( 𝑥 = 𝑖 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑖 ) ) |
259 |
258
|
breq1d |
⊢ ( 𝑥 = 𝑖 → ( ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ) ) |
260 |
257 259
|
bibi12d |
⊢ ( 𝑥 = 𝑖 → ( ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑖 < 𝑦 ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ) ) ) |
261 |
|
breq2 |
⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( 𝑖 < 𝑦 ↔ 𝑖 < ( 𝑖 + 1 ) ) ) |
262 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) |
263 |
262
|
breq2d |
⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) |
264 |
261 263
|
bibi12d |
⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( ( 𝑖 < 𝑦 ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) |
265 |
260 264
|
rspc2v |
⊢ ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) |
266 |
254 256 265
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) |
267 |
252 266
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) |
268 |
251 267
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) |
269 |
268
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) |
270 |
201 247 269
|
jca31 |
⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) |
271 |
8
|
fourierdlem2 |
⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) ) |
272 |
99 271
|
syl |
⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) ) |
273 |
120 270 272
|
mpbir2and |
⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) |
274 |
99 273 108
|
jca31 |
⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) ) |