Metamath Proof Explorer

Theorem fourierdlem102

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem102.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem102.t ⊢ 𝑇 = ( 2 · π )
fourierdlem102.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem102.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
fourierdlem102.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
fourierdlem102.gcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
fourierdlem102.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
fourierdlem102.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
fourierdlem102.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem102.p ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem102.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem102.h ⊢ 𝐻 = ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) )
fourierdlem102.m ⊢ 𝑀 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem102.q ⊢ 𝑄 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
Assertion fourierdlem102 ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem102.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem102.t ⊢ 𝑇 = ( 2 · π )
3 fourierdlem102.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4 fourierdlem102.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5 fourierdlem102.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
6 fourierdlem102.gcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
7 fourierdlem102.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
8 fourierdlem102.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
9 fourierdlem102.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10 fourierdlem102.p ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
11 fourierdlem102.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
12 fourierdlem102.h ⊢ 𝐻 = ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) )
13 fourierdlem102.m ⊢ 𝑀 = ( ( ♯ ‘ 𝐻 ) − 1 )
14 fourierdlem102.q ⊢ 𝑄 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
15 2z ⊢ 2 ∈ ℤ
16 15 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
17 tpfi ⊢ { - π , π , ( 𝐸 ‘ 𝑋 ) } ∈ Fin
18 17 a1i ⊢ ( 𝜑 → { - π , π , ( 𝐸 ‘ 𝑋 ) } ∈ Fin )
19 pire ⊢ π ∈ ℝ
20 19 renegcli ⊢ - π ∈ ℝ
21 20 rexri ⊢ - π ∈ ℝ*
22 19 rexri ⊢ π ∈ ℝ*
23 negpilt0 ⊢ - π < 0
24 pipos ⊢ 0 < π
25 0re ⊢ 0 ∈ ℝ
26 20 25 19 lttri ⊢ ( ( - π < 0 ∧ 0 < π ) → - π < π )
27 23 24 26 mp2an ⊢ - π < π
28 20 19 27 ltleii ⊢ - π ≤ π
29 prunioo ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ - π ≤ π ) → ( ( - π (,) π ) ∪ { - π , π } ) = ( - π [,] π ) )
30 21 22 28 29 mp3an ⊢ ( ( - π (,) π ) ∪ { - π , π } ) = ( - π [,] π )
31 30 difeq1i ⊢ ( ( ( - π (,) π ) ∪ { - π , π } ) ∖ dom 𝐺 ) = ( ( - π [,] π ) ∖ dom 𝐺 )
32 difundir ⊢ ( ( ( - π (,) π ) ∪ { - π , π } ) ∖ dom 𝐺 ) = ( ( ( - π (,) π ) ∖ dom 𝐺 ) ∪ ( { - π , π } ∖ dom 𝐺 ) )
33 31 32 eqtr3i ⊢ ( ( - π [,] π ) ∖ dom 𝐺 ) = ( ( ( - π (,) π ) ∖ dom 𝐺 ) ∪ ( { - π , π } ∖ dom 𝐺 ) )
34 prfi ⊢ { - π , π } ∈ Fin
35 diffi ⊢ ( { - π , π } ∈ Fin → ( { - π , π } ∖ dom 𝐺 ) ∈ Fin )
36 34 35 mp1i ⊢ ( 𝜑 → ( { - π , π } ∖ dom 𝐺 ) ∈ Fin )
37 unfi ⊢ ( ( ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin ∧ ( { - π , π } ∖ dom 𝐺 ) ∈ Fin ) → ( ( ( - π (,) π ) ∖ dom 𝐺 ) ∪ ( { - π , π } ∖ dom 𝐺 ) ) ∈ Fin )
38 5 36 37 syl2anc ⊢ ( 𝜑 → ( ( ( - π (,) π ) ∖ dom 𝐺 ) ∪ ( { - π , π } ∖ dom 𝐺 ) ) ∈ Fin )
39 33 38 eqeltrid ⊢ ( 𝜑 → ( ( - π [,] π ) ∖ dom 𝐺 ) ∈ Fin )
40 unfi ⊢ ( ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∈ Fin ∧ ( ( - π [,] π ) ∖ dom 𝐺 ) ∈ Fin ) → ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ∈ Fin )
41 18 39 40 syl2anc ⊢ ( 𝜑 → ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ∈ Fin )
42 12 41 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ Fin )
43 hashcl ⊢ ( 𝐻 ∈ Fin → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
44 42 43 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
45 44 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℤ )
46 20 27 ltneii ⊢ - π ≠ π
47 hashprg ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π ≠ π ↔ ( ♯ ‘ { - π , π } ) = 2 ) )
48 20 19 47 mp2an ⊢ ( - π ≠ π ↔ ( ♯ ‘ { - π , π } ) = 2 )
49 46 48 mpbi ⊢ ( ♯ ‘ { - π , π } ) = 2
50 17 elexi ⊢ { - π , π , ( 𝐸 ‘ 𝑋 ) } ∈ V
51 ovex ⊢ ( - π [,] π ) ∈ V
52 difexg ⊢ ( ( - π [,] π ) ∈ V → ( ( - π [,] π ) ∖ dom 𝐺 ) ∈ V )
53 51 52 ax-mp ⊢ ( ( - π [,] π ) ∖ dom 𝐺 ) ∈ V
54 50 53 unex ⊢ ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ∈ V
55 12 54 eqeltri ⊢ 𝐻 ∈ V
56 negex ⊢ - π ∈ V
57 56 tpid1 ⊢ - π ∈ { - π , π , ( 𝐸 ‘ 𝑋 ) }
58 19 elexi ⊢ π ∈ V
59 58 tpid2 ⊢ π ∈ { - π , π , ( 𝐸 ‘ 𝑋 ) }
60 prssi ⊢ ( ( - π ∈ { - π , π , ( 𝐸 ‘ 𝑋 ) } ∧ π ∈ { - π , π , ( 𝐸 ‘ 𝑋 ) } ) → { - π , π } ⊆ { - π , π , ( 𝐸 ‘ 𝑋 ) } )
61 57 59 60 mp2an ⊢ { - π , π } ⊆ { - π , π , ( 𝐸 ‘ 𝑋 ) }
62 ssun1 ⊢ { - π , π , ( 𝐸 ‘ 𝑋 ) } ⊆ ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) )
63 62 12 sseqtrri ⊢ { - π , π , ( 𝐸 ‘ 𝑋 ) } ⊆ 𝐻
64 61 63 sstri ⊢ { - π , π } ⊆ 𝐻
65 hashss ⊢ ( ( 𝐻 ∈ V ∧ { - π , π } ⊆ 𝐻 ) → ( ♯ ‘ { - π , π } ) ≤ ( ♯ ‘ 𝐻 ) )
66 55 64 65 mp2an ⊢ ( ♯ ‘ { - π , π } ) ≤ ( ♯ ‘ 𝐻 )
67 66 a1i ⊢ ( 𝜑 → ( ♯ ‘ { - π , π } ) ≤ ( ♯ ‘ 𝐻 ) )
68 49 67 eqbrtrrid ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐻 ) )
69 eluz2 ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝐻 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝐻 ) ) )
70 16 45 68 69 syl3anbrc ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ( ℤ≥ ‘ 2 ) )
71 uz2m1nn ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ )
72 70 71 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ )
73 13 72 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
74 20 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
75 19 a1i ⊢ ( 𝜑 → π ∈ ℝ )
76 negpitopissre ⊢ ( - π (,] π ) ⊆ ℝ
77 27 a1i ⊢ ( 𝜑 → - π < π )
78 picn ⊢ π ∈ ℂ
79 78 2timesi ⊢ ( 2 · π ) = ( π + π )
80 78 78 subnegi ⊢ ( π − - π ) = ( π + π )
81 79 2 80 3eqtr4i ⊢ 𝑇 = ( π − - π )
82 74 75 77 81 11 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( - π (,] π ) )
83 82 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( - π (,] π ) )
84 76 83 sselid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ℝ )
85 74 75 84 3jca ⊢ ( 𝜑 → ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝐸 ‘ 𝑋 ) ∈ ℝ ) )
86 fvex ⊢ ( 𝐸 ‘ 𝑋 ) ∈ V
87 56 58 86 tpss ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝐸 ‘ 𝑋 ) ∈ ℝ ) ↔ { - π , π , ( 𝐸 ‘ 𝑋 ) } ⊆ ℝ )
88 85 87 sylib ⊢ ( 𝜑 → { - π , π , ( 𝐸 ‘ 𝑋 ) } ⊆ ℝ )
89 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
90 20 19 89 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
91 ssdifss ⊢ ( ( - π [,] π ) ⊆ ℝ → ( ( - π [,] π ) ∖ dom 𝐺 ) ⊆ ℝ )
92 90 91 mp1i ⊢ ( 𝜑 → ( ( - π [,] π ) ∖ dom 𝐺 ) ⊆ ℝ )
93 88 92 unssd ⊢ ( 𝜑 → ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ⊆ ℝ )
94 12 93 eqsstrid ⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
95 42 94 14 13 fourierdlem36 ⊢ ( 𝜑 → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
96 isof1o ⊢ ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) → 𝑄 : ( 0 ... 𝑀 ) –1-1-onto→ 𝐻 )
97 f1of ⊢ ( 𝑄 : ( 0 ... 𝑀 ) –1-1-onto→ 𝐻 → 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 )
98 95 96 97 3syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 )
99 98 94 fssd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
100 reex ⊢ ℝ ∈ V
101 ovex ⊢ ( 0 ... 𝑀 ) ∈ V
102 100 101 elmap ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ↔ 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
103 99 102 sylibr ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
104 fveq2 ⊢ ( 0 = 𝑖 → ( 𝑄 ‘ 0 ) = ( 𝑄 ‘ 𝑖 ) )
105 104 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 = 𝑖 ) → ( 𝑄 ‘ 0 ) = ( 𝑄 ‘ 𝑖 ) )
106 99 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
107 106 leidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑖 ) )
108 107 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 = 𝑖 ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑖 ) )
109 105 108 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 = 𝑖 ) → ( 𝑄 ‘ 0 ) ≤ ( 𝑄 ‘ 𝑖 ) )
110 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ℤ )
111 110 zred ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ℝ )
112 111 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 0 = 𝑖 ) → 𝑖 ∈ ℝ )
113 elfzle1 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑖 )
114 113 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 0 = 𝑖 ) → 0 ≤ 𝑖 )
115 neqne ⊢ ( ¬ 0 = 𝑖 → 0 ≠ 𝑖 )
116 115 necomd ⊢ ( ¬ 0 = 𝑖 → 𝑖 ≠ 0 )
117 116 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 0 = 𝑖 ) → 𝑖 ≠ 0 )
118 112 114 117 ne0gt0d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 0 = 𝑖 ) → 0 < 𝑖 )
119 nnssnn0 ⊢ ℕ ⊆ ℕ0
120 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
121 119 120 sseqtri ⊢ ℕ ⊆ ( ℤ≥ ‘ 0 )
122 121 73 sselid ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
123 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
124 122 123 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
125 98 124 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ 𝐻 )
126 94 125 sseldd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
127 126 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
128 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
129 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → 0 < 𝑖 )
130 95 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
131 124 anim1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 0 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → ( 0 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) )
133 isorel ⊢ ( ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) ∧ ( 0 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ) → ( 0 < 𝑖 ↔ ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ 𝑖 ) ) )
134 130 132 133 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → ( 0 < 𝑖 ↔ ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ 𝑖 ) ) )
135 129 134 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ 𝑖 ) )
136 127 128 135 ltled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 0 < 𝑖 ) → ( 𝑄 ‘ 0 ) ≤ ( 𝑄 ‘ 𝑖 ) )
137 118 136 syldan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 0 = 𝑖 ) → ( 𝑄 ‘ 0 ) ≤ ( 𝑄 ‘ 𝑖 ) )
138 109 137 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 0 ) ≤ ( 𝑄 ‘ 𝑖 ) )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → ( 𝑄 ‘ 0 ) ≤ ( 𝑄 ‘ 𝑖 ) )
140 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → ( 𝑄 ‘ 𝑖 ) = - π )
141 139 140 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → ( 𝑄 ‘ 0 ) ≤ - π )
142 74 rexrd ⊢ ( 𝜑 → - π ∈ ℝ* )
143 75 rexrd ⊢ ( 𝜑 → π ∈ ℝ* )
144 lbicc2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ - π ≤ π ) → - π ∈ ( - π [,] π ) )
145 21 22 28 144 mp3an ⊢ - π ∈ ( - π [,] π )
146 145 a1i ⊢ ( 𝜑 → - π ∈ ( - π [,] π ) )
147 ubicc2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ - π ≤ π ) → π ∈ ( - π [,] π ) )
148 21 22 28 147 mp3an ⊢ π ∈ ( - π [,] π )
149 148 a1i ⊢ ( 𝜑 → π ∈ ( - π [,] π ) )
150 iocssicc ⊢ ( - π (,] π ) ⊆ ( - π [,] π )
151 150 83 sselid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( - π [,] π ) )
152 tpssi ⊢ ( ( - π ∈ ( - π [,] π ) ∧ π ∈ ( - π [,] π ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( - π [,] π ) ) → { - π , π , ( 𝐸 ‘ 𝑋 ) } ⊆ ( - π [,] π ) )
153 146 149 151 152 syl3anc ⊢ ( 𝜑 → { - π , π , ( 𝐸 ‘ 𝑋 ) } ⊆ ( - π [,] π ) )
154 difssd ⊢ ( 𝜑 → ( ( - π [,] π ) ∖ dom 𝐺 ) ⊆ ( - π [,] π ) )
155 153 154 unssd ⊢ ( 𝜑 → ( { - π , π , ( 𝐸 ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ⊆ ( - π [,] π ) )
156 12 155 eqsstrid ⊢ ( 𝜑 → 𝐻 ⊆ ( - π [,] π ) )
157 156 125 sseldd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ( - π [,] π ) )
158 iccgelb ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ ( 𝑄 ‘ 0 ) ∈ ( - π [,] π ) ) → - π ≤ ( 𝑄 ‘ 0 ) )
159 142 143 157 158 syl3anc ⊢ ( 𝜑 → - π ≤ ( 𝑄 ‘ 0 ) )
160 159 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → - π ≤ ( 𝑄 ‘ 0 ) )
161 126 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
162 20 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → - π ∈ ℝ )
163 161 162 letri3d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → ( ( 𝑄 ‘ 0 ) = - π ↔ ( ( 𝑄 ‘ 0 ) ≤ - π ∧ - π ≤ ( 𝑄 ‘ 0 ) ) ) )
164 141 160 163 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = - π ) → ( 𝑄 ‘ 0 ) = - π )
165 63 57 sselii ⊢ - π ∈ 𝐻
166 f1ofo ⊢ ( 𝑄 : ( 0 ... 𝑀 ) –1-1-onto→ 𝐻 → 𝑄 : ( 0 ... 𝑀 ) –onto→ 𝐻 )
167 96 166 syl ⊢ ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) → 𝑄 : ( 0 ... 𝑀 ) –onto→ 𝐻 )
168 forn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) –onto→ 𝐻 → ran 𝑄 = 𝐻 )
169 95 167 168 3syl ⊢ ( 𝜑 → ran 𝑄 = 𝐻 )
170 165 169 eleqtrrid ⊢ ( 𝜑 → - π ∈ ran 𝑄 )
171 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 → 𝑄 Fn ( 0 ... 𝑀 ) )
172 fvelrnb ⊢ ( 𝑄 Fn ( 0 ... 𝑀 ) → ( - π ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = - π ) )
173 98 171 172 3syl ⊢ ( 𝜑 → ( - π ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = - π ) )
174 170 173 mpbid ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = - π )
175 164 174 r19.29a ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = - π )
176 63 59 sselii ⊢ π ∈ 𝐻
177 176 169 eleqtrrid ⊢ ( 𝜑 → π ∈ ran 𝑄 )
178 fvelrnb ⊢ ( 𝑄 Fn ( 0 ... 𝑀 ) → ( π ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = π ) )
179 98 171 178 3syl ⊢ ( 𝜑 → ( π ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = π ) )
180 177 179 mpbid ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = π )
181 98 156 fssd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
182 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
183 122 182 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
184 181 183 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( - π [,] π ) )
185 iccleub ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ ( 𝑄 ‘ 𝑀 ) ∈ ( - π [,] π ) ) → ( 𝑄 ‘ 𝑀 ) ≤ π )
186 142 143 184 185 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ≤ π )
187 186 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → ( 𝑄 ‘ 𝑀 ) ≤ π )
188 id ⊢ ( ( 𝑄 ‘ 𝑖 ) = π → ( 𝑄 ‘ 𝑖 ) = π )
189 188 eqcomd ⊢ ( ( 𝑄 ‘ 𝑖 ) = π → π = ( 𝑄 ‘ 𝑖 ) )
190 189 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → π = ( 𝑄 ‘ 𝑖 ) )
191 107 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 = 𝑀 ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑖 ) )
192 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑀 ) )
193 192 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 = 𝑀 ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑀 ) )
194 191 193 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 = 𝑀 ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑀 ) )
195 111 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑀 ) → 𝑖 ∈ ℝ )
196 elfzel2 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
197 196 zred ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℝ )
198 197 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑀 ) → 𝑀 ∈ ℝ )
199 elfzle2 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ≤ 𝑀 )
200 199 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑀 ) → 𝑖 ≤ 𝑀 )
201 neqne ⊢ ( ¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀 )
202 201 necomd ⊢ ( ¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖 )
203 202 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑀 ) → 𝑀 ≠ 𝑖 )
204 195 198 200 203 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑀 ) → 𝑖 < 𝑀 )
205 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
206 90 184 sselid ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
207 206 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
208 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → 𝑖 < 𝑀 )
209 95 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
210 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
211 183 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
212 210 211 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) )
213 212 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) )
214 isorel ⊢ ( ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) ∧ ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) ) → ( 𝑖 < 𝑀 ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ 𝑀 ) ) )
215 209 213 214 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → ( 𝑖 < 𝑀 ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ 𝑀 ) ) )
216 208 215 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ 𝑀 ) )
217 205 207 216 ltled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑀 ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑀 ) )
218 204 217 syldan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑀 ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑀 ) )
219 194 218 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑀 ) )
220 219 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑀 ) )
221 190 220 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → π ≤ ( 𝑄 ‘ 𝑀 ) )
222 206 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
223 19 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → π ∈ ℝ )
224 222 223 letri3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → ( ( 𝑄 ‘ 𝑀 ) = π ↔ ( ( 𝑄 ‘ 𝑀 ) ≤ π ∧ π ≤ ( 𝑄 ‘ 𝑀 ) ) ) )
225 187 221 224 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑖 ) = π ) → ( 𝑄 ‘ 𝑀 ) = π )
226 225 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = π → ( 𝑄 ‘ 𝑀 ) = π ) )
227 180 226 mpd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = π )
228 elfzoelz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ℤ )
229 228 zred ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ℝ )
230 229 ltp1d ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 < ( 𝑖 + 1 ) )
231 230 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 < ( 𝑖 + 1 ) )
232 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
233 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
234 232 233 jca ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
235 isorel ⊢ ( ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) ∧ ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
236 95 234 235 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
237 231 236 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
238 237 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
239 175 227 238 jca31 ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
240 10 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
241 73 240 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
242 103 239 241 mpbir2and ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
243 4 reseq1i ⊢ ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
244 21 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
245 22 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
246 181 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
247 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
248 244 245 246 247 fourierdlem27 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π (,) π ) )
249 248 resabs1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
250 243 249 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
251 6 10 73 242 12 169 fourierdlem38 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
252 250 251 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
253 250 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
254 6 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
255 7 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
256 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
257 95 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
258 257 96 97 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 )
259 84 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐸 ‘ 𝑋 ) ∈ ℝ )
260 257 167 168 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ran 𝑄 = 𝐻 )
261 254 255 256 257 258 247 237 248 259 12 260 fourierdlem46 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ ∧ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ ) )
262 261 simpld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
263 253 262 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
264 250 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
265 261 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
266 264 265 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
267 1 2 3 9 10 73 242 252 263 266 fourierdlem94 ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ ) )