fourierdlem19

Description: If two elements of D have the same periodic image in ( A (,] B ) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem19.a	$⊢ φ \to A \in ℝ$
	fourierdlem19.b	$⊢ φ \to B \in ℝ$
	fourierdlem19.altb	$⊢ φ \to A < B$
	fourierdlem19.x	$⊢ φ \to X \in ℝ$
	fourierdlem19.d	$⊢ D = \{y \in (A + X, B + X] \| \exists k \in ℤ y + k T \in C\}$
	fourierdlem19.t	$⊢ T = B - A$
	fourierdlem19.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem19.w	$⊢ φ \to W \in D$
	fourierdlem19.z	$⊢ φ \to Z \in D$
	fourierdlem19.ezew	$⊢ φ \to E (Z) = E (W)$
Assertion	fourierdlem19	$⊢ φ \to \neg W < Z$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem19.a	$⊢ φ \to A \in ℝ$
2		fourierdlem19.b	$⊢ φ \to B \in ℝ$
3		fourierdlem19.altb	$⊢ φ \to A < B$
4		fourierdlem19.x	$⊢ φ \to X \in ℝ$
5		fourierdlem19.d	$⊢ D = \{y \in (A + X, B + X] \| \exists k \in ℤ y + k T \in C\}$
6		fourierdlem19.t	$⊢ T = B - A$
7		fourierdlem19.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
8		fourierdlem19.w	$⊢ φ \to W \in D$
9		fourierdlem19.z	$⊢ φ \to Z \in D$
10		fourierdlem19.ezew	$⊢ φ \to E (Z) = E (W)$
11	1 4	readdcld	$⊢ φ \to A + X \in ℝ$
12	11	rexrd	$⊢ φ \to A + X \in ℝ^{*}$
13	2 4	readdcld	$⊢ φ \to B + X \in ℝ$
14	13	rexrd	$⊢ φ \to B + X \in ℝ^{*}$
15		ssrab2	$⊢ \{y \in (A + X, B + X] \| \exists k \in ℤ y + k T \in C\} \subseteq (A + X, B + X]$
16	5 15	eqsstri	$⊢ D \subseteq (A + X, B + X]$
17	16 9	sselid	$⊢ φ \to Z \in (A + X, B + X]$
18		iocleub	$⊢ (A + X \in ℝ^{} \land B + X \in ℝ^{} \land Z \in (A + X, B + X]) \to Z \leq B + X$
19	12 14 17 18	syl3anc	$⊢ φ \to Z \leq B + X$
20	19	adantr	$⊢ (φ \land W < Z) \to Z \leq B + X$
21	13	adantr	$⊢ (φ \land W < Z) \to B + X \in ℝ$
22		iocssre	$⊢ (A + X \in ℝ^{*} \land B + X \in ℝ) \to (A + X, B + X] \subseteq ℝ$
23	12 13 22	syl2anc	$⊢ φ \to (A + X, B + X] \subseteq ℝ$
24	16 8	sselid	$⊢ φ \to W \in (A + X, B + X]$
25	23 24	sseldd	$⊢ φ \to W \in ℝ$
26	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
27	6 26	eqeltrid	$⊢ φ \to T \in ℝ$
28	25 27	readdcld	$⊢ φ \to W + T \in ℝ$
29	28	adantr	$⊢ (φ \land W < Z) \to W + T \in ℝ$
30	23 17	sseldd	$⊢ φ \to Z \in ℝ$
31	30	adantr	$⊢ (φ \land W < Z) \to Z \in ℝ$
32	6	eqcomi	$⊢ B - A = T$
33	32	a1i	$⊢ φ \to B - A = T$
34	2	recnd	$⊢ φ \to B \in ℂ$
35	1	recnd	$⊢ φ \to A \in ℂ$
36	27	recnd	$⊢ φ \to T \in ℂ$
37	34 35 36	subaddd	$⊢ φ \to (B - A = T \leftrightarrow A + T = B)$
38	33 37	mpbid	$⊢ φ \to A + T = B$
39	38	eqcomd	$⊢ φ \to B = A + T$
40	39	oveq1d	$⊢ φ \to B + X = A + T + X$
41	4	recnd	$⊢ φ \to X \in ℂ$
42	35 36 41	add32d	$⊢ φ \to A + T + X = A + X + T$
43	40 42	eqtrd	$⊢ φ \to B + X = A + X + T$
44		iocgtlb	$⊢ (A + X \in ℝ^{} \land B + X \in ℝ^{} \land W \in (A + X, B + X]) \to A + X < W$
45	12 14 24 44	syl3anc	$⊢ φ \to A + X < W$
46	11 25 27 45	ltadd1dd	$⊢ φ \to A + X + T < W + T$
47	43 46	eqbrtrd	$⊢ φ \to B + X < W + T$
48	47	adantr	$⊢ (φ \land W < Z) \to B + X < W + T$
49	7	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
50		id	$⊢ x = W \to x = W$
51		oveq2	$⊢ x = W \to B - x = B - W$
52	51	oveq1d	$⊢ x = W \to \frac{B - x}{T} = \frac{B - W}{T}$
53	52	fveq2d	$⊢ x = W \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - W}{T}⌋$
54	53	oveq1d	$⊢ x = W \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - W}{T}⌋ T$
55	50 54	oveq12d	$⊢ x = W \to x + ⌊\frac{B - x}{T}⌋ T = W + ⌊\frac{B - W}{T}⌋ T$
56	55	adantl	$⊢ (φ \land x = W) \to x + ⌊\frac{B - x}{T}⌋ T = W + ⌊\frac{B - W}{T}⌋ T$
57	2 25	resubcld	$⊢ φ \to B - W \in ℝ$
58	1 2	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
59	3 58	mpbid	$⊢ φ \to 0 < B - A$
60	59 6	breqtrrdi	$⊢ φ \to 0 < T$
61	60	gt0ne0d	$⊢ φ \to T \neq 0$
62	57 27 61	redivcld	$⊢ φ \to \frac{B - W}{T} \in ℝ$
63	62	flcld	$⊢ φ \to ⌊\frac{B - W}{T}⌋ \in ℤ$
64	63	zred	$⊢ φ \to ⌊\frac{B - W}{T}⌋ \in ℝ$
65	64 27	remulcld	$⊢ φ \to ⌊\frac{B - W}{T}⌋ T \in ℝ$
66	25 65	readdcld	$⊢ φ \to W + ⌊\frac{B - W}{T}⌋ T \in ℝ$
67	49 56 25 66	fvmptd	$⊢ φ \to E (W) = W + ⌊\frac{B - W}{T}⌋ T$
68	67 66	eqeltrd	$⊢ φ \to E (W) \in ℝ$
69	68	recnd	$⊢ φ \to E (W) \in ℂ$
70	69	adantr	$⊢ (φ \land W < Z) \to E (W) \in ℂ$
71	65	recnd	$⊢ φ \to ⌊\frac{B - W}{T}⌋ T \in ℂ$
72	71	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - W}{T}⌋ T \in ℂ$
73	36	adantr	$⊢ (φ \land W < Z) \to T \in ℂ$
74	70 72 73	subsubd	$⊢ (φ \land W < Z) \to E (W) - (⌊\frac{B - W}{T}⌋ T - T) = E (W) - ⌊\frac{B - W}{T}⌋ T + T$
75	74	eqcomd	$⊢ (φ \land W < Z) \to E (W) - ⌊\frac{B - W}{T}⌋ T + T = E (W) - (⌊\frac{B - W}{T}⌋ T - T)$
76	2 30	resubcld	$⊢ φ \to B - Z \in ℝ$
77	76 27 61	redivcld	$⊢ φ \to \frac{B - Z}{T} \in ℝ$
78	77	flcld	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ \in ℤ$
79	78	zred	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ \in ℝ$
80	79	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ \in ℝ$
81	27	adantr	$⊢ (φ \land W < Z) \to T \in ℝ$
82	80 81	remulcld	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T \in ℝ$
83	64	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - W}{T}⌋ \in ℝ$
84	83 81	remulcld	$⊢ (φ \land W < Z) \to ⌊\frac{B - W}{T}⌋ T \in ℝ$
85	84 81	resubcld	$⊢ (φ \land W < Z) \to ⌊\frac{B - W}{T}⌋ T - T \in ℝ$
86	68	adantr	$⊢ (φ \land W < Z) \to E (W) \in ℝ$
87	79 27	remulcld	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ T \in ℝ$
88	87	recnd	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ T \in ℂ$
89	88 36	pncand	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ T + T - T = ⌊\frac{B - Z}{T}⌋ T$
90	89	eqcomd	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ T = ⌊\frac{B - Z}{T}⌋ T + T - T$
91	90	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T = ⌊\frac{B - Z}{T}⌋ T + T - T$
92	82 81	readdcld	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T + T \in ℝ$
93	79	recnd	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ \in ℂ$
94	93 36	adddirp1d	$⊢ φ \to (⌊\frac{B - Z}{T}⌋ + 1) T = ⌊\frac{B - Z}{T}⌋ T + T$
95	94	eqcomd	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ T + T = (⌊\frac{B - Z}{T}⌋ + 1) T$
96	95	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T + T = (⌊\frac{B - Z}{T}⌋ + 1) T$
97		1red	$⊢ (φ \land W < Z) \to 1 \in ℝ$
98	80 97	readdcld	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ + 1 \in ℝ$
99		0red	$⊢ φ \to 0 \in ℝ$
100	99 27 60	ltled	$⊢ φ \to 0 \leq T$
101	100	adantr	$⊢ (φ \land W < Z) \to 0 \leq T$
102	86 31	resubcld	$⊢ (φ \land W < Z) \to E (W) - Z \in ℝ$
103	25	adantr	$⊢ (φ \land W < Z) \to W \in ℝ$
104	86 103	resubcld	$⊢ (φ \land W < Z) \to E (W) - W \in ℝ$
105	27 60	elrpd	$⊢ φ \to T \in ℝ^{+}$
106	105	adantr	$⊢ (φ \land W < Z) \to T \in ℝ^{+}$
107		simpr	$⊢ (φ \land W < Z) \to W < Z$
108	103 31 86 107	ltsub2dd	$⊢ (φ \land W < Z) \to E (W) - Z < E (W) - W$
109	102 104 106 108	ltdiv1dd	$⊢ (φ \land W < Z) \to \frac{E (W) - Z}{T} < \frac{E (W) - W}{T}$
110		id	$⊢ x = Z \to x = Z$
111		oveq2	$⊢ x = Z \to B - x = B - Z$
112	111	oveq1d	$⊢ x = Z \to \frac{B - x}{T} = \frac{B - Z}{T}$
113	112	fveq2d	$⊢ x = Z \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - Z}{T}⌋$
114	113	oveq1d	$⊢ x = Z \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - Z}{T}⌋ T$
115	110 114	oveq12d	$⊢ x = Z \to x + ⌊\frac{B - x}{T}⌋ T = Z + ⌊\frac{B - Z}{T}⌋ T$
116	115	adantl	$⊢ (φ \land x = Z) \to x + ⌊\frac{B - x}{T}⌋ T = Z + ⌊\frac{B - Z}{T}⌋ T$
117	30 87	readdcld	$⊢ φ \to Z + ⌊\frac{B - Z}{T}⌋ T \in ℝ$
118	49 116 30 117	fvmptd	$⊢ φ \to E (Z) = Z + ⌊\frac{B - Z}{T}⌋ T$
119	10 118	eqtr3d	$⊢ φ \to E (W) = Z + ⌊\frac{B - Z}{T}⌋ T$
120	119	oveq1d	$⊢ φ \to E (W) - Z = Z + ⌊\frac{B - Z}{T}⌋ T - Z$
121	30	recnd	$⊢ φ \to Z \in ℂ$
122	121 88	pncan2d	$⊢ φ \to Z + ⌊\frac{B - Z}{T}⌋ T - Z = ⌊\frac{B - Z}{T}⌋ T$
123	120 122	eqtrd	$⊢ φ \to E (W) - Z = ⌊\frac{B - Z}{T}⌋ T$
124	123	oveq1d	$⊢ φ \to \frac{E (W) - Z}{T} = \frac{⌊\frac{B - Z}{T}⌋ T}{T}$
125	93 36 61	divcan4d	$⊢ φ \to \frac{⌊\frac{B - Z}{T}⌋ T}{T} = ⌊\frac{B - Z}{T}⌋$
126	124 125	eqtr2d	$⊢ φ \to ⌊\frac{B - Z}{T}⌋ = \frac{E (W) - Z}{T}$
127	126	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ = \frac{E (W) - Z}{T}$
128	67	oveq1d	$⊢ φ \to E (W) - W = W + ⌊\frac{B - W}{T}⌋ T - W$
129	128	oveq1d	$⊢ φ \to \frac{E (W) - W}{T} = \frac{W + ⌊\frac{B - W}{T}⌋ T - W}{T}$
130	25	recnd	$⊢ φ \to W \in ℂ$
131	130 71	pncan2d	$⊢ φ \to W + ⌊\frac{B - W}{T}⌋ T - W = ⌊\frac{B - W}{T}⌋ T$
132	131	oveq1d	$⊢ φ \to \frac{W + ⌊\frac{B - W}{T}⌋ T - W}{T} = \frac{⌊\frac{B - W}{T}⌋ T}{T}$
133	64	recnd	$⊢ φ \to ⌊\frac{B - W}{T}⌋ \in ℂ$
134	133 36 61	divcan4d	$⊢ φ \to \frac{⌊\frac{B - W}{T}⌋ T}{T} = ⌊\frac{B - W}{T}⌋$
135	129 132 134	3eqtrrd	$⊢ φ \to ⌊\frac{B - W}{T}⌋ = \frac{E (W) - W}{T}$
136	135	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - W}{T}⌋ = \frac{E (W) - W}{T}$
137	109 127 136	3brtr4d	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ < ⌊\frac{B - W}{T}⌋$
138	78	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ \in ℤ$
139	63	adantr	$⊢ (φ \land W < Z) \to ⌊\frac{B - W}{T}⌋ \in ℤ$
140		zltp1le	$⊢ (⌊\frac{B - Z}{T}⌋ \in ℤ \land ⌊\frac{B - W}{T}⌋ \in ℤ) \to (⌊\frac{B - Z}{T}⌋ < ⌊\frac{B - W}{T}⌋ \leftrightarrow ⌊\frac{B - Z}{T}⌋ + 1 \leq ⌊\frac{B - W}{T}⌋)$
141	138 139 140	syl2anc	$⊢ (φ \land W < Z) \to (⌊\frac{B - Z}{T}⌋ < ⌊\frac{B - W}{T}⌋ \leftrightarrow ⌊\frac{B - Z}{T}⌋ + 1 \leq ⌊\frac{B - W}{T}⌋)$
142	137 141	mpbid	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ + 1 \leq ⌊\frac{B - W}{T}⌋$
143	98 83 81 101 142	lemul1ad	$⊢ (φ \land W < Z) \to (⌊\frac{B - Z}{T}⌋ + 1) T \leq ⌊\frac{B - W}{T}⌋ T$
144	96 143	eqbrtrd	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T + T \leq ⌊\frac{B - W}{T}⌋ T$
145	92 84 81 144	lesub1dd	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T + T - T \leq ⌊\frac{B - W}{T}⌋ T - T$
146	91 145	eqbrtrd	$⊢ (φ \land W < Z) \to ⌊\frac{B - Z}{T}⌋ T \leq ⌊\frac{B - W}{T}⌋ T - T$
147	82 85 86 146	lesub2dd	$⊢ (φ \land W < Z) \to E (W) - (⌊\frac{B - W}{T}⌋ T - T) \leq E (W) - ⌊\frac{B - Z}{T}⌋ T$
148	75 147	eqbrtrd	$⊢ (φ \land W < Z) \to E (W) - ⌊\frac{B - W}{T}⌋ T + T \leq E (W) - ⌊\frac{B - Z}{T}⌋ T$
149	67	eqcomd	$⊢ φ \to W + ⌊\frac{B - W}{T}⌋ T = E (W)$
150	69 71 130	subadd2d	$⊢ φ \to (E (W) - ⌊\frac{B - W}{T}⌋ T = W \leftrightarrow W + ⌊\frac{B - W}{T}⌋ T = E (W))$
151	149 150	mpbird	$⊢ φ \to E (W) - ⌊\frac{B - W}{T}⌋ T = W$
152	151	eqcomd	$⊢ φ \to W = E (W) - ⌊\frac{B - W}{T}⌋ T$
153	152	oveq1d	$⊢ φ \to W + T = E (W) - ⌊\frac{B - W}{T}⌋ T + T$
154	153	adantr	$⊢ (φ \land W < Z) \to W + T = E (W) - ⌊\frac{B - W}{T}⌋ T + T$
155	118	eqcomd	$⊢ φ \to Z + ⌊\frac{B - Z}{T}⌋ T = E (Z)$
156	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
157		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
158	156 2 157	syl2anc	$⊢ φ \to (A, B] \subseteq ℝ$
159	1 2 3 6 7	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
160	159 30	ffvelcdmd	$⊢ φ \to E (Z) \in (A, B]$
161	158 160	sseldd	$⊢ φ \to E (Z) \in ℝ$
162	161	recnd	$⊢ φ \to E (Z) \in ℂ$
163	162 88 121	subadd2d	$⊢ φ \to (E (Z) - ⌊\frac{B - Z}{T}⌋ T = Z \leftrightarrow Z + ⌊\frac{B - Z}{T}⌋ T = E (Z))$
164	155 163	mpbird	$⊢ φ \to E (Z) - ⌊\frac{B - Z}{T}⌋ T = Z$
165	10	oveq1d	$⊢ φ \to E (Z) - ⌊\frac{B - Z}{T}⌋ T = E (W) - ⌊\frac{B - Z}{T}⌋ T$
166	164 165	eqtr3d	$⊢ φ \to Z = E (W) - ⌊\frac{B - Z}{T}⌋ T$
167	166	adantr	$⊢ (φ \land W < Z) \to Z = E (W) - ⌊\frac{B - Z}{T}⌋ T$
168	148 154 167	3brtr4d	$⊢ (φ \land W < Z) \to W + T \leq Z$
169	21 29 31 48 168	ltletrd	$⊢ (φ \land W < Z) \to B + X < Z$
170	21 31	ltnled	$⊢ (φ \land W < Z) \to (B + X < Z \leftrightarrow \neg Z \leq B + X)$
171	169 170	mpbid	$⊢ (φ \land W < Z) \to \neg Z \leq B + X$
172	20 171	pm2.65da	$⊢ φ \to \neg W < Z$

Metamath Proof Explorer

Theorem fourierdlem19

Proof