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 ( 𝜑𝐴 ∈ ℝ )
fourierdlem35.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem35.altb ( 𝜑𝐴 < 𝐵 )
fourierdlem35.t 𝑇 = ( 𝐵𝐴 )
fourierdlem35.5 ( 𝜑𝑋 ∈ ℝ )
fourierdlem35.i ( 𝜑𝐼 ∈ ℤ )
fourierdlem35.j ( 𝜑𝐽 ∈ ℤ )
fourierdlem35.iel ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
fourierdlem35.jel ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
Assertion fourierdlem35 ( 𝜑𝐼 = 𝐽 )

Proof

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