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 → ( ♯ ‘ 𝐻 ) ∈ ℕ₀ )
44	42 43	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ₀ )
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	⊢ ℕ ⊆ ℕ₀
120		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 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_ℂ 𝑋 ) ≠ ∅ ) )

Metamath Proof Explorer

Theorem fourierdlem102

Proof