Metamath Proof Explorer

Theorem fourierdlem114

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

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