fourierdlem26

Description: Periodic image of a point Y that's in the period that begins with the point X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem26.1	$⊢ φ \to A \in ℝ$
	fourierdlem26.2	$⊢ φ \to B \in ℝ$
	fourierdlem26.3	$⊢ φ \to A < B$
	fourierdlem26.4	$⊢ T = B - A$
	fourierdlem26.5	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem26.6	$⊢ φ \to X \in ℝ$
	fourierdlem26.7	$⊢ φ \to E (X) = B$
	fourierdlem26.8	$⊢ φ \to Y \in (X, X + T]$
Assertion	fourierdlem26	$⊢ φ \to E (Y) = A + Y - X$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem26.1	$⊢ φ \to A \in ℝ$
2		fourierdlem26.2	$⊢ φ \to B \in ℝ$
3		fourierdlem26.3	$⊢ φ \to A < B$
4		fourierdlem26.4	$⊢ T = B - A$
5		fourierdlem26.5	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
6		fourierdlem26.6	$⊢ φ \to X \in ℝ$
7		fourierdlem26.7	$⊢ φ \to E (X) = B$
8		fourierdlem26.8	$⊢ φ \to Y \in (X, X + T]$
9	5	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
10		simpr	$⊢ (φ \land x = Y) \to x = Y$
11	10	oveq2d	$⊢ (φ \land x = Y) \to B - x = B - Y$
12	11	oveq1d	$⊢ (φ \land x = Y) \to \frac{B - x}{T} = \frac{B - Y}{T}$
13	12	fveq2d	$⊢ (φ \land x = Y) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - Y}{T}⌋$
14	13	oveq1d	$⊢ (φ \land x = Y) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - Y}{T}⌋ T$
15	10 14	oveq12d	$⊢ (φ \land x = Y) \to x + ⌊\frac{B - x}{T}⌋ T = Y + ⌊\frac{B - Y}{T}⌋ T$
16	6	rexrd	$⊢ φ \to X \in ℝ^{*}$
17	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
18	4 17	eqeltrid	$⊢ φ \to T \in ℝ$
19	6 18	readdcld	$⊢ φ \to X + T \in ℝ$
20		elioc2	$⊢ (X \in ℝ^{*} \land X + T \in ℝ) \to (Y \in (X, X + T] \leftrightarrow (Y \in ℝ \land X < Y \land Y \leq X + T))$
21	16 19 20	syl2anc	$⊢ φ \to (Y \in (X, X + T] \leftrightarrow (Y \in ℝ \land X < Y \land Y \leq X + T))$
22	8 21	mpbid	$⊢ φ \to (Y \in ℝ \land X < Y \land Y \leq X + T)$
23	22	simp1d	$⊢ φ \to Y \in ℝ$
24	2 23	resubcld	$⊢ φ \to B - Y \in ℝ$
25	1 2	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
26	3 25	mpbid	$⊢ φ \to 0 < B - A$
27	26 4	breqtrrdi	$⊢ φ \to 0 < T$
28	27	gt0ne0d	$⊢ φ \to T \neq 0$
29	24 18 28	redivcld	$⊢ φ \to \frac{B - Y}{T} \in ℝ$
30	29	flcld	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ \in ℤ$
31	30	zred	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ \in ℝ$
32	31 18	remulcld	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ T \in ℝ$
33	23 32	readdcld	$⊢ φ \to Y + ⌊\frac{B - Y}{T}⌋ T \in ℝ$
34	9 15 23 33	fvmptd	$⊢ φ \to E (Y) = Y + ⌊\frac{B - Y}{T}⌋ T$
35	6	recnd	$⊢ φ \to X \in ℂ$
36	23	recnd	$⊢ φ \to Y \in ℂ$
37	35 36	pncan3d	$⊢ φ \to X + Y - X = Y$
38	37	eqcomd	$⊢ φ \to Y = X + Y - X$
39	38	oveq2d	$⊢ φ \to B - Y = B - (X + Y - X)$
40	2	recnd	$⊢ φ \to B \in ℂ$
41	36 35	subcld	$⊢ φ \to Y - X \in ℂ$
42	40 35 41	subsub4d	$⊢ φ \to B - X - (Y - X) = B - (X + Y - X)$
43	39 42	eqtr4d	$⊢ φ \to B - Y = B - X - (Y - X)$
44	43	oveq1d	$⊢ φ \to \frac{B - Y}{T} = \frac{B - X - (Y - X)}{T}$
45	2 6	resubcld	$⊢ φ \to B - X \in ℝ$
46	45	recnd	$⊢ φ \to B - X \in ℂ$
47	18	recnd	$⊢ φ \to T \in ℂ$
48	46 41 47 28	divsubdird	$⊢ φ \to \frac{B - X - (Y - X)}{T} = (\frac{B - X}{T}) - (\frac{Y - X}{T})$
49	41 47 28	divnegd	$⊢ φ \to - \frac{Y - X}{T} = \frac{- (Y - X)}{T}$
50	36 35	negsubdi2d	$⊢ φ \to - (Y - X) = X - Y$
51	50	oveq1d	$⊢ φ \to \frac{- (Y - X)}{T} = \frac{X - Y}{T}$
52	49 51	eqtrd	$⊢ φ \to - \frac{Y - X}{T} = \frac{X - Y}{T}$
53	52	oveq2d	$⊢ φ \to (\frac{B - X}{T}) + (- \frac{Y - X}{T}) = (\frac{B - X}{T}) + (\frac{X - Y}{T})$
54	45 18 28	redivcld	$⊢ φ \to \frac{B - X}{T} \in ℝ$
55	54	recnd	$⊢ φ \to \frac{B - X}{T} \in ℂ$
56	41 47 28	divcld	$⊢ φ \to \frac{Y - X}{T} \in ℂ$
57	55 56	negsubd	$⊢ φ \to (\frac{B - X}{T}) + (- \frac{Y - X}{T}) = (\frac{B - X}{T}) - (\frac{Y - X}{T})$
58		1cnd	$⊢ φ \to 1 \in ℂ$
59	55 58	npcand	$⊢ φ \to (\frac{B - X}{T}) - 1 + 1 = \frac{B - X}{T}$
60	59	eqcomd	$⊢ φ \to \frac{B - X}{T} = (\frac{B - X}{T}) - 1 + 1$
61	60	oveq1d	$⊢ φ \to (\frac{B - X}{T}) + (\frac{X - Y}{T}) = ((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})$
62	55 58	subcld	$⊢ φ \to (\frac{B - X}{T}) - 1 \in ℂ$
63	35 36	subcld	$⊢ φ \to X - Y \in ℂ$
64	63 47 28	divcld	$⊢ φ \to \frac{X - Y}{T} \in ℂ$
65	62 58 64	addassd	$⊢ φ \to ((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T}) = ((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})$
66	61 65	eqtrd	$⊢ φ \to (\frac{B - X}{T}) + (\frac{X - Y}{T}) = ((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})$
67	53 57 66	3eqtr3d	$⊢ φ \to (\frac{B - X}{T}) - (\frac{Y - X}{T}) = ((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})$
68	44 48 67	3eqtrd	$⊢ φ \to \frac{B - Y}{T} = ((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})$
69	68	fveq2d	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ = ⌊((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})⌋$
70	6 23	resubcld	$⊢ φ \to X - Y \in ℝ$
71	18 70	readdcld	$⊢ φ \to T + X - Y \in ℝ$
72	18 27	elrpd	$⊢ φ \to T \in ℝ^{+}$
73	35 47	addcomd	$⊢ φ \to X + T = T + X$
74	73	oveq2d	$⊢ φ \to (X, X + T] = (X, T + X]$
75	8 74	eleqtrd	$⊢ φ \to Y \in (X, T + X]$
76	18 6	readdcld	$⊢ φ \to T + X \in ℝ$
77		elioc2	$⊢ (X \in ℝ^{*} \land T + X \in ℝ) \to (Y \in (X, T + X] \leftrightarrow (Y \in ℝ \land X < Y \land Y \leq T + X))$
78	16 76 77	syl2anc	$⊢ φ \to (Y \in (X, T + X] \leftrightarrow (Y \in ℝ \land X < Y \land Y \leq T + X))$
79	75 78	mpbid	$⊢ φ \to (Y \in ℝ \land X < Y \land Y \leq T + X)$
80	79	simp3d	$⊢ φ \to Y \leq T + X$
81	23 6 18	lesubaddd	$⊢ φ \to (Y - X \leq T \leftrightarrow Y \leq T + X)$
82	80 81	mpbird	$⊢ φ \to Y - X \leq T$
83	23 6	resubcld	$⊢ φ \to Y - X \in ℝ$
84	18 83	subge0d	$⊢ φ \to (0 \leq T - (Y - X) \leftrightarrow Y - X \leq T)$
85	82 84	mpbird	$⊢ φ \to 0 \leq T - (Y - X)$
86	47 36 35	subsub2d	$⊢ φ \to T - (Y - X) = T + X - Y$
87	85 86	breqtrd	$⊢ φ \to 0 \leq T + X - Y$
88	71 72 87	divge0d	$⊢ φ \to 0 \leq \frac{T + X - Y}{T}$
89	47 63 47 28	divdird	$⊢ φ \to \frac{T + X - Y}{T} = (\frac{T}{T}) + (\frac{X - Y}{T})$
90	47 28	dividd	$⊢ φ \to \frac{T}{T} = 1$
91	90	eqcomd	$⊢ φ \to 1 = \frac{T}{T}$
92	91	oveq1d	$⊢ φ \to 1 + (\frac{X - Y}{T}) = (\frac{T}{T}) + (\frac{X - Y}{T})$
93	89 92	eqtr4d	$⊢ φ \to \frac{T + X - Y}{T} = 1 + (\frac{X - Y}{T})$
94	88 93	breqtrd	$⊢ φ \to 0 \leq 1 + (\frac{X - Y}{T})$
95	22	simp2d	$⊢ φ \to X < Y$
96	6 23	sublt0d	$⊢ φ \to (X - Y < 0 \leftrightarrow X < Y)$
97	95 96	mpbird	$⊢ φ \to X - Y < 0$
98	70 72 97	divlt0gt0d	$⊢ φ \to \frac{X - Y}{T} < 0$
99	70 18 28	redivcld	$⊢ φ \to \frac{X - Y}{T} \in ℝ$
100		1red	$⊢ φ \to 1 \in ℝ$
101		ltaddneg	$⊢ (\frac{X - Y}{T} \in ℝ \land 1 \in ℝ) \to (\frac{X - Y}{T} < 0 \leftrightarrow 1 + (\frac{X - Y}{T}) < 1)$
102	99 100 101	syl2anc	$⊢ φ \to (\frac{X - Y}{T} < 0 \leftrightarrow 1 + (\frac{X - Y}{T}) < 1)$
103	98 102	mpbid	$⊢ φ \to 1 + (\frac{X - Y}{T}) < 1$
104	54	flcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℤ$
105	104	zcnd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℂ$
106	105 47	mulcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T \in ℂ$
107	35 106	pncan2d	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T - X = ⌊\frac{B - X}{T}⌋ T$
108	107	eqcomd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T = X + ⌊\frac{B - X}{T}⌋ T - X$
109	108	oveq1d	$⊢ φ \to \frac{⌊\frac{B - X}{T}⌋ T}{T} = \frac{X + ⌊\frac{B - X}{T}⌋ T - X}{T}$
110	105 47 28	divcan4d	$⊢ φ \to \frac{⌊\frac{B - X}{T}⌋ T}{T} = ⌊\frac{B - X}{T}⌋$
111		id	$⊢ x = X \to x = X$
112		oveq2	$⊢ x = X \to B - x = B - X$
113	112	oveq1d	$⊢ x = X \to \frac{B - x}{T} = \frac{B - X}{T}$
114	113	fveq2d	$⊢ x = X \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - X}{T}⌋$
115	114	oveq1d	$⊢ x = X \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - X}{T}⌋ T$
116	111 115	oveq12d	$⊢ x = X \to x + ⌊\frac{B - x}{T}⌋ T = X + ⌊\frac{B - X}{T}⌋ T$
117	116	adantl	$⊢ (φ \land x = X) \to x + ⌊\frac{B - x}{T}⌋ T = X + ⌊\frac{B - X}{T}⌋ T$
118		reflcl	$⊢ \frac{B - X}{T} \in ℝ \to ⌊\frac{B - X}{T}⌋ \in ℝ$
119	54 118	syl	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℝ$
120	119 18	remulcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T \in ℝ$
121	6 120	readdcld	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T \in ℝ$
122	9 117 6 121	fvmptd	$⊢ φ \to E (X) = X + ⌊\frac{B - X}{T}⌋ T$
123	122	eqcomd	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T = E (X)$
124	123	oveq1d	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T - X = E (X) - X$
125	124	oveq1d	$⊢ φ \to \frac{X + ⌊\frac{B - X}{T}⌋ T - X}{T} = \frac{E (X) - X}{T}$
126	7	oveq1d	$⊢ φ \to E (X) - X = B - X$
127	126	oveq1d	$⊢ φ \to \frac{E (X) - X}{T} = \frac{B - X}{T}$
128	125 127	eqtrd	$⊢ φ \to \frac{X + ⌊\frac{B - X}{T}⌋ T - X}{T} = \frac{B - X}{T}$
129	109 110 128	3eqtr3d	$⊢ φ \to ⌊\frac{B - X}{T}⌋ = \frac{B - X}{T}$
130	129 104	eqeltrrd	$⊢ φ \to \frac{B - X}{T} \in ℤ$
131		1zzd	$⊢ φ \to 1 \in ℤ$
132	130 131	zsubcld	$⊢ φ \to (\frac{B - X}{T}) - 1 \in ℤ$
133	100 99	readdcld	$⊢ φ \to 1 + (\frac{X - Y}{T}) \in ℝ$
134		flbi2	$⊢ ((\frac{B - X}{T}) - 1 \in ℤ \land 1 + (\frac{X - Y}{T}) \in ℝ) \to (⌊((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})⌋ = (\frac{B - X}{T}) - 1 \leftrightarrow (0 \leq 1 + (\frac{X - Y}{T}) \land 1 + (\frac{X - Y}{T}) < 1))$
135	132 133 134	syl2anc	$⊢ φ \to (⌊((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})⌋ = (\frac{B - X}{T}) - 1 \leftrightarrow (0 \leq 1 + (\frac{X - Y}{T}) \land 1 + (\frac{X - Y}{T}) < 1))$
136	94 103 135	mpbir2and	$⊢ φ \to ⌊((\frac{B - X}{T}) - 1) + 1 + (\frac{X - Y}{T})⌋ = (\frac{B - X}{T}) - 1$
137	129	eqcomd	$⊢ φ \to \frac{B - X}{T} = ⌊\frac{B - X}{T}⌋$
138	137	oveq1d	$⊢ φ \to (\frac{B - X}{T}) - 1 = ⌊\frac{B - X}{T}⌋ - 1$
139	69 136 138	3eqtrd	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ = ⌊\frac{B - X}{T}⌋ - 1$
140	139	oveq1d	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ T = (⌊\frac{B - X}{T}⌋ - 1) T$
141	140	oveq2d	$⊢ φ \to Y + ⌊\frac{B - Y}{T}⌋ T = Y + (⌊\frac{B - X}{T}⌋ - 1) T$
142	38	oveq1d	$⊢ φ \to Y + (⌊\frac{B - X}{T}⌋ - 1) T = X + (Y - X) + (⌊\frac{B - X}{T}⌋ - 1) T$
143	105 58 47	subdird	$⊢ φ \to (⌊\frac{B - X}{T}⌋ - 1) T = ⌊\frac{B - X}{T}⌋ T - 1 T$
144	143	oveq2d	$⊢ φ \to X + (Y - X) + (⌊\frac{B - X}{T}⌋ - 1) T = X + (Y - X) + (⌊\frac{B - X}{T}⌋ T - 1 T)$
145	35 41	addcld	$⊢ φ \to X + Y - X \in ℂ$
146	58 47	mulcld	$⊢ φ \to 1 T \in ℂ$
147	145 106 146	addsubassd	$⊢ φ \to (X + Y - X) + ⌊\frac{B - X}{T}⌋ T - 1 T = X + (Y - X) + (⌊\frac{B - X}{T}⌋ T - 1 T)$
148	147	eqcomd	$⊢ φ \to X + (Y - X) + (⌊\frac{B - X}{T}⌋ T - 1 T) = (X + Y - X) + ⌊\frac{B - X}{T}⌋ T - 1 T$
149	35 41 106	add32d	$⊢ φ \to X + (Y - X) + ⌊\frac{B - X}{T}⌋ T = X + ⌊\frac{B - X}{T}⌋ T + (Y - X)$
150	149	oveq1d	$⊢ φ \to (X + Y - X) + ⌊\frac{B - X}{T}⌋ T - 1 T = (X + ⌊\frac{B - X}{T}⌋ T) + (Y - X) - 1 T$
151	123	oveq1d	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T + (Y - X) = E (X) + Y - X$
152	47	mulid2d	$⊢ φ \to 1 T = T$
153	151 152	oveq12d	$⊢ φ \to (X + ⌊\frac{B - X}{T}⌋ T) + (Y - X) - 1 T = E (X) + (Y - X) - T$
154	7 2	eqeltrd	$⊢ φ \to E (X) \in ℝ$
155	154	recnd	$⊢ φ \to E (X) \in ℂ$
156	155 41 47	addsubd	$⊢ φ \to E (X) + (Y - X) - T = (E (X) - T) + Y - X$
157	7	oveq1d	$⊢ φ \to E (X) - T = B - T$
158	4	a1i	$⊢ φ \to T = B - A$
159	158	oveq2d	$⊢ φ \to B - T = B - (B - A)$
160	1	recnd	$⊢ φ \to A \in ℂ$
161	40 160	nncand	$⊢ φ \to B - (B - A) = A$
162	157 159 161	3eqtrd	$⊢ φ \to E (X) - T = A$
163	162	oveq1d	$⊢ φ \to (E (X) - T) + Y - X = A + Y - X$
164	156 163	eqtrd	$⊢ φ \to E (X) + (Y - X) - T = A + Y - X$
165	150 153 164	3eqtrd	$⊢ φ \to (X + Y - X) + ⌊\frac{B - X}{T}⌋ T - 1 T = A + Y - X$
166	144 148 165	3eqtrd	$⊢ φ \to X + (Y - X) + (⌊\frac{B - X}{T}⌋ - 1) T = A + Y - X$
167	142 166	eqtrd	$⊢ φ \to Y + (⌊\frac{B - X}{T}⌋ - 1) T = A + Y - X$
168	34 141 167	3eqtrd	$⊢ φ \to E (Y) = A + Y - X$

Metamath Proof Explorer

Theorem fourierdlem26

Proof