fourierdlem51 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem51		Structured version Visualization version GIF version

Theorem fourierdlem51 46172

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
fourierdlem51	⊢ (𝜑 → 𝑋 ∈ ran 𝐹)

Distinct variable groups: 𝐴,𝑘,𝑥,𝑦 𝐵,𝑘,𝑥,𝑦 𝐶,𝑘,𝑥,𝑦 𝐷,𝑓 𝑘,𝐸,𝑥 𝑓,𝐹 𝑥,𝐻 𝑇,𝑘,𝑥,𝑦 𝑘,𝑋,𝑥,𝑦 𝜑,𝑓 𝜑,𝑘,𝑥 Allowed substitution hints: 𝜑(𝑦) 𝐴(𝑓) 𝐵(𝑓) 𝐶(𝑓) 𝐷(𝑥,𝑦,𝑘) 𝑇(𝑓) 𝐸(𝑦,𝑓) 𝐹(𝑥,𝑦,𝑘) 𝐻(𝑦,𝑓,𝑘) 𝑋(𝑓)

Proof of Theorem fourierdlem51 Dummy variables 𝑖 𝑗 𝑤 𝑧 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 ∪ cun 3949 ⊆ wss 3951 {csn 4626 {cpr 4628 class class class wbr 5143 ↦ cmpt 5225 ran crn 5686 ↾ cres 5687 ℩cio 6512 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 ℤcz 12613 ℝ⁺crp 13034 (,]cioc 13388 [,]cicc 13390 ...cfz 13547 ⌊cfl 13830 ♯chash 14369

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-inf 9483 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-n0 12527 df-z 12614 df-uz 12879 df-rp 13035 df-ioc 13392 df-icc 13394 df-fz 13548 df-fl 13832 df-hash 14370

This theorem is referenced by: fourierdlem113 46234

W3C validator