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	⊢ 𝐴 = ( 𝑛 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( 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	⊢ 𝐴 = ( 𝑛 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( 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 → ( ♯ ‘ 𝐻 ) ∈ ℕ₀ )
49	47 48	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ₀ )
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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( - π (,] π ) )
89	81 88	sselid	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ℝ )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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	⊢ ℕ ⊆ ℕ₀
125		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
126	124 125	sseqtri	⊢ ℕ ⊆ ( ℤ_≥ ‘ 0 )
127	126 78	sselid	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ 0 ) )
128		eluzfz1	⊢ ( 𝑀 ∈ ( ℤ_≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
129	127 128	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
130	103 129	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 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	sselid	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( - π [,] π ) )
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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( - π [,] π ) )
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	sselid	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
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	eqtr2id	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ) ) )

Metamath Proof Explorer

Theorem fourierdlem114

Proof