Theorem fourierdlem51

Description: X is in the periodic partition, when the considered interval is centered at X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem51.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem51.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem51.alt0	⊢ ( 𝜑 → 𝐴 < 0 )
	fourierdlem51.bgt0	⊢ ( 𝜑 → 0 < 𝐵 )
	fourierdlem51.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem51.cfi	⊢ ( 𝜑 → 𝐶 ∈ Fin )
	fourierdlem51.css	⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐴 [,] 𝐵 ) )
	fourierdlem51.bc	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
	fourierdlem51.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
	fourierdlem51.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem51.exc	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ 𝐶 )
	fourierdlem51.d	⊢ 𝐷 = ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
	fourierdlem51.f	⊢ 𝐹 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) )
	fourierdlem51.h	⊢ 𝐻 = { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
Assertion	fourierdlem51	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem51.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		fourierdlem51.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		fourierdlem51.alt0	⊢ ( 𝜑 → 𝐴 < 0 )
4		fourierdlem51.bgt0	⊢ ( 𝜑 → 0 < 𝐵 )
5		fourierdlem51.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
6		fourierdlem51.cfi	⊢ ( 𝜑 → 𝐶 ∈ Fin )
7		fourierdlem51.css	⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐴 [,] 𝐵 ) )
8		fourierdlem51.bc	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
9		fourierdlem51.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
10		fourierdlem51.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
11		fourierdlem51.exc	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ 𝐶 )
12		fourierdlem51.d	⊢ 𝐷 = ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
13		fourierdlem51.f	⊢ 𝐹 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) )
14		fourierdlem51.h	⊢ 𝐻 = { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
15	1 10	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ )
16	2 10	readdcld	⊢ ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ )
17		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
18	1 17 10 3	ltadd1dd	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) < ( 0 + 𝑋 ) )
19	10	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
20	19	addlidd	⊢ ( 𝜑 → ( 0 + 𝑋 ) = 𝑋 )
21	18 20	breqtrd	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) < 𝑋 )
22	15 10 21	ltled	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ≤ 𝑋 )
23	17 2 10 4	ltadd1dd	⊢ ( 𝜑 → ( 0 + 𝑋 ) < ( 𝐵 + 𝑋 ) )
24	20 23	eqbrtrrd	⊢ ( 𝜑 → 𝑋 < ( 𝐵 + 𝑋 ) )
25	10 16 24	ltled	⊢ ( 𝜑 → 𝑋 ≤ ( 𝐵 + 𝑋 ) )
26	15 16 10 22 25	eliccd	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
27	2 10	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
28	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
29	5 28	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
30	1 17 2 3 4	lttrd	⊢ ( 𝜑 → 𝐴 < 𝐵 )
31	1 2	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
32	30 31	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
33	5	eqcomi	⊢ ( 𝐵 − 𝐴 ) = 𝑇
34	33	a1i	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = 𝑇 )
35	32 34	breqtrd	⊢ ( 𝜑 → 0 < 𝑇 )
36	35	gt0ne0d	⊢ ( 𝜑 → 𝑇 ≠ 0 )
37	27 29 36	redivcld	⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℝ )
38	37	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℤ )
39	9	a1i	⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
40		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
41		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑋 ) )
42	41	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
43	42	fveq2d	⊢ ( 𝑥 = 𝑋 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
44	43	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
45	40 44	oveq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
47	38	zred	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℝ )
48	47 29	remulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
49	10 48	readdcld	⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
50	39 46 10 49	fvmptd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
51	50 11	eqeltrrd	⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐶 )
52		oveq1	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
53	52	oveq2d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( 𝑋 + ( 𝑘 · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
54	53	eleq1d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐶 ) )
55	54	rspcev	⊢ ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℤ ∧ ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐶 ) → ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
56	38 51 55	syl2anc	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
57		oveq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
58	57	eleq1d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
59	58	rexbidv	⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
60	59	elrab	⊢ ( 𝑋 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↔ ( 𝑋 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
61	26 56 60	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
62		elun2	⊢ ( 𝑋 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑋 ∈ ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
63	61 62	syl	⊢ ( 𝜑 → 𝑋 ∈ ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
64	63 12	eleqtrrdi	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
65		prfi	⊢ { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∈ Fin
66		snfi	⊢ { ( 𝐴 + 𝑋 ) } ∈ Fin
67		fvres	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
69		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
70	69	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
71	70	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
72	71	elrab	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↔ ( 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
73	72	simprbi	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
74	73	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
75		nfv	⊢ Ⅎ 𝑘 𝜑
76		nfre1	⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶
77		nfcv	⊢ Ⅎ 𝑘 ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) )
78	76 77	nfrabw	⊢ Ⅎ 𝑘 { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
79	78	nfcri	⊢ Ⅎ 𝑘 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
80	75 79	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
81		nfv	⊢ Ⅎ 𝑘 ( 𝐸 ‘ 𝑥 ) ∈ 𝐶
82		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝜑 )
83	15	rexrd	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ* )
84		iocssre	⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
85	83 16 84	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
86	85	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
87		elrabi	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
88	87	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
89	86 88	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ℝ )
90		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
91	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
92	91 90	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐵 − 𝑥 ) ∈ ℝ )
93	29	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
94	36	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ≠ 0 )
95	92 93 94	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) ∈ ℝ )
96	95	flcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
97	96	zred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
98	97 93	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
99	90 98	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
100	9	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
101	90 99 100	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
102	101	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
103		simpl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) )
104	96	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
105		simpr	⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 )
106	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
107	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
108	1 2 30	ltled	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
109		lbicc2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
110	106 107 108 109	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
111	110	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
112	105 111	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
113	112	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
114	103 104 113	jca31	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
115		iocssicc	⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
116	1 2 30 5 9	fourierdlem4	⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
117	116	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
118	115 117	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) )
119	101 118	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
120	119	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
121	106	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ* )
122	91	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ* )
123		iocgtlb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
124	121 122 117 123	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
125	124	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
126		id	⊢ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 )
127	126	eqcomd	⊢ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → 𝐴 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
128	127	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
129	125 128 102	3brtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
130		zre	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
131	130	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
132	29	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℝ )
133	131 132	remulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
134	133	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
135	134	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
136	98	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
137		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑥 ∈ ℝ )
138	135 136 137	ltadd2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑘 · 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
139	129 138	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑘 · 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
140	130	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑘 ∈ ℝ )
141	97	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
142	29 35	elrpd	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
143	142	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑇 ∈ ℝ+ )
144	140 141 143	ltmul1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ↔ ( 𝑘 · 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
145	139 144	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) )
146		fvex	⊢ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ V
147		eleq1	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑗 ∈ ℤ ↔ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) )
148	147	anbi2d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ) )
149	148	anbi1d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
150		oveq1	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑗 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
151	150	oveq2d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
152	151	eleq1d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
153	149 152	anbi12d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
154		breq2	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑘 < 𝑗 ↔ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) )
155	153 154	anbi12d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) ) )
156		eqeq1	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑗 = ( 𝑘 + 1 ) ↔ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) ) )
157	155 156	imbi12d	⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) → 𝑗 = ( 𝑘 + 1 ) ) ↔ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) ) ) )
158		eleq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ℤ ↔ 𝑘 ∈ ℤ ) )
159	158	anbi2d	⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ) )
160	159	anbi1d	⊢ ( 𝑖 = 𝑘 → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ) )
161		oveq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 · 𝑇 ) = ( 𝑘 · 𝑇 ) )
162	161	oveq2d	⊢ ( 𝑖 = 𝑘 → ( 𝑥 + ( 𝑖 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
163	162	eleq1d	⊢ ( 𝑖 = 𝑘 → ( ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
164	160 163	anbi12d	⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
165	164	anbi1d	⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
166		breq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 < 𝑗 ↔ 𝑘 < 𝑗 ) )
167	165 166	anbi12d	⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) ) )
168		oveq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 + 1 ) = ( 𝑘 + 1 ) )
169	168	eqeq2d	⊢ ( 𝑖 = 𝑘 → ( 𝑗 = ( 𝑖 + 1 ) ↔ 𝑗 = ( 𝑘 + 1 ) ) )
170	167 169	imbi12d	⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 = ( 𝑖 + 1 ) ) ↔ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) → 𝑗 = ( 𝑘 + 1 ) ) ) )
171		simp-6l	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝜑 )
172	171 1	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝐴 ∈ ℝ )
173	171 2	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝐵 ∈ ℝ )
174	171 30	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝐴 < 𝐵 )
175		simp-6r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑥 ∈ ℝ )
176		simp-5r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ ℤ )
177		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ℤ )
178		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 )
179		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
180		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
181	172 173 174 5 175 176 177 178 179 180	fourierdlem6	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 = ( 𝑖 + 1 ) )
182	170 181	chvarvv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) → 𝑗 = ( 𝑘 + 1 ) )
183	146 157 182	vtocl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) )
184	114 120 145 183	syl21anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) )
185	184	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( 𝑘 + 1 ) · 𝑇 ) )
186	185	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) )
187	131	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
188	29	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
189	188	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℂ )
190	187 189	adddirp1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 + 1 ) · 𝑇 ) = ( ( 𝑘 · 𝑇 ) + 𝑇 ) )
191	190	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
192	191	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
193	192	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
194	90	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
195	194	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → 𝑥 ∈ ℂ )
196	134	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℂ )
197	188	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℂ )
198	195 196 197	addassd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
199	198	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) = ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) )
200	199	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) = ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) )
201		oveq1	⊢ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = ( 𝐴 + 𝑇 ) )
202	201	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = ( 𝐴 + 𝑇 ) )
203	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
204	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
205	203 204 188	subaddd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) = 𝑇 ↔ ( 𝐴 + 𝑇 ) = 𝐵 ) )
206	34 205	mpbid	⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) = 𝐵 )
207	206	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐴 + 𝑇 ) = 𝐵 )
208	202 207	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = 𝐵 )
209	193 200 208	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = 𝐵 )
210	102 186 209	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) = 𝐵 )
211	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐵 ∈ 𝐶 )
212	210 211	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
213	212	3adantl3	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
214		simpl1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝜑 ∧ 𝑥 ∈ ℝ ) )
215		simpl2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑘 ∈ ℤ )
216	7	sselda	⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
217	216	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
218	217	3adant2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
219	218	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
220		neqne	⊢ ( ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ≠ 𝐴 )
221	220	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ≠ 𝐴 )
222	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
223	214 222	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 ∈ ℝ )
224	214 91	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐵 ∈ ℝ )
225		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → 𝑥 ∈ ℝ )
226	225 134	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
227	226	rexrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
228	214 215 227	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
229	223 224 228	eliccelioc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ≠ 𝐴 ) ) )
230	219 221 229	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
231	101	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
232	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 ∈ ℝ )
233	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐵 ∈ ℝ )
234	30	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < 𝐵 )
235		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ℝ )
236	96	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
237		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝑘 ∈ ℤ )
238	101 117	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
239	238	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
240		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
241	232 233 234 5 235 236 237 239 240	fourierdlem35	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = 𝑘 )
242	241	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( 𝑘 · 𝑇 ) )
243	242	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
244	231 243	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
245	214 215 230 244	syl21anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
246		simpl3	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
247	245 246	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
248	213 247	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
249	248	3exp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑘 ∈ ℤ → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 ) ) )
250	82 89 249	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( 𝑘 ∈ ℤ → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 ) ) )
251	80 81 250	rexlimd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 ) )
252	74 251	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
253	68 252	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ∈ 𝐶 )
254		eqid	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) )
255	253 254	fmptd	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 )
256		iocssre	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
257	106 2 256	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
258	116 257	fssd	⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ℝ )
259		ssrab2	⊢ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) )
260	259 85	sstrid	⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ℝ )
261	258 260	fssresd	⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ ℝ )
262	261	feqmptd	⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) = ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) )
263	262	feq1d	⊢ ( 𝜑 → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 ↔ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 ) )
264	255 263	mpbird	⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 )
265		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝜑 )
266		id	⊢ ( 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
267	266 14	eleqtrrdi	⊢ ( 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑤 ∈ 𝐻 )
268	267	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝑤 ∈ 𝐻 )
269	265 268	jca	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) )
270		id	⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
271	270 14	eleqtrrdi	⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑧 ∈ 𝐻 )
272	271	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝑧 ∈ 𝐻 )
273		fvres	⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) = ( 𝐸 ‘ 𝑧 ) )
274	273	eqcomd	⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( 𝐸 ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) )
275	274	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( 𝐸 ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) )
276		id	⊢ ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) )
277	276	eqcomd	⊢ ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) )
278	277	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) )
279		fvres	⊢ ( 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( 𝐸 ‘ 𝑤 ) )
280	279	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( 𝐸 ‘ 𝑤 ) )
281	275 278 280	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) )
282	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝐴 ∈ ℝ )
283	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝐵 ∈ ℝ )
284	30	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝐴 < 𝐵 )
285	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑋 ∈ ℝ )
286		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑤 ∈ 𝐻 )
287		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑧 ∈ 𝐻 )
288		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) )
289	282 283 284 285 14 5 9 286 287 288	fourierdlem19	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ¬ 𝑤 < 𝑧 )
290	288	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑧 ) )
291	282 283 284 285 14 5 9 287 286 290	fourierdlem19	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ¬ 𝑧 < 𝑤 )
292	14 260	eqsstrid	⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
293	292	sselda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) → 𝑤 ∈ ℝ )
294	293	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑤 ∈ ℝ )
295	292	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) → 𝐻 ⊆ ℝ )
296	295	sselda	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) → 𝑧 ∈ ℝ )
297	296	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑧 ∈ ℝ )
298	294 297	lttri3d	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ( 𝑤 = 𝑧 ↔ ( ¬ 𝑤 < 𝑧 ∧ ¬ 𝑧 < 𝑤 ) ) )
299	289 291 298	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑤 = 𝑧 )
300	269 272 281 299	syl21anc	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝑤 = 𝑧 )
301	300	ex	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
302	301	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ∀ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
303	302	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∀ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
304		dff13	⊢ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } –1-1→ 𝐶 ↔ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 ∧ ∀ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∀ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) ) )
305	264 303 304	sylanbrc	⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } –1-1→ 𝐶 )
306		f1fi	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } –1-1→ 𝐶 ) → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
307	6 305 306	syl2anc	⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
308		unfi	⊢ ( ( { ( 𝐴 + 𝑋 ) } ∈ Fin ∧ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin ) → ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
309	66 307 308	sylancr	⊢ ( 𝜑 → ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
310		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝜑 )
311		elrabi	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
312	311	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
313	71	elrab	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↔ ( 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
314	313	simprbi	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
315	314	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
316		velsn	⊢ ( 𝑥 ∈ { ( 𝐴 + 𝑋 ) } ↔ 𝑥 = ( 𝐴 + 𝑋 ) )
317		elun1	⊢ ( 𝑥 ∈ { ( 𝐴 + 𝑋 ) } → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
318	316 317	sylbir	⊢ ( 𝑥 = ( 𝐴 + 𝑋 ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
319	318	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
320	83	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ* )
321	16	rexrd	⊢ ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ* )
322	321	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐵 + 𝑋 ) ∈ ℝ* )
323	15 16	iccssred	⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
324	323	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ∈ ℝ )
325	324	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ∈ ℝ* )
326	325	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ℝ* )
327	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ )
328	324	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ℝ )
329	83	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ* )
330	321	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐵 + 𝑋 ) ∈ ℝ* )
331		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
332		iccgelb	⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) ≤ 𝑥 )
333	329 330 331 332	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) ≤ 𝑥 )
334	333	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) ≤ 𝑥 )
335		neqne	⊢ ( ¬ 𝑥 = ( 𝐴 + 𝑋 ) → 𝑥 ≠ ( 𝐴 + 𝑋 ) )
336	335	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ≠ ( 𝐴 + 𝑋 ) )
337	327 328 334 336	leneltd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) < 𝑥 )
338		iccleub	⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑋 ) )
339	329 330 331 338	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑋 ) )
340	339	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ≤ ( 𝐵 + 𝑋 ) )
341	320 322 326 337 340	eliocd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
342	341	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
343		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
344	342 343 72	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
345		elun2	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
346	344 345	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
347	319 346	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
348	310 312 315 347	syl21anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
349	348	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
350		dfss3	⊢ ( { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ↔ ∀ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
351	349 350	sylibr	⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
352		ssfi	⊢ ( ( ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin ∧ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ) → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
353	309 351 352	syl2anc	⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
354		unfi	⊢ ( ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∈ Fin ∧ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin ) → ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
355	65 353 354	sylancr	⊢ ( 𝜑 → ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
356	12 355	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ Fin )
357		prssi	⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ ∧ ( 𝐵 + 𝑋 ) ∈ ℝ ) → { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ⊆ ℝ )
358	15 16 357	syl2anc	⊢ ( 𝜑 → { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ⊆ ℝ )
359		ssrab2	⊢ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) )
360	359 323	sstrid	⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ℝ )
361	358 360	unssd	⊢ ( 𝜑 → ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ⊆ ℝ )
362	12 361	eqsstrid	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
363		eqid	⊢ ( ( ♯ ‘ 𝐷 ) − 1 ) = ( ( ♯ ‘ 𝐷 ) − 1 )
364	356 362 13 363	fourierdlem36	⊢ ( 𝜑 → 𝐹 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) )
365		isof1o	⊢ ( 𝐹 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) → 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –1-1-onto→ 𝐷 )
366		f1ofo	⊢ ( 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –1-1-onto→ 𝐷 → 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –onto→ 𝐷 )
367	365 366	syl	⊢ ( 𝐹 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) → 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –onto→ 𝐷 )
368		forn	⊢ ( 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –onto→ 𝐷 → ran 𝐹 = 𝐷 )
369	364 367 368	3syl	⊢ ( 𝜑 → ran 𝐹 = 𝐷 )
370	64 369	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐹 )