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