fourierdlem51

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

	Ref	Expression
Hypotheses	fourierdlem51.a	$⊢ φ \to A \in ℝ$
	fourierdlem51.b	$⊢ φ \to B \in ℝ$
	fourierdlem51.alt0	$⊢ φ \to A < 0$
	fourierdlem51.bgt0	$⊢ φ \to 0 < B$
	fourierdlem51.t	$⊢ T = B - A$
	fourierdlem51.cfi	$⊢ φ \to C \in Fin$
	fourierdlem51.css	$⊢ φ \to C \subseteq [A, B]$
	fourierdlem51.bc	$⊢ φ \to B \in C$
	fourierdlem51.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem51.x	$⊢ φ \to X \in ℝ$
	fourierdlem51.exc	$⊢ φ \to E (X) \in C$
	fourierdlem51.d	$⊢ D = \{A + X, B + X\} \cup \{y \in [A + X, B + X] \| \exists k \in ℤ y + k T \in C\}$
	fourierdlem51.f	$⊢ F = (ι f \| f {Isom}_{<, <} ((0 \dots \|D\| - 1), D))$
	fourierdlem51.h	$⊢ H = \{y \in (A + X, B + X] \| \exists k \in ℤ y + k T \in C\}$
Assertion	fourierdlem51	$⊢ φ \to X \in ran F$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem51

Proof