Metamath Proof Explorer

Theorem fourierdlem54

Description: Given a partition Q and an arbitrary interval [ C , D ] , a partition S on [ C , D ] is built such that it preserves any periodic function piecewise continuous on Q will be piecewise continuous on S , with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem54.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem54.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem54.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem54.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem54.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem54.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem54.cd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
fourierdlem54.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem54.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
fourierdlem54.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem54.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
Assertion fourierdlem54 ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )

Proof

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 ... 𝑁 ) , 𝐻 ) ) )