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 39050

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 9948	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ)
4		fourierdlem51.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5	4, 2	readdcld 9948	. . . . . 6 ⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ)
6		0red 9920	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
7		fourierdlem51.alt0	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < 0)
8	1, 6, 2, 7	ltadd1dd 10517	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 𝑋) < (0 + 𝑋))
9	2	recnd 9947	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ℂ)
10	9	addid2d 10116	. . . . . . . 8 ⊢ (𝜑 → (0 + 𝑋) = 𝑋)
11	8, 10	breqtrd 4609	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝑋) < 𝑋)
12	3, 2, 11	ltled 10064	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝑋) ≤ 𝑋)
13		fourierdlem51.bgt0	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝐵)
14	6, 4, 2, 13	ltadd1dd 10517	. . . . . . . 8 ⊢ (𝜑 → (0 + 𝑋) < (𝐵 + 𝑋))
15	10, 14	eqbrtrrd 4607	. . . . . . 7 ⊢ (𝜑 → 𝑋 < (𝐵 + 𝑋))
16	2, 5, 15	ltled 10064	. . . . . 6 ⊢ (𝜑 → 𝑋 ≤ (𝐵 + 𝑋))
17	3, 5, 2, 12, 16	eliccd 38573	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
18	4, 2	resubcld 10337	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
19		fourierdlem51.t	. . . . . . . . 9 ⊢ 𝑇 = (𝐵 − 𝐴)
20	4, 1	resubcld 10337	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
21	19, 20	syl5eqel 2692	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℝ)
22	1, 6, 4, 7, 13	lttrd 10077	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
23	1, 4	posdifd 10493	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
24	22, 23	mpbid 221	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
25	19	eqcomi 2619	. . . . . . . . . . 11 ⊢ (𝐵 − 𝐴) = 𝑇
26	25	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
27	24, 26	breqtrd 4609	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝑇)
28	27	gt0ne0d 10471	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ≠ 0)
29	18, 21, 28	redivcld 10732	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
30	29	flcld 12461	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
31		fourierdlem51.e	. . . . . . . . 9 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
32	31	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
33		id 22	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
34		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
35	34	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
36	35	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
37	36	oveq1d 6564	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
38	33, 37	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
39	38	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
40	30	zred 11358	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
41	40, 21	remulcld 9949	. . . . . . . . 9 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
42	2, 41	readdcld 9948	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
43	32, 39, 2, 42	fvmptd 6197	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
44		fourierdlem51.exc	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐶)
45	43, 44	eqeltrrd 2689	. . . . . 6 ⊢ (𝜑 → (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶)
46		oveq1 6556	. . . . . . . . 9 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
47	46	oveq2d 6565	. . . . . . . 8 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑋 + (𝑘 · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
48	47	eleq1d 2672	. . . . . . 7 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑋 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶))
49	48	rspcev 3282	. . . . . 6 ⊢ (((⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ ∧ (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶) → ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶)
50	30, 45, 49	syl2anc 691	. . . . 5 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶)
51		oveq1 6556	. . . . . . . 8 ⊢ (𝑦 = 𝑋 → (𝑦 + (𝑘 · 𝑇)) = (𝑋 + (𝑘 · 𝑇)))
52	51	eleq1d 2672	. . . . . . 7 ⊢ (𝑦 = 𝑋 → ((𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
53	52	rexbidv 3034	. . . . . 6 ⊢ (𝑦 = 𝑋 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
54	53	elrab 3331	. . . . 5 ⊢ (𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑋 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
55	17, 50, 54	sylanbrc 695	. . . 4 ⊢ (𝜑 → 𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
56		elun2 3743	. . . 4 ⊢ (𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑋 ∈ ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
57	55, 56	syl 17	. . 3 ⊢ (𝜑 → 𝑋 ∈ ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
58		fourierdlem51.d	. . 3 ⊢ 𝐷 = ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
59	57, 58	syl6eleqr 2699	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
60		prfi 8120	. . . . . 6 ⊢ {(𝐴 + 𝑋), (𝐵 + 𝑋)} ∈ Fin
61		snfi 7923	. . . . . . . 8 ⊢ {(𝐴 + 𝑋)} ∈ Fin
62		fourierdlem51.cfi	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ Fin)
63		fvres 6117	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) = (𝐸‘𝑥))
64	63	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) = (𝐸‘𝑥))
65		oveq1 6556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
66	65	eleq1d 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
67	66	rexbidv 3034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
68	67	elrab 3331	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
69	68	simprbi 479	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
70	69	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
71		nfv 1830	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
72		nfre1 2988	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶
73		nfcv 2751	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐴 + 𝑋)(,](𝐵 + 𝑋))
74	72, 73	nfrab 3100	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
75	74	nfcri 2745	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
76	71, 75	nfan 1816	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
77		nfv 1830	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐸‘𝑥) ∈ 𝐶
78		simpl 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝜑)
79	3	rexrd 9968	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ^*)
80		iocssre 12124	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
81	79, 5, 80	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
82	81	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
83		elrabi 3328	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
84	83	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
85	82, 84	sseldd 3569	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ℝ)
86		simpr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
87	4	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
88	87, 86	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
89	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
90	28	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
91	88, 89, 90	redivcld 10732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
92	91	flcld 12461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
93	92	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
94	93, 89	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
95	86, 94	readdcld 9948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
96	31	fvmpt2 6200	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
97	86, 95, 96	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
98	97	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
99		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ))
100	92	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
101		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) = 𝐴)
102	1	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
103	4	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
104	1, 4, 22	ltled 10064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
105		lbicc2 12159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
106	102, 103, 104, 105	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
107	106	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 ∈ (𝐴[,]𝐵))
108	101, 107	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
109	108	ad4ant14 1285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
110	99, 100, 109	jca31 555	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)))
111		iocssicc 12132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
112	1, 4, 22, 19, 31	fourierdlem4 39004	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
113	112	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
114	111, 113	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴[,]𝐵))
115	97, 114	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))
116	115	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))
117	102	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ^*)
118	87	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ^*)
119		iocgtlb 38571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑥))
120	117, 118, 113, 119	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥))
121	120	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 < (𝐸‘𝑥))
122		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → (𝑥 + (𝑘 · 𝑇)) = 𝐴)
123	122	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → 𝐴 = (𝑥 + (𝑘 · 𝑇)))
124	123	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 = (𝑥 + (𝑘 · 𝑇)))
125	121, 124, 98	3brtr3d 4614	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
126		zre 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
127	126	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
128	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
129	127, 128	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
130	129	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 · 𝑇) ∈ ℝ)
132	94	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
133		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑥 ∈ ℝ)
134	131, 132, 133	ltadd2d 10072	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ↔ (𝑥 + (𝑘 · 𝑇)) < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
135	125, 134	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
136	126	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 ∈ ℝ)
137	93	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
138	21, 27	elrpd 11745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
139	138	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑇 ∈ ℝ⁺)
140	136, 137, 139	ltmul1d 11789	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)) ↔ (𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
141	135, 140	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)))
142		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ V
143		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ))
144	143	anbi2d 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ↔ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)))
145	144	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))))
146		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
147	146	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑥 + (𝑗 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
148	147	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵) ↔ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)))
149	145, 148	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))))
150		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 < 𝑗 ↔ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))))
151	149, 150	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) ↔ ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)))))
152		eqeq1 2614	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 = (𝑘 + 1) ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1)))
153	151, 152	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1)) ↔ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))))
154		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ ℤ ↔ 𝑘 ∈ ℤ))
155	154	anbi2d 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ↔ ((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ)))
156	155	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ↔ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ)))
157		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑘 → (𝑖 · 𝑇) = (𝑘 · 𝑇))
158	157	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑘 → (𝑥 + (𝑖 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
159	158	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑘 → ((𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵) ↔ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)))
160	156, 159	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑘 → (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))))
161	160	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵))))
162		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → (𝑖 < 𝑗 ↔ 𝑘 < 𝑗))
163	161, 162	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑘 → (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) ↔ ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗)))
164		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
165	164	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑘 → (𝑗 = (𝑖 + 1) ↔ 𝑗 = (𝑘 + 1)))
166	163, 165	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = 𝑘 → ((((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 = (𝑖 + 1)) ↔ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1))))
167		simp-6l 806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝜑)
168	167, 1	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐴 ∈ ℝ)
169	167, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐵 ∈ ℝ)
170	167, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐴 < 𝐵)
171		simp-6r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑥 ∈ ℝ)
172		simp-5r 805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
173		simp-4r 803	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
174		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
175		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵))
176		simplr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵))
177	168, 169, 170, 19, 171, 172, 173, 174, 175, 176	fourierdlem6 39006	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 = (𝑖 + 1))
178	166, 177	chvarv 2251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1))
179	142, 153, 178	vtocl 3232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))
180	110, 116, 141, 179	syl21anc 1317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))
181	180	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((𝑘 + 1) · 𝑇))
182	181	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((𝑘 + 1) · 𝑇)))
183	127	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
184	21	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
185	184	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℂ)
186	183, 185	adddirp1d 9945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → ((𝑘 + 1) · 𝑇) = ((𝑘 · 𝑇) + 𝑇))
187	186	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
188	187	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
189	188	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
190	86	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
191	190	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℂ)
192	130	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℂ)
193	184	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℂ)
194	191, 192, 193	addassd 9941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
195	194	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 · 𝑇) + 𝑇)) = ((𝑥 + (𝑘 · 𝑇)) + 𝑇))
196	195	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 · 𝑇) + 𝑇)) = ((𝑥 + (𝑘 · 𝑇)) + 𝑇))
197		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝐴 + 𝑇))
198	197	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝐴 + 𝑇))
199	4	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐵 ∈ ℂ)
200	1	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 ∈ ℂ)
201	199, 200, 184	subaddd 10289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐵 − 𝐴) = 𝑇 ↔ (𝐴 + 𝑇) = 𝐵))
202	26, 201	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
203	202	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐴 + 𝑇) = 𝐵)
204	198, 203	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = 𝐵)
205	189, 196, 204	3eqtrd 2648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 + 1) · 𝑇)) = 𝐵)
206	98, 182, 205	3eqtrd 2648	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = 𝐵)
207		fourierdlem51.bc	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
208	207	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐵 ∈ 𝐶)
209	206, 208	eqeltrd 2688	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
210	209	3adantl3 1212	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
211		simpl1 1057	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝜑 ∧ 𝑥 ∈ ℝ))
212		simpl2 1058	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 ∈ ℤ)
213		fourierdlem51.css	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ⊆ (𝐴[,]𝐵))
214	213	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
215	214	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
216	215	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
217	216	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
218		neqne 2790	. . . . . . . . . . . . . . . . . . . . . 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 788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℝ)
224	223, 130	readdcld 9948	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ)
225	224	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ^*)
226	211, 212, 225	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ^*)
227	221, 222, 226	eliccelioc 38594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵) ∧ (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)))
228	217, 219, 227	mpbir2and 959	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵))
229	97	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
230	1	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
231	4	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ)
232	22	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐵)
233		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ)
234	92	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
235		simplr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝑘 ∈ ℤ)
236	97, 113	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
237	236	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
238		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵))
239	230, 231, 232, 19, 233, 234, 235, 237, 238	fourierdlem35 39035	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = 𝑘)
240	239	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = (𝑘 · 𝑇))
241	240	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
242	229, 241	eqtrd 2644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑥) = (𝑥 + (𝑘 · 𝑇)))
243	211, 212, 228, 242	syl21anc 1317	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = (𝑥 + (𝑘 · 𝑇)))
244		simpl3 1059	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
245	243, 244	eqeltrd 2688	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
246	210, 245	pm2.61dan 828	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝐸‘𝑥) ∈ 𝐶)
247	246	3exp 1256	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑘 ∈ ℤ → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶)))
248	78, 85, 247	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (𝑘 ∈ ℤ → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶)))
249	76, 77, 248	rexlimd 3008	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶))
250	70, 249	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (𝐸‘𝑥) ∈ 𝐶)
251	64, 250	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) ∈ 𝐶)
252		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)) = (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥))
253	251, 252	fmptd 6292	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶)
254		iocssre 12124	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
255	102, 4, 254	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
256	112, 255	fssd 5970	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:ℝ⟶ℝ)
257		ssrab2 3650	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))
258	257, 81	syl5ss 3579	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ℝ)
259	256, 258	fssresd 5984	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶ℝ)
260	259	feqmptd 6159	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) = (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)))
261	260	feq1d 5943	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶 ↔ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶))
262	253, 261	mpbird 246	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶)
263		simplll 794	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝜑)
264		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
265		fourierdlem51.h	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
266	264, 265	syl6eleqr 2699	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑤 ∈ 𝐻)
267	266	ad3antlr 763	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑤 ∈ 𝐻)
268	263, 267	jca 553	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝜑 ∧ 𝑤 ∈ 𝐻))
269		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
270	269, 265	syl6eleqr 2699	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑧 ∈ 𝐻)
271	270	ad2antlr 759	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑧 ∈ 𝐻)
272		fvres 6117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = (𝐸‘𝑧))
273	272	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → (𝐸‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
274	273	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝐸‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
275		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
276	275	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤))
277	276	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤))
278		fvres 6117	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = (𝐸‘𝑤))
279	278	ad3antlr 763	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = (𝐸‘𝑤))
280	274, 277, 279	3eqtrd 2648	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝐸‘𝑧) = (𝐸‘𝑤))
281	1	ad3antrrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐴 ∈ ℝ)
282	4	ad3antrrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐵 ∈ ℝ)
283	22	ad3antrrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐴 < 𝐵)
284	2	ad3antrrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑋 ∈ ℝ)
285		simpllr 795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 ∈ 𝐻)
286		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑧 ∈ 𝐻)
287		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝐸‘𝑧) = (𝐸‘𝑤))
288	281, 282, 283, 284, 265, 19, 31, 285, 286, 287	fourierdlem19 39019	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → ¬ 𝑤 < 𝑧)
289	287	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝐸‘𝑤) = (𝐸‘𝑧))
290	281, 282, 283, 284, 265, 19, 31, 286, 285, 289	fourierdlem19 39019	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → ¬ 𝑧 < 𝑤)
291	265, 258	syl5eqss 3612	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
292	291	sselda 3568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐻) → 𝑤 ∈ ℝ)
293	292	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 ∈ ℝ)
294	291	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐻) → 𝐻 ⊆ ℝ)
295	294	sselda 3568	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) → 𝑧 ∈ ℝ)
296	295	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑧 ∈ ℝ)
297	293, 296	lttri3d 10056	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝑤 = 𝑧 ↔ (¬ 𝑤 < 𝑧 ∧ ¬ 𝑧 < 𝑤)))
298	288, 290, 297	mpbir2and 959	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 = 𝑧)
299	268, 271, 280, 298	syl21anc 1317	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑤 = 𝑧)
300	299	ex 449	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
301	300	ralrimiva 2949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
302	301	ralrimiva 2949	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
303		dff13 6416	. . . . . . . . . 10 ⊢ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶 ↔ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶 ∧ ∀𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧)))
304	262, 302, 303	sylanbrc 695	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶)
305		f1fi 8136	. . . . . . . . 9 ⊢ ((𝐶 ∈ Fin ∧ (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶) → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
306	62, 304, 305	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
307		unfi 8112	. . . . . . . 8 ⊢ (({(𝐴 + 𝑋)} ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin) → ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
308	61, 306, 307	sylancr 694	. . . . . . 7 ⊢ (𝜑 → ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
309		simpl 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝜑)
310		elrabi 3328	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
311	310	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
312	67	elrab 3331	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
313	312	simprbi 479	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
314	313	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
315		velsn 4141	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐴 + 𝑋)} ↔ 𝑥 = (𝐴 + 𝑋))
316		elun1 3742	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐴 + 𝑋)} → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
317	315, 316	sylbir 224	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 + 𝑋) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
318	317	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
319	79	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ∈ ℝ^*)
320	5	rexrd 9968	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ^*)
321	320	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐵 + 𝑋) ∈ ℝ^*)
322	3, 5	iccssred 38574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ⊆ ℝ)
323	322	sselda 3568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ℝ)
324	323	rexrd 9968	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ℝ^*)
325	324	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ℝ^*)
326	3	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ∈ ℝ)
327	323	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ℝ)
328	79	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ∈ ℝ^*)
329	320	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐵 + 𝑋) ∈ ℝ^*)
330		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
331		iccgelb 12101	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ^* ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ≤ 𝑥)
332	328, 329, 330, 331	syl3anc 1318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ≤ 𝑥)
333	332	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ≤ 𝑥)
334		neqne 2790	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 = (𝐴 + 𝑋) → 𝑥 ≠ (𝐴 + 𝑋))
335	334	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ≠ (𝐴 + 𝑋))
336	326, 327, 333, 335	leneltd 10070	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) < 𝑥)
337		iccleub 12100	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ^* ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ≤ (𝐵 + 𝑋))
338	328, 329, 330, 337	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ≤ (𝐵 + 𝑋))
339	338	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ≤ (𝐵 + 𝑋))
340	319, 321, 325, 336, 339	eliocd 38577	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
341	340	adantlr 747	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
342		simplr 788	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
343	341, 342, 68	sylanbrc 695	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
344		elun2 3743	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
345	343, 344	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
346	318, 345	pm2.61dan 828	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
347	309, 311, 314, 346	syl21anc 1317	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
348	347	ralrimiva 2949	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
349		dfss3 3558	. . . . . . . 8 ⊢ ({𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ↔ ∀𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
350	348, 349	sylibr 223	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
351		ssfi 8065	. . . . . . 7 ⊢ ((({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})) → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
352	308, 350, 351	syl2anc 691	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
353		unfi 8112	. . . . . 6 ⊢ (({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin) → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
354	60, 352, 353	sylancr 694	. . . . 5 ⊢ (𝜑 → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
355	58, 354	syl5eqel 2692	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Fin)
356		prssi 4293	. . . . . . 7 ⊢ (((𝐴 + 𝑋) ∈ ℝ ∧ (𝐵 + 𝑋) ∈ ℝ) → {(𝐴 + 𝑋), (𝐵 + 𝑋)} ⊆ ℝ)
357	3, 5, 356	syl2anc 691	. . . . . 6 ⊢ (𝜑 → {(𝐴 + 𝑋), (𝐵 + 𝑋)} ⊆ ℝ)
358		ssrab2 3650	. . . . . . 7 ⊢ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))
359	358, 322	syl5ss 3579	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ℝ)
360	357, 359	unssd 3751	. . . . 5 ⊢ (𝜑 → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ⊆ ℝ)
361	58, 360	syl5eqss 3612	. . . 4 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
362		fourierdlem51.f	. . . 4 ⊢ 𝐹 = (℩𝑓𝑓 Isom < , < ((0...((#‘𝐷) − 1)), 𝐷))
363		eqid 2610	. . . 4 ⊢ ((#‘𝐷) − 1) = ((#‘𝐷) − 1)
364	355, 361, 362, 363	fourierdlem36 39036	. . 3 ⊢ (𝜑 → 𝐹 Isom < , < ((0...((#‘𝐷) − 1)), 𝐷))
365		isof1o 6473	. . . 4 ⊢ (𝐹 Isom < , < ((0...((#‘𝐷) − 1)), 𝐷) → 𝐹:(0...((#‘𝐷) − 1))–1-1-onto→𝐷)
366		f1ofo 6057	. . . 4 ⊢ (𝐹:(0...((#‘𝐷) − 1))–1-1-onto→𝐷 → 𝐹:(0...((#‘𝐷) − 1))–onto→𝐷)
367	365, 366	syl 17	. . 3 ⊢ (𝐹 Isom < , < ((0...((#‘𝐷) − 1)), 𝐷) → 𝐹:(0...((#‘𝐷) − 1))–onto→𝐷)
368		forn 6031	. . 3 ⊢ (𝐹:(0...((#‘𝐷) − 1))–onto→𝐷 → ran 𝐹 = 𝐷)
369	364, 367, 368	3syl 18	. 2 ⊢ (𝜑 → ran 𝐹 = 𝐷)
370	59, 369	eleqtrrd 2691	1 ⊢ (𝜑 → 𝑋 ∈ ran 𝐹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ∪ cun 3538 ⊆ wss 3540 {csn 4125 {cpr 4127 class class class wbr 4583 ↦ cmpt 4643 ran crn 5039 ↾ cres 5040 ℩cio 5766 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 Isom wiso 5805 (class class class)co 6549 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℤcz 11254 ℝ⁺crp 11708 (,]cioc 12047 [,]cicc 12049 ...cfz 12197 ⌊cfl 12453 #chash 12979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-ioc 12051 df-icc 12053 df-fz 12198 df-fl 12455 df-hash 12980

This theorem is referenced by: fourierdlem113 39112

W3C validator