fourierdlem35

Description: There is a single point in ( A (,] B ) that's distant from X a multiple integer of T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem35.a	$⊢ φ \to A \in ℝ$
	fourierdlem35.b	$⊢ φ \to B \in ℝ$
	fourierdlem35.altb	$⊢ φ \to A < B$
	fourierdlem35.t	$⊢ T = B - A$
	fourierdlem35.5	$⊢ φ \to X \in ℝ$
	fourierdlem35.i	$⊢ φ \to I \in ℤ$
	fourierdlem35.j	$⊢ φ \to J \in ℤ$
	fourierdlem35.iel	$⊢ φ \to X + I T \in (A, B]$
	fourierdlem35.jel	$⊢ φ \to X + J T \in (A, B]$
Assertion	fourierdlem35	$⊢ φ \to I = J$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem35.a	$⊢ φ \to A \in ℝ$
2		fourierdlem35.b	$⊢ φ \to B \in ℝ$
3		fourierdlem35.altb	$⊢ φ \to A < B$
4		fourierdlem35.t	$⊢ T = B - A$
5		fourierdlem35.5	$⊢ φ \to X \in ℝ$
6		fourierdlem35.i	$⊢ φ \to I \in ℤ$
7		fourierdlem35.j	$⊢ φ \to J \in ℤ$
8		fourierdlem35.iel	$⊢ φ \to X + I T \in (A, B]$
9		fourierdlem35.jel	$⊢ φ \to X + J T \in (A, B]$
10		neqne	$⊢ \neg I = J \to I \neq J$
11	1	adantr	$⊢ (φ \land I < J) \to A \in ℝ$
12	2	adantr	$⊢ (φ \land I < J) \to B \in ℝ$
13	3	adantr	$⊢ (φ \land I < J) \to A < B$
14	5	adantr	$⊢ (φ \land I < J) \to X \in ℝ$
15	6	adantr	$⊢ (φ \land I < J) \to I \in ℤ$
16	7	adantr	$⊢ (φ \land I < J) \to J \in ℤ$
17		simpr	$⊢ (φ \land I < J) \to I < J$
18		iocssicc	$⊢ (A, B] \subseteq [A, B]$
19	18 8	sselid	$⊢ φ \to X + I T \in [A, B]$
20	19	adantr	$⊢ (φ \land I < J) \to X + I T \in [A, B]$
21	18 9	sselid	$⊢ φ \to X + J T \in [A, B]$
22	21	adantr	$⊢ (φ \land I < J) \to X + J T \in [A, B]$
23	11 12 13 4 14 15 16 17 20 22	fourierdlem6	$⊢ (φ \land I < J) \to J = I + 1$
24	23	orcd	$⊢ (φ \land I < J) \to (J = I + 1 \lor I = J + 1)$
25	24	adantlr	$⊢ ((φ \land I \neq J) \land I < J) \to (J = I + 1 \lor I = J + 1)$
26		simpll	$⊢ ((φ \land I \neq J) \land \neg I < J) \to φ$
27	7	zred	$⊢ φ \to J \in ℝ$
28	26 27	syl	$⊢ ((φ \land I \neq J) \land \neg I < J) \to J \in ℝ$
29	6	zred	$⊢ φ \to I \in ℝ$
30	26 29	syl	$⊢ ((φ \land I \neq J) \land \neg I < J) \to I \in ℝ$
31		id	$⊢ I \neq J \to I \neq J$
32	31	necomd	$⊢ I \neq J \to J \neq I$
33	32	ad2antlr	$⊢ ((φ \land I \neq J) \land \neg I < J) \to J \neq I$
34		simpr	$⊢ ((φ \land I \neq J) \land \neg I < J) \to \neg I < J$
35	28 30 33 34	lttri5d	$⊢ ((φ \land I \neq J) \land \neg I < J) \to J < I$
36	1	adantr	$⊢ (φ \land J < I) \to A \in ℝ$
37	2	adantr	$⊢ (φ \land J < I) \to B \in ℝ$
38	3	adantr	$⊢ (φ \land J < I) \to A < B$
39	5	adantr	$⊢ (φ \land J < I) \to X \in ℝ$
40	7	adantr	$⊢ (φ \land J < I) \to J \in ℤ$
41	6	adantr	$⊢ (φ \land J < I) \to I \in ℤ$
42		simpr	$⊢ (φ \land J < I) \to J < I$
43	21	adantr	$⊢ (φ \land J < I) \to X + J T \in [A, B]$
44	19	adantr	$⊢ (φ \land J < I) \to X + I T \in [A, B]$
45	36 37 38 4 39 40 41 42 43 44	fourierdlem6	$⊢ (φ \land J < I) \to I = J + 1$
46	45	olcd	$⊢ (φ \land J < I) \to (J = I + 1 \lor I = J + 1)$
47	26 35 46	syl2anc	$⊢ ((φ \land I \neq J) \land \neg I < J) \to (J = I + 1 \lor I = J + 1)$
48	25 47	pm2.61dan	$⊢ (φ \land I \neq J) \to (J = I + 1 \lor I = J + 1)$
49	10 48	sylan2	$⊢ (φ \land \neg I = J) \to (J = I + 1 \lor I = J + 1)$
50	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
51	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
52		iocleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land X + J T \in (A, B]) \to X + J T \leq B$
53	50 51 9 52	syl3anc	$⊢ φ \to X + J T \leq B$
54	53	adantr	$⊢ (φ \land J = I + 1) \to X + J T \leq B$
55	1	adantr	$⊢ (φ \land J = I + 1) \to A \in ℝ$
56	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
57	4 56	eqeltrid	$⊢ φ \to T \in ℝ$
58	29 57	remulcld	$⊢ φ \to I T \in ℝ$
59	5 58	readdcld	$⊢ φ \to X + I T \in ℝ$
60	59	adantr	$⊢ (φ \land J = I + 1) \to X + I T \in ℝ$
61	57	adantr	$⊢ (φ \land J = I + 1) \to T \in ℝ$
62		iocgtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land X + I T \in (A, B]) \to A < X + I T$
63	50 51 8 62	syl3anc	$⊢ φ \to A < X + I T$
64	63	adantr	$⊢ (φ \land J = I + 1) \to A < X + I T$
65	55 60 61 64	ltadd1dd	$⊢ (φ \land J = I + 1) \to A + T < X + I T + T$
66	4	eqcomi	$⊢ B - A = T$
67	2	recnd	$⊢ φ \to B \in ℂ$
68	1	recnd	$⊢ φ \to A \in ℂ$
69	57	recnd	$⊢ φ \to T \in ℂ$
70	67 68 69	subaddd	$⊢ φ \to (B - A = T \leftrightarrow A + T = B)$
71	66 70	mpbii	$⊢ φ \to A + T = B$
72	71	eqcomd	$⊢ φ \to B = A + T$
73	72	adantr	$⊢ (φ \land J = I + 1) \to B = A + T$
74	5	recnd	$⊢ φ \to X \in ℂ$
75	58	recnd	$⊢ φ \to I T \in ℂ$
76	74 75 69	addassd	$⊢ φ \to X + I T + T = X + I T + T$
77	76	adantr	$⊢ (φ \land J = I + 1) \to X + I T + T = X + I T + T$
78	29	recnd	$⊢ φ \to I \in ℂ$
79	78 69	adddirp1d	$⊢ φ \to (I + 1) T = I T + T$
80	79	eqcomd	$⊢ φ \to I T + T = (I + 1) T$
81	80	oveq2d	$⊢ φ \to X + I T + T = X + (I + 1) T$
82	81	adantr	$⊢ (φ \land J = I + 1) \to X + I T + T = X + (I + 1) T$
83		oveq1	$⊢ J = I + 1 \to J T = (I + 1) T$
84	83	eqcomd	$⊢ J = I + 1 \to (I + 1) T = J T$
85	84	oveq2d	$⊢ J = I + 1 \to X + (I + 1) T = X + J T$
86	85	adantl	$⊢ (φ \land J = I + 1) \to X + (I + 1) T = X + J T$
87	77 82 86	3eqtrrd	$⊢ (φ \land J = I + 1) \to X + J T = X + I T + T$
88	65 73 87	3brtr4d	$⊢ (φ \land J = I + 1) \to B < X + J T$
89	2	adantr	$⊢ (φ \land J = I + 1) \to B \in ℝ$
90	27 57	remulcld	$⊢ φ \to J T \in ℝ$
91	5 90	readdcld	$⊢ φ \to X + J T \in ℝ$
92	91	adantr	$⊢ (φ \land J = I + 1) \to X + J T \in ℝ$
93	89 92	ltnled	$⊢ (φ \land J = I + 1) \to (B < X + J T \leftrightarrow \neg X + J T \leq B)$
94	88 93	mpbid	$⊢ (φ \land J = I + 1) \to \neg X + J T \leq B$
95	54 94	pm2.65da	$⊢ φ \to \neg J = I + 1$
96		iocleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land X + I T \in (A, B]) \to X + I T \leq B$
97	50 51 8 96	syl3anc	$⊢ φ \to X + I T \leq B$
98	97	adantr	$⊢ (φ \land I = J + 1) \to X + I T \leq B$
99	1	adantr	$⊢ (φ \land I = J + 1) \to A \in ℝ$
100	91	adantr	$⊢ (φ \land I = J + 1) \to X + J T \in ℝ$
101	57	adantr	$⊢ (φ \land I = J + 1) \to T \in ℝ$
102		iocgtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land X + J T \in (A, B]) \to A < X + J T$
103	50 51 9 102	syl3anc	$⊢ φ \to A < X + J T$
104	103	adantr	$⊢ (φ \land I = J + 1) \to A < X + J T$
105	99 100 101 104	ltadd1dd	$⊢ (φ \land I = J + 1) \to A + T < X + J T + T$
106	72	adantr	$⊢ (φ \land I = J + 1) \to B = A + T$
107	90	recnd	$⊢ φ \to J T \in ℂ$
108	74 107 69	addassd	$⊢ φ \to X + J T + T = X + J T + T$
109	108	adantr	$⊢ (φ \land I = J + 1) \to X + J T + T = X + J T + T$
110	27	recnd	$⊢ φ \to J \in ℂ$
111	110 69	adddirp1d	$⊢ φ \to (J + 1) T = J T + T$
112	111	eqcomd	$⊢ φ \to J T + T = (J + 1) T$
113	112	oveq2d	$⊢ φ \to X + J T + T = X + (J + 1) T$
114	113	adantr	$⊢ (φ \land I = J + 1) \to X + J T + T = X + (J + 1) T$
115		oveq1	$⊢ I = J + 1 \to I T = (J + 1) T$
116	115	eqcomd	$⊢ I = J + 1 \to (J + 1) T = I T$
117	116	oveq2d	$⊢ I = J + 1 \to X + (J + 1) T = X + I T$
118	117	adantl	$⊢ (φ \land I = J + 1) \to X + (J + 1) T = X + I T$
119	109 114 118	3eqtrrd	$⊢ (φ \land I = J + 1) \to X + I T = X + J T + T$
120	105 106 119	3brtr4d	$⊢ (φ \land I = J + 1) \to B < X + I T$
121	2	adantr	$⊢ (φ \land I = J + 1) \to B \in ℝ$
122	59	adantr	$⊢ (φ \land I = J + 1) \to X + I T \in ℝ$
123	121 122	ltnled	$⊢ (φ \land I = J + 1) \to (B < X + I T \leftrightarrow \neg X + I T \leq B)$
124	120 123	mpbid	$⊢ (φ \land I = J + 1) \to \neg X + I T \leq B$
125	98 124	pm2.65da	$⊢ φ \to \neg I = J + 1$
126	95 125	jca	$⊢ φ \to (\neg J = I + 1 \land \neg I = J + 1)$
127	126	adantr	$⊢ (φ \land \neg I = J) \to (\neg J = I + 1 \land \neg I = J + 1)$
128		pm4.56	$⊢ (\neg J = I + 1 \land \neg I = J + 1) \leftrightarrow \neg (J = I + 1 \lor I = J + 1)$
129	127 128	sylib	$⊢ (φ \land \neg I = J) \to \neg (J = I + 1 \lor I = J + 1)$
130	49 129	condan	$⊢ φ \to I = J$

Metamath Proof Explorer

Theorem fourierdlem35

Proof