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 47274

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 11343	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ)
4		fourierdlem51.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5	4, 2	readdcld 11343	. . . . . 6 ⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ)
6		0red 11316	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
7		fourierdlem51.alt0	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < 0)
8	1, 6, 2, 7	ltadd1dd 11932	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 𝑋) < (0 + 𝑋))
9	2	recnd 11342	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ℂ)
10	9	addlidd 11516	. . . . . . . 8 ⊢ (𝜑 → (0 + 𝑋) = 𝑋)
11	8, 10	breqtrd 5130	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝑋) < 𝑋)
12	3, 2, 11	ltled 11463	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝑋) ≤ 𝑋)
13		fourierdlem51.bgt0	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝐵)
14	6, 4, 2, 13	ltadd1dd 11932	. . . . . . . 8 ⊢ (𝜑 → (0 + 𝑋) < (𝐵 + 𝑋))
15	10, 14	eqbrtrrd 5128	. . . . . . 7 ⊢ (𝜑 → 𝑋 < (𝐵 + 𝑋))
16	2, 5, 15	ltled 11463	. . . . . 6 ⊢ (𝜑 → 𝑋 ≤ (𝐵 + 𝑋))
17	3, 5, 2, 12, 16	eliccd 46623	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
18	4, 2	resubcld 11749	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
19		fourierdlem51.t	. . . . . . . . 9 ⊢ 𝑇 = (𝐵 − 𝐴)
20	4, 1	resubcld 11749	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
21	19, 20	eqeltrid 2864	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℝ)
22	1, 6, 4, 7, 13	lttrd 11476	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
23	1, 4	posdifd 11908	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
24	22, 23	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
25	19	eqcomi 2769	. . . . . . . . . . 11 ⊢ (𝐵 − 𝐴) = 𝑇
26	25	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
27	24, 26	breqtrd 5130	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝑇)
28	27	gt0ne0d 11885	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ≠ 0)
29	18, 21, 28	redivcld 12150	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
30	29	flcld 13943	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
31		fourierdlem51.e	. . . . . . . . 9 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
32	31	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
33		id 23	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
34		oveq2 7430	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
35	34	oveq1d 7437	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
36	35	fveq2d 6892	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
37	36	oveq1d 7437	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
38	33, 37	oveq12d 7440	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
39	38	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
40	30	zred 12808	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
41	40, 21	remulcld 11344	. . . . . . . . 9 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
42	2, 41	readdcld 11343	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
43	32, 39, 2, 42	fvmptd 7004	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
44		fourierdlem51.exc	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐶)
45	43, 44	eqeltrrd 2861	. . . . . 6 ⊢ (𝜑 → (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶)
46		oveq1 7429	. . . . . . . . 9 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
47	46	oveq2d 7438	. . . . . . . 8 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑋 + (𝑘 · 𝑇)) = (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
48	47	eleq1d 2845	. . . . . . 7 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑋 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶))
49	48	rspcev 3576	. . . . . 6 ⊢ (((⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ ∧ (𝑋 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐶) → ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶)
50	30, 45, 49	syl2anc 596	. . . . 5 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶)
51		oveq1 7429	. . . . . . . 8 ⊢ (𝑦 = 𝑋 → (𝑦 + (𝑘 · 𝑇)) = (𝑋 + (𝑘 · 𝑇)))
52	51	eleq1d 2845	. . . . . . 7 ⊢ (𝑦 = 𝑋 → ((𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
53	52	rexbidv 3186	. . . . . 6 ⊢ (𝑦 = 𝑋 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
54	53	elrab 3644	. . . . 5 ⊢ (𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑋 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑋 + (𝑘 · 𝑇)) ∈ 𝐶))
55	17, 50, 54	sylanbrc 595	. . . 4 ⊢ (𝜑 → 𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
56		elun2 4180	. . . 4 ⊢ (𝑋 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑋 ∈ ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
57	55, 56	syl 18	. . 3 ⊢ (𝜑 → 𝑋 ∈ ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
58		fourierdlem51.d	. . 3 ⊢ 𝐷 = ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
59	57, 58	eleqtrrdi 2871	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
60		prfi 9320	. . . . . 6 ⊢ {(𝐴 + 𝑋), (𝐵 + 𝑋)} ∈ Fin
61		snfi 9076	. . . . . . . 8 ⊢ {(𝐴 + 𝑋)} ∈ Fin
62		fourierdlem51.cfi	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ Fin)
63		fvres 6907	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) = (𝐸‘𝑥))
64	63	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) = (𝐸‘𝑥))
65		oveq1 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
66	65	eleq1d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
67	66	rexbidv 3186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
68	67	elrab 3644	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
69	68	simprbi 503	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
70	69	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
71		nfv 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
72		nfre1 3287	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶
73		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐴 + 𝑋)(,](𝐵 + 𝑋))
74	72, 73	nfrabw 3447	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
75	74	nfcri 2914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
76	71, 75	nfan 1931	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
77		nfv 1946	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐸‘𝑥) ∈ 𝐶
78		simpl 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝜑)
79	3	rexrd 11364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ^*)
80		iocssre 13563	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
81	79, 5, 80	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
82	81	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ)
83		elrabi 3640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
84	83	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
85	82, 84	sseldd 3910	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ℝ)
86		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
87	4	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
88	87, 86	resubcld 11749	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
89	21	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
90	28	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
91	88, 89, 90	redivcld 12150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
92	91	flcld 13943	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
93	92	zred 12808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
94	93, 89	remulcld 11344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
95	86, 94	readdcld 11343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
96	31	fvmpt2 7008	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
97	86, 95, 96	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
98	97	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
99		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ))
100	92	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
101		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) = 𝐴)
102	1	rexrd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
103	4	rexrd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
104	1, 4, 22	ltled 11463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
105		lbicc2 13600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
106	102, 103, 104, 105	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
107	106	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 ∈ (𝐴[,]𝐵))
108	101, 107	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
109	108	ad4ant14 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
110	99, 100, 109	jca31 524	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)))
111		iocssicc 13573	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
112	1, 4, 22, 19, 31	fourierdlem4 47228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
113	112	ffvelcdmda 7087	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
114	111, 113	sselid 3907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴[,]𝐵))
115	97, 114	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))
116	115	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))
117	102	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ^*)
118	87	rexrd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ^*)
119		iocgtlb 46621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑥))
120	117, 118, 113, 119	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥))
121	120	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 < (𝐸‘𝑥))
122		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → (𝑥 + (𝑘 · 𝑇)) = 𝐴)
123	122	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → 𝐴 = (𝑥 + (𝑘 · 𝑇)))
124	123	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 = (𝑥 + (𝑘 · 𝑇)))
125	121, 124, 98	3brtr3d 5135	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
126		zre 12702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
127	126	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
128	21	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
129	127, 128	remulcld 11344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
130	129	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
131	130	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 · 𝑇) ∈ ℝ)
132	94	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
133		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑥 ∈ ℝ)
134	131, 132, 133	ltadd2d 11471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ↔ (𝑥 + (𝑘 · 𝑇)) < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
135	125, 134	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
136	126	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 ∈ ℝ)
137	93	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
138	21, 27	elrpd 13166	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
139	138	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑇 ∈ ℝ⁺)
140	136, 137, 139	ltmul1d 13210	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)) ↔ (𝑘 · 𝑇) < ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
141	135, 140	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)))
142		fvex 6901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ V
143		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ))
144	143	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ↔ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)))
145	144	anbi1d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))))
146		oveq1 7429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
147	146	oveq2d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑥 + (𝑗 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
148	147	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵) ↔ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)))
149	145, 148	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵))))
150		breq2 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 < 𝑗 ↔ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))))
151	149, 150	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) ↔ ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇)))))
152		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑗 = (𝑘 + 1) ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1)))
153	151, 152	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1)) ↔ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))))
154		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ ℤ ↔ 𝑘 ∈ ℤ))
155	154	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ↔ ((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ)))
156	155	anbi1d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ↔ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ)))
157		oveq1 7429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑘 → (𝑖 · 𝑇) = (𝑘 · 𝑇))
158	157	oveq2d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑘 → (𝑥 + (𝑖 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
159	158	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑘 → ((𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵) ↔ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)))
160	156, 159	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑘 → (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))))
161	160	anbi1d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵))))
162		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → (𝑖 < 𝑗 ↔ 𝑘 < 𝑗))
163	161, 162	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑘 → (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) ↔ ((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗)))
164		oveq1 7429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
165	164	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑘 → (𝑗 = (𝑖 + 1) ↔ 𝑗 = (𝑘 + 1)))
166	163, 165	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = 𝑘 → ((((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 = (𝑖 + 1)) ↔ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1))))
167		simp-6l 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝜑)
168	167, 1	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐴 ∈ ℝ)
169	167, 4	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐵 ∈ ℝ)
170	167, 22	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝐴 < 𝐵)
171		simp-6r 800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑥 ∈ ℝ)
172		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
173		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
174		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
175		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵))
176		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵))
177	168, 169, 170, 19, 171, 172, 173, 174, 175, 176	fourierdlem6 47230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑖 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑖 < 𝑗) → 𝑗 = (𝑖 + 1))
178	166, 177	chvarvv 2021	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ 𝑗 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + (𝑗 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < 𝑗) → 𝑗 = (𝑘 + 1))
179	142, 153, 178	vtocl 3520	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴[,]𝐵)) ∧ 𝑘 < (⌊‘((𝐵 − 𝑥) / 𝑇))) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))
180	110, 116, 141, 179	syl21anc 851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (𝑘 + 1))
181	180	oveq1d 7437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((𝑘 + 1) · 𝑇))
182	181	oveq2d 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((𝑘 + 1) · 𝑇)))
183	127	recnd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
184	21	recnd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
185	184	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℂ)
186	183, 185	adddirp1d 11340	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → ((𝑘 + 1) · 𝑇) = ((𝑘 · 𝑇) + 𝑇))
187	186	oveq2d 7438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
188	187	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
189	188	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 + 1) · 𝑇)) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
190	86	recnd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
191	190	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℂ)
192	130	recnd 11342	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℂ)
193	184	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℂ)
194	191, 192, 193	addassd 11336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝑥 + ((𝑘 · 𝑇) + 𝑇)))
195	194	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + ((𝑘 · 𝑇) + 𝑇)) = ((𝑥 + (𝑘 · 𝑇)) + 𝑇))
196	195	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 · 𝑇) + 𝑇)) = ((𝑥 + (𝑘 · 𝑇)) + 𝑇))
197		oveq1 7429	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 + (𝑘 · 𝑇)) = 𝐴 → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝐴 + 𝑇))
198	197	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = (𝐴 + 𝑇))
199	4	recnd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐵 ∈ ℂ)
200	1	recnd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 ∈ ℂ)
201	199, 200, 184	subaddd 11692	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐵 − 𝐴) = 𝑇 ↔ (𝐴 + 𝑇) = 𝐵))
202	26, 201	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
203	202	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐴 + 𝑇) = 𝐵)
204	198, 203	eqtrd 2795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) + 𝑇) = 𝐵)
205	189, 196, 204	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + ((𝑘 + 1) · 𝑇)) = 𝐵)
206	98, 182, 205	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = 𝐵)
207		fourierdlem51.bc	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
208	207	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐵 ∈ 𝐶)
209	206, 208	eqeltrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
210	209	3adantl3 1187	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
211		simpl1 1210	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝜑 ∧ 𝑥 ∈ ℝ))
212		simpl2 1211	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝑘 ∈ ℤ)
213		fourierdlem51.css	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ⊆ (𝐴[,]𝐵))
214	213	sselda 3909	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
215	214	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
216	215	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
217	216	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵))
218		neqne 2963	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴 → (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)
219	218	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)
220	1	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
221	211, 220	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐴 ∈ ℝ)
222	211, 87	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → 𝐵 ∈ ℝ)
223		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ ℝ)
224	223, 130	readdcld 11343	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ)
225	224	rexrd 11364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ^*)
226	211, 212, 225	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ ℝ^*)
227	221, 222, 226	eliccelioc 46640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → ((𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + (𝑘 · 𝑇)) ∈ (𝐴[,]𝐵) ∧ (𝑥 + (𝑘 · 𝑇)) ≠ 𝐴)))
228	217, 219, 227	mpbir2and 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵))
229	97	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
230	1	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
231	4	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ)
232	22	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐵)
233		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ)
234	92	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
235		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → 𝑘 ∈ ℤ)
236	97, 113	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
237	236	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
238		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵))
239	230, 231, 232, 19, 233, 234, 235, 237, 238	fourierdlem35 47259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = 𝑘)
240	239	oveq1d 7437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = (𝑘 · 𝑇))
241	240	oveq2d 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
242	229, 241	eqtrd 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ) ∧ (𝑥 + (𝑘 · 𝑇)) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑥) = (𝑥 + (𝑘 · 𝑇)))
243	211, 212, 228, 242	syl21anc 851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) = (𝑥 + (𝑘 · 𝑇)))
244		simpl3 1212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
245	243, 244	eqeltrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ (𝑥 + (𝑘 · 𝑇)) = 𝐴) → (𝐸‘𝑥) ∈ 𝐶)
246	210, 245	pm2.61dan 825	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℤ ∧ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → (𝐸‘𝑥) ∈ 𝐶)
247	246	3exp 1137	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑘 ∈ ℤ → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶)))
248	78, 85, 247	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (𝑘 ∈ ℤ → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶)))
249	76, 77, 248	rexlimd 3269	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶 → (𝐸‘𝑥) ∈ 𝐶))
250	70, 249	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (𝐸‘𝑥) ∈ 𝐶)
251	64, 250	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥) ∈ 𝐶)
252		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)) = (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥))
253	251, 252	fmptd 7117	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶)
254		iocssre 13563	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
255	102, 4, 254	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
256	112, 255	fssd 6730	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:ℝ⟶ℝ)
257		ssrab2 4004	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))
258	257, 81	sstrid 3920	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ℝ)
259	256, 258	fssresd 6752	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶ℝ)
260	259	feqmptd 6956	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) = (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)))
261	260	feq1d 6694	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶 ↔ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↦ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑥)):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶))
262	253, 261	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶)
263		simplll 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝜑)
264		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
265		fourierdlem51.h	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}
266	264, 265	eleqtrrdi 2871	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑤 ∈ 𝐻)
267	266	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑤 ∈ 𝐻)
268	263, 267	jca 521	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝜑 ∧ 𝑤 ∈ 𝐻))
269		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
270	269, 265	eleqtrrdi 2871	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑧 ∈ 𝐻)
271	270	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑧 ∈ 𝐻)
272		fvres 6907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = (𝐸‘𝑧))
273	272	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → (𝐸‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
274	273	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝐸‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
275		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧))
276	275	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤))
277	276	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤))
278		fvres 6907	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = (𝐸‘𝑤))
279	278	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = (𝐸‘𝑤))
280	274, 277, 279	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → (𝐸‘𝑧) = (𝐸‘𝑤))
281	1	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐴 ∈ ℝ)
282	4	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐵 ∈ ℝ)
283	22	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝐴 < 𝐵)
284	2	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑋 ∈ ℝ)
285		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 ∈ 𝐻)
286		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑧 ∈ 𝐻)
287		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝐸‘𝑧) = (𝐸‘𝑤))
288	281, 282, 283, 284, 265, 19, 31, 285, 286, 287	fourierdlem19 47243	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → ¬ 𝑤 < 𝑧)
289	287	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝐸‘𝑤) = (𝐸‘𝑧))
290	281, 282, 283, 284, 265, 19, 31, 286, 285, 289	fourierdlem19 47243	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → ¬ 𝑧 < 𝑤)
291	265, 258	eqsstrid 3947	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
292	291	sselda 3909	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐻) → 𝑤 ∈ ℝ)
293	292	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 ∈ ℝ)
294	291	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐻) → 𝐻 ⊆ ℝ)
295	294	sselda 3909	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) → 𝑧 ∈ ℝ)
296	295	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑧 ∈ ℝ)
297	293, 296	lttri3d 11455	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → (𝑤 = 𝑧 ↔ (¬ 𝑤 < 𝑧 ∧ ¬ 𝑧 < 𝑤)))
298	288, 290, 297	mpbir2and 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐻) ∧ 𝑧 ∈ 𝐻) ∧ (𝐸‘𝑧) = (𝐸‘𝑤)) → 𝑤 = 𝑧)
299	268, 271, 280, 298	syl21anc 851	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧)) → 𝑤 = 𝑧)
300	299	ex 418	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∧ 𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
301	300	ralrimiva 3154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
302	301	ralrimiva 3154	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧))
303		dff13 7260	. . . . . . . . . 10 ⊢ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶 ↔ ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}⟶𝐶 ∧ ∀𝑤 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}∀𝑧 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} (((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑤) = ((𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})‘𝑧) → 𝑤 = 𝑧)))
304	262, 302, 303	sylanbrc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶)
305		f1fi 9311	. . . . . . . . 9 ⊢ ((𝐶 ∈ Fin ∧ (𝐸 ↾ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}):{𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}–1-1→𝐶) → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
306	62, 304, 305	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
307		unfi 9191	. . . . . . . 8 ⊢ (({(𝐴 + 𝑋)} ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin) → ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
308	61, 306, 307	sylancr 599	. . . . . . 7 ⊢ (𝜑 → ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
309		simpl 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝜑)
310		elrabi 3640	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
311	310	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
312	67	elrab 3644	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ↔ (𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶))
313	312	simprbi 503	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
314	313	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
315		velsn 4596	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐴 + 𝑋)} ↔ 𝑥 = (𝐴 + 𝑋))
316		elun1 4179	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐴 + 𝑋)} → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
317	315, 316	sylbir 238	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 + 𝑋) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
318	317	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
319	79	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ∈ ℝ^*)
320	5	rexrd 11364	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ^*)
321	320	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐵 + 𝑋) ∈ ℝ^*)
322	3, 5	iccssred 13570	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ⊆ ℝ)
323	322	sselda 3909	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ℝ)
324	323	rexrd 11364	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ℝ^*)
325	324	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ℝ^*)
326	3	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ∈ ℝ)
327	323	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ℝ)
328	79	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ∈ ℝ^*)
329	320	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐵 + 𝑋) ∈ ℝ^*)
330		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)))
331		iccgelb 13538	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ^* ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ≤ 𝑥)
332	328, 329, 330, 331	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → (𝐴 + 𝑋) ≤ 𝑥)
333	332	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) ≤ 𝑥)
334		neqne 2963	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 = (𝐴 + 𝑋) → 𝑥 ≠ (𝐴 + 𝑋))
335	334	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ≠ (𝐴 + 𝑋))
336	326, 327, 333, 335	leneltd 11469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → (𝐴 + 𝑋) < 𝑥)
337		iccleub 13537	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 + 𝑋) ∈ ℝ^* ∧ (𝐵 + 𝑋) ∈ ℝ^* ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ≤ (𝐵 + 𝑋))
338	328, 329, 330, 337	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) → 𝑥 ≤ (𝐵 + 𝑋))
339	338	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ≤ (𝐵 + 𝑋))
340	319, 321, 325, 336, 339	eliocd 46626	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
341	340	adantlr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)))
342		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶)
343	341, 342, 68	sylanbrc 595	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})
344		elun2 4180	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
345	343, 344	syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) ∧ ¬ 𝑥 = (𝐴 + 𝑋)) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
346	318, 345	pm2.61dan 825	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))) ∧ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐶) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
347	309, 311, 314, 346	syl21anc 851	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) → 𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
348	347	ralrimiva 3154	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
349		dfss3 3898	. . . . . . . 8 ⊢ ({𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ↔ ∀𝑥 ∈ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}𝑥 ∈ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
350	348, 349	sylibr 237	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}))
351		ssfi 9193	. . . . . . 7 ⊢ ((({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ({(𝐴 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})) → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
352	308, 350, 351	syl2anc 596	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin)
353		unfi 9191	. . . . . 6 ⊢ (({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∈ Fin ∧ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ∈ Fin) → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
354	60, 352, 353	sylancr 599	. . . . 5 ⊢ (𝜑 → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ∈ Fin)
355	58, 354	eqeltrid 2864	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Fin)
356		prssi 4776	. . . . . . 7 ⊢ (((𝐴 + 𝑋) ∈ ℝ ∧ (𝐵 + 𝑋) ∈ ℝ) → {(𝐴 + 𝑋), (𝐵 + 𝑋)} ⊆ ℝ)
357	3, 5, 356	syl2anc 596	. . . . . 6 ⊢ (𝜑 → {(𝐴 + 𝑋), (𝐵 + 𝑋)} ⊆ ℝ)
358		ssrab2 4004	. . . . . . 7 ⊢ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)[,](𝐵 + 𝑋))
359	358, 322	sstrid 3920	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ℝ)
360	357, 359	unssd 4189	. . . . 5 ⊢ (𝜑 → ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) ⊆ ℝ)
361	58, 360	eqsstrid 3947	. . . 4 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
362		fourierdlem51.f	. . . 4 ⊢ 𝐹 = (℩𝑓𝑓 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷))
363		eqid 2760	. . . 4 ⊢ ((♯‘𝐷) − 1) = ((♯‘𝐷) − 1)
364	355, 361, 362, 363	fourierdlem36 47260	. . 3 ⊢ (𝜑 → 𝐹 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷))
365		isof1o 7333	. . 3 ⊢ (𝐹 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷) → 𝐹:(0...((♯‘𝐷) − 1))–1-1-onto→𝐷)
366		f1ofo 6835	. . 3 ⊢ (𝐹:(0...((♯‘𝐷) − 1))–1-1-onto→𝐷 → 𝐹:(0...((♯‘𝐷) − 1))–onto→𝐷)
367		forn 6802	. . 3 ⊢ (𝐹:(0...((♯‘𝐷) − 1))–onto→𝐷 → ran 𝐹 = 𝐷)
368	364, 365, 366, 367	4syl 20	. 2 ⊢ (𝜑 → ran 𝐹 = 𝐷)
369	59, 368	eleqtrrd 2863	1 ⊢ (𝜑 → 𝑋 ∈ ran 𝐹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3896 ∪ cun 4148 {csn 4584 {cpr 4586 class class class wbr 5102 ↦ cmpt 5185 ran crn 5651 ↾ cres 5652 ℩cio 6494 ⟶wf 6537 –1-1→wf1 6538 –onto→wfo 6539 –1-1-onto→wf1o 6540 ‘cfv 6541 Isom wiso 6542 (class class class)co 7422 Fincfn 8978 ℂcc 11203 ℝcr 11204 0cc0 11205 1c1 11206 + caddc 11208 · cmul 11210 ℝ^*cxr 11347 < clt 11348 ≤ cle 11349 − cmin 11546 / cdiv 11978 ℤcz 12698 ℝ⁺crp 13125 (,]cioc 13482 [,]cicc 13484 ...cfz 13644 ⌊cfl 13935 ♯chash 14479

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-inf2 9647 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282 ax-pre-sup 11283

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-om 7880 df-1st 8003 df-2nd 8004 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-2o 8482 df-er 8722 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-sup 9439 df-inf 9440 df-oi 9509 df-card 10025 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-div 11979 df-nn 12341 df-n0 12612 df-z 12699 df-uz 12971 df-rp 13126 df-ioc 13486 df-icc 13488 df-fz 13645 df-fl 13937 df-hash 14480

This theorem is used by: fourierdlem113 47336

W3C validator