Theorem fourierdlem97

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem97.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem97.g	⊢ 𝐺 = ( ℝ D 𝐹 )
	fourierdlem97.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem97.a	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem97.b	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem97.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem97.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem97.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem97.fper	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
	fourierdlem97.qcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem97.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	fourierdlem97.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
	fourierdlem97.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) )
	fourierdlem97.v	⊢ 𝑉 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
	fourierdlem97.h	⊢ 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
Assertion	fourierdlem97	⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem97.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem97.g	⊢ 𝐺 = ( ℝ D 𝐹 )
3		fourierdlem97.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4		fourierdlem97.a	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		fourierdlem97.b	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6		fourierdlem97.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
7		fourierdlem97.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
8		fourierdlem97.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
9		fourierdlem97.fper	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
10		fourierdlem97.qcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11		fourierdlem97.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12		fourierdlem97.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
13		fourierdlem97.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) )
14		fourierdlem97.v	⊢ 𝑉 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
15		fourierdlem97.h	⊢ 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
16		ioossre	⊢ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ
17	16	a1i	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ )
18	17	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
19		iftrue	⊢ ( 𝑠 ∈ dom 𝐺 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
21		ssid	⊢ ℝ ⊆ ℝ
22		dvfre	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
23	1 21 22	sylancl	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
24	2	feq1i	⊢ ( 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
25	23 24	sylibr	⊢ ( 𝜑 → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ )
27		id	⊢ ( 𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom 𝐺 )
28	2	dmeqi	⊢ dom 𝐺 = dom ( ℝ D 𝐹 )
29	27 28	eleqtrdi	⊢ ( 𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom ( ℝ D 𝐹 ) )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → 𝑠 ∈ dom ( ℝ D 𝐹 ) )
31	26 30	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
32	20 31	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
34		iffalse	⊢ ( ¬ 𝑠 ∈ dom 𝐺 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = 0 )
35		0red	⊢ ( ¬ 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ )
36	34 35	eqeltrd	⊢ ( ¬ 𝑠 ∈ dom 𝐺 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
37	36	adantl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
38	33 37	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
39	18 38	syldan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
40	15	fvmpt2	⊢ ( ( 𝑠 ∈ ℝ ∧ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
41	18 39 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
42		elioore	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
43	12 42	syl	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
44	11	rexrd	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
45		pnfxr	⊢ +∞ ∈ ℝ*
46	45	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
47		ioogtlb	⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ( 𝐶 (,) +∞ ) ) → 𝐶 < 𝐷 )
48	44 46 12 47	syl3anc	⊢ ( 𝜑 → 𝐶 < 𝐷 )
49		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( ℎ · 𝑇 ) ) = ( 𝑥 + ( ℎ · 𝑇 ) ) )
50	49	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
51	50	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ℎ ∈ ℤ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
52	51	cbvrabv	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 }
53	52	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } )
54		oveq1	⊢ ( 𝑘 = 𝑙 → ( 𝑘 · 𝑇 ) = ( 𝑙 · 𝑇 ) )
55	54	oveq2d	⊢ ( 𝑘 = 𝑙 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑙 · 𝑇 ) ) )
56	55	eleq1d	⊢ ( 𝑘 = 𝑙 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
57	56	cbvrexvw	⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 )
58	57	a1i	⊢ ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
59	58	rabbiia	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 }
60	59	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
61		oveq1	⊢ ( 𝑙 = ℎ → ( 𝑙 · 𝑇 ) = ( ℎ · 𝑇 ) )
62	61	oveq2d	⊢ ( 𝑙 = ℎ → ( 𝑦 + ( 𝑙 · 𝑇 ) ) = ( 𝑦 + ( ℎ · 𝑇 ) ) )
63	62	eleq1d	⊢ ( 𝑙 = ℎ → ( ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
64	63	cbvrexvw	⊢ ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 )
65	64	a1i	⊢ ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
66	65	rabbiia	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 }
67	66	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } )
68	60 67	eqtri	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } )
69	68	fveq2i	⊢ ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) )
70	69	oveq1i	⊢ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
71		oveq1	⊢ ( 𝑘 = ℎ → ( 𝑘 · 𝑇 ) = ( ℎ · 𝑇 ) )
72	71	oveq2d	⊢ ( 𝑘 = ℎ → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) )
73	72	breq1d	⊢ ( 𝑘 = ℎ → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
74	73	cbvrabv	⊢ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } = { ℎ ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) }
75	74	supeq1i	⊢ sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) = sup ( { ℎ ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
76		fveq2	⊢ ( 𝑗 = 𝑒 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑒 ) )
77	76	oveq1d	⊢ ( 𝑗 = 𝑒 → ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) = ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) )
78	77	breq1d	⊢ ( 𝑗 = 𝑒 → ( ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
79	78	cbvrabv	⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } = { 𝑒 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) }
80	79	supeq1i	⊢ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) = sup ( { 𝑒 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
81	6 3 7 8 11 43 48 53 70 14 13 75 80	fourierdlem64	⊢ ( 𝜑 → ( ( sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) ∧ sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ ℤ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) )
82	81	simprd	⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
83		simpl1	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝜑 )
84		simpl2l	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
85		cncff	⊢ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
86	10 85	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
87		ffun	⊢ ( 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ → Fun 𝐺 )
88	25 87	syl	⊢ ( 𝜑 → Fun 𝐺 )
89	88	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → Fun 𝐺 )
90		ffvresb	⊢ ( Fun 𝐺 → ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ↔ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) ) )
91	89 90	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ↔ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) ) )
92	86 91	mpbid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) )
93	92	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) )
94	93	simpld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ dom 𝐺 )
95	94	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑠 ∈ dom 𝐺 )
96		dfss3	⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐺 ↔ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑠 ∈ dom 𝐺 )
97	95 96	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐺 )
98	83 84 97	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐺 )
99		simpl2	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) )
100	83 99	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) )
101		simpl3	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
102		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
103	101 102	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
104	3	fourierdlem2	⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
105	7 104	syl	⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
106	8 105	mpbid	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
107	106	simpld	⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
108		elmapi	⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
109	107 108	syl	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
110	109	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
111		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
112	111	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
113	110 112	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
114	113	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
115	114	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
116	115	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
117		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
118	117	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
119	110 118	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
120	119	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
121	120	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
122	121	rexrd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
123		elioore	⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) → 𝑡 ∈ ℝ )
124	123	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 ∈ ℝ )
125		zre	⊢ ( 𝑙 ∈ ℤ → 𝑙 ∈ ℝ )
126	125	adantl	⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) → 𝑙 ∈ ℝ )
127	126	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑙 ∈ ℝ )
128	4 5	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
129	6 128	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
130	129	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑇 ∈ ℝ )
131	127 130	remulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑙 · 𝑇 ) ∈ ℝ )
132	124 131	resubcld	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ ℝ )
133	113	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
134	125	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → 𝑙 ∈ ℝ )
135	129	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → 𝑇 ∈ ℝ )
136	134 135	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑙 · 𝑇 ) ∈ ℝ )
137	133 136	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ )
138	137	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
139	138	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
140	120 136	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ )
141	140	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
142	141	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
143		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
144		ioogtlb	⊢ ( ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) < 𝑡 )
145	139 142 143 144	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) < 𝑡 )
146	133	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
147	146 131 124	ltaddsubd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) < 𝑡 ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) )
148	145 147	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑡 − ( 𝑙 · 𝑇 ) ) )
149		iooltub	⊢ ( ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) )
150	139 142 143 149	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) )
151	124 131 121	ltsubaddd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ 𝑡 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
152	150 151	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
153	116 122 132 148 152	eliood	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
154	100 103 153	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
155	98 154	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 )
156		elioore	⊢ ( 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) → 𝑡 ∈ ℝ )
157		recn	⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
158	157	adantl	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ )
159		zcn	⊢ ( 𝑙 ∈ ℤ → 𝑙 ∈ ℂ )
160	159	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑙 ∈ ℂ )
161	129	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
162	161	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑇 ∈ ℂ )
163	160 162	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( 𝑙 · 𝑇 ) ∈ ℂ )
164	158 163	npcand	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) = 𝑡 )
165	164	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑡 = ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) )
166	165	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → 𝑡 = ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) )
167		ovex	⊢ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ V
168		eleq1	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝑠 ∈ dom 𝐺 ↔ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) )
169	168	anbi2d	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ dom 𝐺 ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) ) )
170		oveq1	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝑠 + ( 𝑙 · 𝑇 ) ) = ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) )
171	170	eleq1d	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ↔ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) )
172	170	fveq2d	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) )
173		fveq2	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) )
174	172 173	eqeq12d	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ↔ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) )
175	171 174	anbi12d	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ) ↔ ( ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) ) )
176	169 175	imbi12d	⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ dom 𝐺 ) → ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) ) ) )
177		ax-resscn	⊢ ℝ ⊆ ℂ
178	177	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
179	1 178	fssd	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
180	179	adantr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → 𝐹 : ℝ ⟶ ℂ )
181	125	adantl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → 𝑙 ∈ ℝ )
182	129	adantr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → 𝑇 ∈ ℝ )
183	181 182	remulcld	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → ( 𝑙 · 𝑇 ) ∈ ℝ )
184	179	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
185	129	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝑇 ∈ ℝ )
186		simplr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝑙 ∈ ℤ )
187		simpr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝑠 ∈ ℝ )
188	9	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
189	184 185 186 187 188	fperiodmul	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑠 ) )
190	180 183 189 2	fperdvper	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ dom 𝐺 ) → ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ) )
191	167 176 190	vtocl	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) )
192	191	simpld	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 )
193	192	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 )
194	166 193	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → 𝑡 ∈ dom 𝐺 )
195	194	ex	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
196	156 195	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
197	196	adantlrl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
198	197	3adantl3	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
199	155 198	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑡 ∈ dom 𝐺 )
200	199	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ∀ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) 𝑡 ∈ dom 𝐺 )
201		dfss3	⊢ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 ↔ ∀ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) 𝑡 ∈ dom 𝐺 )
202	200 201	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 )
203	202	3exp	⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) → ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 ) ) )
204	203	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 ) )
205	82 204	mpd	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 )
206	205	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑠 ∈ dom 𝐺 )
207	206	iftrued	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
208	41 207	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐺 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑠 ) )
209	208	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
210	28	a1i	⊢ ( 𝜑 → dom 𝐺 = dom ( ℝ D 𝐹 ) )
211	210	feq2d	⊢ ( 𝜑 → ( 𝐺 : dom 𝐺 ⟶ ℝ ↔ 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ) )
212	25 211	mpbird	⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℝ )
213	212 205	feqresmpt	⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
214	38 15	fmptd	⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ℝ )
215	214 17	feqresmpt	⊢ ( 𝜑 → ( 𝐻 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
216	209 213 215	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝐻 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) )
217	214 178	fssd	⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ℂ )
218	15	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ) )
219		eleq1	⊢ ( 𝑠 = ( 𝑥 + 𝑇 ) → ( 𝑠 ∈ dom 𝐺 ↔ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) )
220		fveq2	⊢ ( 𝑠 = ( 𝑥 + 𝑇 ) → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
221	219 220	ifbieq1d	⊢ ( 𝑠 = ( 𝑥 + 𝑇 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) )
222	179 129 9 2	fperdvper	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) ) )
223	222	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
224	223	iftrued	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
225	221 224	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = ( 𝑥 + 𝑇 ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
226	225	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = ( 𝑥 + 𝑇 ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
227		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
228	129	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
229	227 228	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
230	229	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
231	212	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝐺 : dom 𝐺 ⟶ ℝ )
232	223	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
233	231 232	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ∈ ℝ )
234	218 226 230 233	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
235	222	simprd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) )
236	235	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) )
237		eleq1	⊢ ( 𝑠 = 𝑥 → ( 𝑠 ∈ dom 𝐺 ↔ 𝑥 ∈ dom 𝐺 ) )
238		fveq2	⊢ ( 𝑠 = 𝑥 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑥 ) )
239	237 238	ifbieq1d	⊢ ( 𝑠 = 𝑥 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) )
240	239	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = 𝑥 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) )
241		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ ℝ )
242		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
243	242	iftrued	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) = ( 𝐺 ‘ 𝑥 ) )
244	212	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
245	243 244	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) ∈ ℝ )
246	245	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) ∈ ℝ )
247	218 240 241 246	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) )
248		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
249	248	iftrued	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) = ( 𝐺 ‘ 𝑥 ) )
250	247 249	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
251	234 236 250	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐻 ‘ 𝑥 ) )
252	229	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 𝑇 ) ∈ ℂ )
253	228	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℂ )
254	252 253	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 + 𝑇 ) + - 𝑇 ) = ( ( 𝑥 + 𝑇 ) − 𝑇 ) )
255	227	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
256	255 253	pncand	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 + 𝑇 ) − 𝑇 ) = 𝑥 )
257	254 256	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 = ( ( 𝑥 + 𝑇 ) + - 𝑇 ) )
258	257	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → 𝑥 = ( ( 𝑥 + 𝑇 ) + - 𝑇 ) )
259		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
260		simpll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → 𝜑 )
261	260 259	jca	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) )
262		eleq1	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝑦 ∈ dom 𝐺 ↔ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) )
263	262	anbi2d	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐺 ) ↔ ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) ) )
264		oveq1	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝑦 + - 𝑇 ) = ( ( 𝑥 + 𝑇 ) + - 𝑇 ) )
265	264	eleq1d	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ↔ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ) )
266	264	fveq2d	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) )
267		fveq2	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
268	266 267	eqeq12d	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) )
269	265 268	anbi12d	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) ) )
270	263 269	imbi12d	⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐺 ) → ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) ) ) )
271	129	renegcld	⊢ ( 𝜑 → - 𝑇 ∈ ℝ )
272	161	mulm1d	⊢ ( 𝜑 → ( - 1 · 𝑇 ) = - 𝑇 )
273	272	eqcomd	⊢ ( 𝜑 → - 𝑇 = ( - 1 · 𝑇 ) )
274	273	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → - 𝑇 = ( - 1 · 𝑇 ) )
275	274	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + - 𝑇 ) = ( 𝑦 + ( - 1 · 𝑇 ) ) )
276	275	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐹 ‘ ( 𝑦 + ( - 1 · 𝑇 ) ) ) )
277	179	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
278	129	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑇 ∈ ℝ )
279		1zzd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℤ )
280	279	znegcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → - 1 ∈ ℤ )
281		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
282	9	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
283	277 278 280 281 282	fperiodmul	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + ( - 1 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
284	276 283	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
285	179 271 284 2	fperdvper	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐺 ) → ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ) )
286	270 285	vtoclg	⊢ ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 → ( ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) ) )
287	259 261 286	sylc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) )
288	287	simpld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 )
289	258 288	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
290	289	stoic1a	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ¬ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
291	290	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) = 0 )
292	15	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ) )
293	221	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = ( 𝑥 + 𝑇 ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) )
294	229	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
295		0red	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → 0 ∈ ℝ )
296	291 295	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) ∈ ℝ )
297	292 293 294 296	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) )
298		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ¬ 𝑥 ∈ dom 𝐺 )
299	298	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) = 0 )
300	239 299	sylan9eqr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = 𝑥 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = 0 )
301		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ ℝ )
302	292 300 301 295	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ 𝑥 ) = 0 )
303	291 297 302	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐻 ‘ 𝑥 ) )
304	251 303	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐻 ‘ 𝑥 ) )
305		elioore	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
306	305	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
307	305 38	sylan2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
308	306 307 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
309	308	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
310	94	iftrued	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
311	309 310	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑠 ) )
312	311	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
313	214	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 : ℝ ⟶ ℝ )
314		ioossre	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
315	314	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
316	313 315	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
317	212	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 : dom 𝐺 ⟶ ℝ )
318	317 97	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
319	312 316 318	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
320	319 10	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
321		eqid	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
322		oveq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 + ( 𝑙 · 𝑇 ) ) = ( 𝑦 + ( 𝑙 · 𝑇 ) ) )
323	322	eleq1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
324	323	rexbidv	⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
325	324	cbvrabv	⊢ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 }
326	325	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
327	326	eqcomi	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
328	60	fveq2i	⊢ ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) )
329	328	oveq1i	⊢ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
330		isoeq5	⊢ ( ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
331	67 330	ax-mp	⊢ ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
332	331	iotabii	⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
333		isoeq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
334	333	cbviotavw	⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
335	332 334 14	3eqtr4ri	⊢ 𝑉 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
336		id	⊢ ( 𝑣 = 𝑥 → 𝑣 = 𝑥 )
337		oveq2	⊢ ( 𝑣 = 𝑥 → ( 𝐵 − 𝑣 ) = ( 𝐵 − 𝑥 ) )
338	337	oveq1d	⊢ ( 𝑣 = 𝑥 → ( ( 𝐵 − 𝑣 ) / 𝑇 ) = ( ( 𝐵 − 𝑥 ) / 𝑇 ) )
339	338	fveq2d	⊢ ( 𝑣 = 𝑥 → ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) )
340	339	oveq1d	⊢ ( 𝑣 = 𝑥 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
341	336 340	oveq12d	⊢ ( 𝑣 = 𝑥 → ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
342	341	cbvmptv	⊢ ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
343		eqeq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 = 𝐵 ↔ 𝑧 = 𝐵 ) )
344		id	⊢ ( 𝑢 = 𝑧 → 𝑢 = 𝑧 )
345	343 344	ifbieq2d	⊢ ( 𝑢 = 𝑧 → if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) = if ( 𝑧 = 𝐵 , 𝐴 , 𝑧 ) )
346	345	cbvmptv	⊢ ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) = ( 𝑧 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑧 = 𝐵 , 𝐴 , 𝑧 ) )
347		eqid	⊢ ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
348		eqid	⊢ ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) )
349		eqid	⊢ ( 𝑧 ∈ ( ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) (,) ( ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) ↦ ( ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑧 − ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) ) = ( 𝑧 ∈ ( ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) (,) ( ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) ↦ ( ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑧 − ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) )
350		fveq2	⊢ ( 𝑖 = 𝑡 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑡 ) )
351	350	breq1d	⊢ ( 𝑖 = 𝑡 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
352	351	cbvrabv	⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } = { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) }
353		fveq2	⊢ ( 𝑤 = 𝑥 → ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) = ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) )
354	353	fveq2d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) = ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) )
355	354	eqcomd	⊢ ( 𝑤 = 𝑥 → ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) = ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) )
356	355	breq2d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) ) )
357	356	rabbidv	⊢ ( 𝑤 = 𝑥 → { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } = { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } )
358	352 357	eqtr2id	⊢ ( 𝑤 = 𝑥 → { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
359	358	supeq1d	⊢ ( 𝑤 = 𝑥 → sup ( { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
360	359	cbvmptv	⊢ ( 𝑤 ∈ ℝ ↦ sup ( { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
361	3 6 7 8 217 304 320 11 12 321 327 329 335 342 346 13 347 348 349 360	fourierdlem90	⊢ ( 𝜑 → ( 𝐻 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )
362	216 361	eqeltrd	⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )