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 43698

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 11004	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ)
4		fourierdlem51.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5	4, 2	readdcld 11004	. . . . . 6 ⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ)
6		0red 10978	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
7		fourierdlem51.alt0	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < 0)
8	1, 6, 2, 7	ltadd1dd 11586	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 𝑋) < (0 + 𝑋))
9	2	recnd 11003	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ℂ)
10	9	addid2d 11176	. . . . . . . 8 ⊢ (𝜑 → (0 + 𝑋) = 𝑋)
11	8, 10	breqtrd 5100	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝑋) < 𝑋)
12	3, 2, 11	ltled 11123	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝑋) ≤ 𝑋)
13		fourierdlem51.bgt0	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝐵)
14	6, 4, 2, 13	ltadd1dd 11586	. . . . . . . 8 ⊢ (𝜑 → (0 + 𝑋) < (𝐵 + 𝑋))
15	10, 14	eqbrtrrd 5098	. . . . . . 7 ⊢ (𝜑 → 𝑋 < (𝐵 + 𝑋))
16	2, 5, 15	ltled 11123	. . . . . 6 ⊢ (𝜑 → 𝑋 ≤ (𝐵 + 𝑋))
17	3, 5, 2, 12, 16	eliccd 43042	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
18	4, 2	resubcld 11403	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
19		fourierdlem51.t	. . . . . . . . 9 ⊢ 𝑇 = (𝐵 − 𝐴)
20	4, 1	resubcld 11403	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
21	19, 20	eqeltrid 2843	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℝ)
22	1, 6, 4, 7, 13	lttrd 11136	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
23	1, 4	posdifd 11562	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
24	22, 23	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
25	19	eqcomi 2747	. . . . . . . . . . 11 ⊢ (𝐵 − 𝐴) = 𝑇
26	25	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
27	24, 26	breqtrd 5100	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝑇)
28	27	gt0ne0d 11539	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ≠ 0)
29	18, 21, 28	redivcld 11803	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
30	29	flcld 13518	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
31		fourierdlem51.e	. . . . . . . . 9 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
32	31	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
33		id 22	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
34		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
35	34	oveq1d 7290	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
36	35	fveq2d 6778	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
37	36	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
38	33, 37	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
39	38	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
40	30	zred 12426	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
41	40, 21	remulcld 11005	. . . . . . . . 9 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
42	2, 41	readdcld 11004	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
43	32, 39, 2, 42	fvmptd 6882	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
44		fourierdlem51.exc	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐶)
45	43, 44	eqeltrrd 2840	. . . . . 6 ⊢ (𝜑 → (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶)
46		oveq1 7282	. . . . . . . . 9 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
47	46	oveq2d 7291	. . . . . . . 8 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑋 + (𝑘 · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
48	47	eleq1d 2823	. . . . . . 7 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑋 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶))
49	48	rspcev 3561	. . . . . 6 ⊢ (((⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ ∧ (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶) → ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶)
50	30, 45, 49	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶)
51		oveq1 7282	. . . . . . . 8 ⊢ (𝑦 = 𝑋 → (𝑦 + (𝑘 · 𝑇)) = (𝑋 + (𝑘 · 𝑇)))
52	51	eleq1d 2823	. . . . . . 7 ⊢ (𝑦 = 𝑋 → ((𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
53	52	rexbidv 3226	. . . . . 6 ⊢ (𝑦 = 𝑋 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
54	53	elrab 3624	. . . . 5 ⊢ (𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑋 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
55	17, 50, 54	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
56		elun2 4111	. . . 4 ⊢ (𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑋 ∈ ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
57	55, 56	syl 17	. . 3 ⊢ (𝜑 → 𝑋 ∈ ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
58		fourierdlem51.d	. . 3 ⊢ 𝐷 = ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
59	57, 58	eleqtrrdi 2850	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
60		prfi 9089	. . . . . 6 ⊢ {(𝐴 + 𝑋), (𝐵 + 𝑋)} ∈ Fin
61		snfi 8834	. . . . . . . 8 ⊢ {(𝐴 + 𝑋)} ∈ Fin
62		fourierdlem51.cfi	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ Fin)
63		fvres 6793	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) = (𝐸‘𝑥))
64	63	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) = (𝐸‘𝑥))
65		oveq1 7282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
66	65	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
67	66	rexbidv 3226	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
68	67	elrab 3624	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
69	68	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
70	69	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
71		nfv 1917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
72		nfre1 3239	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶
73		nfcv 2907	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐴 + 𝑋)(,](𝐵 + 𝑋))
74	72, 73	nfrabw 3318	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
75	74	nfcri 2894	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
76	71, 75	nfan 1902	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
77		nfv 1917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐸‘𝑥) ∈ 𝐶
78		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝜑)
79	3	rexrd 11025	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ^*)
80		iocssre 13159	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
81	79, 5, 80	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
82	81	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
83		elrabi 3618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
84	83	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
85	82, 84	sseldd 3922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ℝ)
86		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
87	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
88	87, 86	resubcld 11403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
89	21	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
90	28	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
91	88, 89, 90	redivcld 11803	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
92	91	flcld 13518	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
93	92	zred 12426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
94	93, 89	remulcld 11005	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
95	86, 94	readdcld 11004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
96	31	fvmpt2 6886	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
97	86, 95, 96	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
98	97	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
99		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ))
100	92	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
101		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) = 𝐴)
102	1	rexrd 11025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
103	4	rexrd 11025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
104	1, 4, 22	ltled 11123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
105		lbicc2 13196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
106	102, 103, 104, 105	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
107	106	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 ∈ (𝐴[,]𝐵))
108	101, 107	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
109	108	ad4ant14 749	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
110	99, 100, 109	jca31 515	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)))
111		iocssicc 13169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
112	1, 4, 22, 19, 31	fourierdlem4 43652	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
113	112	ffvelrnda 6961	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
114	111, 113	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴[,]𝐵))
115	97, 114	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))
116	115	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))
117	102	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ^*)
118	87	rexrd 11025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ^*)
119		iocgtlb 43040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑥))
120	117, 118, 113, 119	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥))
121	120	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 < (𝐸‘𝑥))
122		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → (𝑥 + (𝑘 · 𝑇)) = 𝐴)
123	122	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → 𝐴 = (𝑥 + (𝑘 · 𝑇)))
124	123	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 = (𝑥 + (𝑘 · 𝑇)))
125	121, 124, 98	3brtr3d 5105	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
126		zre 12323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
127	126	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
128	21	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
129	127, 128	remulcld 11005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
130	129	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
131	130	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 · 𝑇) ∈ ℝ)
132	94	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
133		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑥 ∈ ℝ)
134	131, 132, 133	ltadd2d 11131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ↔ (𝑥 + (𝑘 · 𝑇)) < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
135	125, 134	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
136	126	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 ∈ ℝ)
137	93	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
138	21, 27	elrpd 12769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
139	138	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑇 ∈ ℝ⁺)
140	136, 137, 139	ltmul1d 12813	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)) ↔ (𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
141	135, 140	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)))
142		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ V
143		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ))
144	143	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ↔ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)))
145	144	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))))
146		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
147	146	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑥 + (𝑗 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
148	147	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵) ↔ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)))
149	145, 148	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))))
150		breq2 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 < 𝑗 ↔ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))))
151	149, 150	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) ↔ ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)))))
152		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 = (𝑘 + 1) ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1)))
153	151, 152	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1)) ↔ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))))
154		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ ℤ ↔ 𝑘 ∈ ℤ))
155	154	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ↔ ((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ)))
156	155	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ↔ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ)))
157		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑘 → (𝑖 · 𝑇) = (𝑘 · 𝑇))
158	157	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑘 → (𝑥 + (𝑖 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
159	158	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑘 → ((𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵) ↔ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)))
160	156, 159	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑘 → (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))))
161	160	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵))))
162		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → (𝑖 < 𝑗 ↔ 𝑘 < 𝑗))
163	161, 162	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑘 → (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) ↔ ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗)))
164		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
165	164	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑘 → (𝑗 = (𝑖 + 1) ↔ 𝑗 = (𝑘 + 1)))
166	163, 165	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = 𝑘 → ((((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 = (𝑖 + 1)) ↔ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1))))
167		simp-6l 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝜑)
168	167, 1	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐴 ∈ ℝ)
169	167, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐵 ∈ ℝ)
170	167, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐴 < 𝐵)
171		simp-6r 785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑥 ∈ ℝ)
172		simp-5r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
173		simp-4r 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
174		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
175		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵))
176		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵))
177	168, 169, 170, 19, 171, 172, 173, 174, 175, 176	fourierdlem6 43654	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 = (𝑖 + 1))
178	166, 177	chvarvv 2002	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1))
179	142, 153, 178	vtocl 3498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))
180	110, 116, 141, 179	syl21anc 835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))
181	180	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((𝑘 + 1) · 𝑇))
182	181	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((𝑘 + 1) · 𝑇)))
183	127	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
184	21	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
185	184	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℂ)
186	183, 185	adddirp1d 11001	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → ((𝑘 + 1) · 𝑇) = ((𝑘 · 𝑇) + 𝑇))
187	186	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
188	187	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
189	188	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
190	86	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
191	190	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℂ)
192	130	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℂ)
193	184	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℂ)
194	191, 192, 193	addassd 10997	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
195	194	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 · 𝑇) + 𝑇)) = ((𝑥 + (𝑘 · 𝑇)) + 𝑇))
196	195	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 · 𝑇) + 𝑇)) = ((𝑥 + (𝑘 · 𝑇)) + 𝑇))
197		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝐴 + 𝑇))
198	197	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝐴 + 𝑇))
199	4	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐵 ∈ ℂ)
200	1	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 ∈ ℂ)
201	199, 200, 184	subaddd 11350	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐵 − 𝐴) = 𝑇 ↔ (𝐴 + 𝑇) = 𝐵))
202	26, 201	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
203	202	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐴 + 𝑇) = 𝐵)
204	198, 203	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = 𝐵)
205	189, 196, 204	3eqtrd 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 + 1) · 𝑇)) = 𝐵)
206	98, 182, 205	3eqtrd 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = 𝐵)
207		fourierdlem51.bc	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
208	207	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐵 ∈ 𝐶)
209	206, 208	eqeltrd 2839	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
210	209	3adantl3 1167	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
211		simpl1 1190	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝜑 ∧ 𝑥 ∈ ℝ))
212		simpl2 1191	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 ∈ ℤ)
213		fourierdlem51.css	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ⊆ (𝐴[,]𝐵))
214	213	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
215	214	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
216	215	3adant2 1130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
217	216	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
218		neqne 2951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴 → (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)
219	218	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)
220	1	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
221	211, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 ∈ ℝ)
222	211, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐵 ∈ ℝ)
223		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℝ)
224	223, 130	readdcld 11004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ)
225	224	rexrd 11025	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ^*)
226	211, 212, 225	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ^*)
227	221, 222, 226	eliccelioc 43059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵) ∧ (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)))
228	217, 219, 227	mpbir2and 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵))
229	97	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
230	1	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
231	4	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ)
232	22	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐵)
233		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ)
234	92	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
235		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝑘 ∈ ℤ)
236	97, 113	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
237	236	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
238		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵))
239	230, 231, 232, 19, 233, 234, 235, 237, 238	fourierdlem35 43683	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = 𝑘)
240	239	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = (𝑘 · 𝑇))
241	240	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
242	229, 241	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑥) = (𝑥 + (𝑘 · 𝑇)))
243	211, 212, 228, 242	syl21anc 835	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = (𝑥 + (𝑘 · 𝑇)))
244		simpl3 1192	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
245	243, 244	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
246	210, 245	pm2.61dan 810	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝐸‘𝑥) ∈ 𝐶)
247	246	3exp 1118	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑘 ∈ ℤ → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶)))
248	78, 85, 247	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (𝑘 ∈ ℤ → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶)))
249	76, 77, 248	rexlimd 3250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶))
250	70, 249	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (𝐸‘𝑥) ∈ 𝐶)
251	64, 250	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) ∈ 𝐶)
252		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)) = (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥))
253	251, 252	fmptd 6988	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶)
254		iocssre 13159	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
255	102, 4, 254	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
256	112, 255	fssd 6618	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:ℝ⟶ℝ)
257		ssrab2 4013	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))
258	257, 81	sstrid 3932	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ℝ)
259	256, 258	fssresd 6641	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶ℝ)
260	259	feqmptd 6837	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) = (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)))
261	260	feq1d 6585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶 ↔ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶))
262	253, 261	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶)
263		simplll 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝜑)
264		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
265		fourierdlem51.h	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
266	264, 265	eleqtrrdi 2850	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑤 ∈ 𝐻)
267	266	ad3antlr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑤 ∈ 𝐻)
268	263, 267	jca 512	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝜑 ∧ 𝑤 ∈ 𝐻))
269		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
270	269, 265	eleqtrrdi 2850	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑧 ∈ 𝐻)
271	270	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑧 ∈ 𝐻)
272		fvres 6793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = (𝐸‘𝑧))
273	272	eqcomd 2744	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → (𝐸‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
274	273	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝐸‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
275		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
276	275	eqcomd 2744	. . . . . . . . . . . . . . . 16 ⊢ (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤))
277	276	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤))
278		fvres 6793	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = (𝐸‘𝑤))
279	278	ad3antlr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = (𝐸‘𝑤))
280	274, 277, 279	3eqtrd 2782	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝐸‘𝑧) = (𝐸‘𝑤))
281	1	ad3antrrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐴 ∈ ℝ)
282	4	ad3antrrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐵 ∈ ℝ)
283	22	ad3antrrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐴 < 𝐵)
284	2	ad3antrrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑋 ∈ ℝ)
285		simpllr 773	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 ∈ 𝐻)
286		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑧 ∈ 𝐻)
287		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝐸‘𝑧) = (𝐸‘𝑤))
288	281, 282, 283, 284, 265, 19, 31, 285, 286, 287	fourierdlem19 43667	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → ¬ 𝑤 < 𝑧)
289	287	eqcomd 2744	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝐸‘𝑤) = (𝐸‘𝑧))
290	281, 282, 283, 284, 265, 19, 31, 286, 285, 289	fourierdlem19 43667	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → ¬ 𝑧 < 𝑤)
291	265, 258	eqsstrid 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
292	291	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐻) → 𝑤 ∈ ℝ)
293	292	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 ∈ ℝ)
294	291	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐻) → 𝐻 ⊆ ℝ)
295	294	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) → 𝑧 ∈ ℝ)
296	295	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑧 ∈ ℝ)
297	293, 296	lttri3d 11115	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝑤 = 𝑧 ↔ (¬ 𝑤 < 𝑧 ∧ ¬ 𝑧 < 𝑤)))
298	288, 290, 297	mpbir2and 710	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 = 𝑧)
299	268, 271, 280, 298	syl21anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑤 = 𝑧)
300	299	ex 413	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
301	300	ralrimiva 3103	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
302	301	ralrimiva 3103	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
303		dff13 7128	. . . . . . . . . 10 ⊢ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶 ↔ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶 ∧ ∀𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧)))
304	262, 302, 303	sylanbrc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶)
305		f1fi 9106	. . . . . . . . 9 ⊢ ((𝐶 ∈ Fin ∧ (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶) → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
306	62, 304, 305	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
307		unfi 8955	. . . . . . . 8 ⊢ (({(𝐴 + 𝑋)} ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin) → ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
308	61, 306, 307	sylancr 587	. . . . . . 7 ⊢ (𝜑 → ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
309		simpl 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝜑)
310		elrabi 3618	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
311	310	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
312	67	elrab 3624	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
313	312	simprbi 497	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
314	313	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
315		velsn 4577	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐴 + 𝑋)} ↔ 𝑥 = (𝐴 + 𝑋))
316		elun1 4110	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐴 + 𝑋)} → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
317	315, 316	sylbir 234	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 + 𝑋) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
318	317	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
319	79	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ∈ ℝ^*)
320	5	rexrd 11025	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ^*)
321	320	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐵 + 𝑋) ∈ ℝ^*)
322	3, 5	iccssred 13166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ⊆ ℝ)
323	322	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ℝ)
324	323	rexrd 11025	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ℝ^*)
325	324	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ℝ^*)
326	3	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ∈ ℝ)
327	323	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ℝ)
328	79	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ∈ ℝ^*)
329	320	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐵 + 𝑋) ∈ ℝ^*)
330		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
331		iccgelb 13135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ^* ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ≤ 𝑥)
332	328, 329, 330, 331	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ≤ 𝑥)
333	332	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ≤ 𝑥)
334		neqne 2951	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 = (𝐴 + 𝑋) → 𝑥 ≠ (𝐴 + 𝑋))
335	334	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ≠ (𝐴 + 𝑋))
336	326, 327, 333, 335	leneltd 11129	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) < 𝑥)
337		iccleub 13134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ^* ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ≤ (𝐵 + 𝑋))
338	328, 329, 330, 337	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ≤ (𝐵 + 𝑋))
339	338	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ≤ (𝐵 + 𝑋))
340	319, 321, 325, 336, 339	eliocd 43045	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
341	340	adantlr 712	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
342		simplr 766	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
343	341, 342, 68	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
344		elun2 4111	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
345	343, 344	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
346	318, 345	pm2.61dan 810	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
347	309, 311, 314, 346	syl21anc 835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
348	347	ralrimiva 3103	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
349		dfss3 3909	. . . . . . . 8 ⊢ ({𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ↔ ∀𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
350	348, 349	sylibr 233	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
351		ssfi 8956	. . . . . . 7 ⊢ ((({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})) → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
352	308, 350, 351	syl2anc 584	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
353		unfi 8955	. . . . . 6 ⊢ (({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin) → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
354	60, 352, 353	sylancr 587	. . . . 5 ⊢ (𝜑 → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
355	58, 354	eqeltrid 2843	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Fin)
356		prssi 4754	. . . . . . 7 ⊢ (((𝐴 + 𝑋) ∈ ℝ ∧ (𝐵 + 𝑋) ∈ ℝ) → {(𝐴 + 𝑋), (𝐵 + 𝑋)} ⊆ ℝ)
357	3, 5, 356	syl2anc 584	. . . . . 6 ⊢ (𝜑 → {(𝐴 + 𝑋), (𝐵 + 𝑋)} ⊆ ℝ)
358		ssrab2 4013	. . . . . . 7 ⊢ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))
359	358, 322	sstrid 3932	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ℝ)
360	357, 359	unssd 4120	. . . . 5 ⊢ (𝜑 → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ⊆ ℝ)
361	58, 360	eqsstrid 3969	. . . 4 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
362		fourierdlem51.f	. . . 4 ⊢ 𝐹 = (℩𝑓𝑓 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷))
363		eqid 2738	. . . 4 ⊢ ((♯‘𝐷) − 1) = ((♯‘𝐷) − 1)
364	355, 361, 362, 363	fourierdlem36 43684	. . 3 ⊢ (𝜑 → 𝐹 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷))
365		isof1o 7194	. . . 4 ⊢ (𝐹 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷) → 𝐹:(0...((♯‘𝐷) − 1))–1-1-onto→𝐷)
366		f1ofo 6723	. . . 4 ⊢ (𝐹:(0...((♯‘𝐷) − 1))–1-1-onto→𝐷 → 𝐹:(0...((♯‘𝐷) − 1))–onto→𝐷)
367	365, 366	syl 17	. . 3 ⊢ (𝐹 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷) → 𝐹:(0...((♯‘𝐷) − 1))–onto→𝐷)
368		forn 6691	. . 3 ⊢ (𝐹:(0...((♯‘𝐷) − 1))–onto→𝐷 → ran 𝐹 = 𝐷)
369	364, 367, 368	3syl 18	. 2 ⊢ (𝜑 → ran 𝐹 = 𝐷)
370	59, 369	eleqtrrd 2842	1 ⊢ (𝜑 → 𝑋 ∈ ran 𝐹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 ∪ cun 3885 ⊆ wss 3887 {csn 4561 {cpr 4563 class class class wbr 5074 ↦ cmpt 5157 ran crn 5590 ↾ cres 5591 ℩cio 6389 ⟶wf 6429 –1-1→wf1 6430 –onto→wfo 6431 –1-1-onto→wf1o 6432 ‘cfv 6433 Isom wiso 6434 (class class class)co 7275 Fincfn 8733 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 ℤcz 12319 ℝ⁺crp 12730 (,]cioc 13080 [,]cicc 13082 ...cfz 13239 ⌊cfl 13510 ♯chash 14044

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-oi 9269 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-ioc 13084 df-icc 13086 df-fz 13240 df-fl 13512 df-hash 14045

This theorem is referenced by: fourierdlem113 43760

W3C validator