Metamath Proof Explorer

Theorem 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 
|- ( ph -> A e. RR )
fourierdlem35.b 
|- ( ph -> B e. RR )
fourierdlem35.altb 
|- ( ph -> A < B )
fourierdlem35.t 
|- T = ( B - A )
fourierdlem35.5 
|- ( ph -> X e. RR )
fourierdlem35.i 
|- ( ph -> I e. ZZ )
fourierdlem35.j 
|- ( ph -> J e. ZZ )
fourierdlem35.iel 
|- ( ph -> ( X + ( I x. T ) ) e. ( A (,] B ) )
fourierdlem35.jel 
|- ( ph -> ( X + ( J x. T ) ) e. ( A (,] B ) )
Assertion fourierdlem35 
|- ( ph -> I = J )

Proof

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