Metamath Proof Explorer

Theorem fourierdlem6

Description: X is in the periodic partition, when the considered interval is centered at X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem6.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem6.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem6.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem6.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem6.5 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem6.i ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
fourierdlem6.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
fourierdlem6.iltj ⊢ ( 𝜑 → 𝐼 < 𝐽 )
fourierdlem6.iel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
fourierdlem6.jel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
Assertion fourierdlem6 ( 𝜑 → 𝐽 = ( 𝐼 + 1 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem6.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem6.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem6.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 fourierdlem6.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
5 fourierdlem6.5 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
6 fourierdlem6.i ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
7 fourierdlem6.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
8 fourierdlem6.iltj ⊢ ( 𝜑 → 𝐼 < 𝐽 )
9 fourierdlem6.iel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
10 fourierdlem6.jel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
11 7 zred ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
12 6 zred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
13 11 12 resubcld ⊢ ( 𝜑 → ( 𝐽 − 𝐼 ) ∈ ℝ )
14 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
15 4 14 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
16 13 15 remulcld ⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) ∈ ℝ )
17 1 2 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
18 3 17 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
19 18 4 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
20 15 19 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
21 1 2 10 9 iccsuble ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) − ( 𝑋 + ( 𝐼 · 𝑇 ) ) ) ≤ ( 𝐵 − 𝐴 ) )
22 11 recnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
23 12 recnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
24 15 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
25 22 23 24 subdird ⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) = ( ( 𝐽 · 𝑇 ) − ( 𝐼 · 𝑇 ) ) )
26 5 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
27 11 15 remulcld ⊢ ( 𝜑 → ( 𝐽 · 𝑇 ) ∈ ℝ )
28 27 recnd ⊢ ( 𝜑 → ( 𝐽 · 𝑇 ) ∈ ℂ )
29 12 15 remulcld ⊢ ( 𝜑 → ( 𝐼 · 𝑇 ) ∈ ℝ )
30 29 recnd ⊢ ( 𝜑 → ( 𝐼 · 𝑇 ) ∈ ℂ )
31 26 28 30 pnpcand ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) − ( 𝑋 + ( 𝐼 · 𝑇 ) ) ) = ( ( 𝐽 · 𝑇 ) − ( 𝐼 · 𝑇 ) ) )
32 25 31 eqtr4d ⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) = ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) − ( 𝑋 + ( 𝐼 · 𝑇 ) ) ) )
33 4 a1i ⊢ ( 𝜑 → 𝑇 = ( 𝐵 − 𝐴 ) )
34 21 32 33 3brtr4d ⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) ≤ 𝑇 )
35 16 15 20 34 lediv1dd ⊢ ( 𝜑 → ( ( ( 𝐽 − 𝐼 ) · 𝑇 ) / 𝑇 ) ≤ ( 𝑇 / 𝑇 ) )
36 13 recnd ⊢ ( 𝜑 → ( 𝐽 − 𝐼 ) ∈ ℂ )
37 19 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
38 36 24 37 divcan4d ⊢ ( 𝜑 → ( ( ( 𝐽 − 𝐼 ) · 𝑇 ) / 𝑇 ) = ( 𝐽 − 𝐼 ) )
39 24 37 dividd ⊢ ( 𝜑 → ( 𝑇 / 𝑇 ) = 1 )
40 35 38 39 3brtr3d ⊢ ( 𝜑 → ( 𝐽 − 𝐼 ) ≤ 1 )
41 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
42 11 12 41 lesubadd2d ⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) ≤ 1 ↔ 𝐽 ≤ ( 𝐼 + 1 ) ) )
43 40 42 mpbid ⊢ ( 𝜑 → 𝐽 ≤ ( 𝐼 + 1 ) )
44 zltp1le ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
45 6 7 44 syl2anc ⊢ ( 𝜑 → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
46 8 45 mpbid ⊢ ( 𝜑 → ( 𝐼 + 1 ) ≤ 𝐽 )
47 12 41 readdcld ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ )
48 11 47 letri3d ⊢ ( 𝜑 → ( 𝐽 = ( 𝐼 + 1 ) ↔ ( 𝐽 ≤ ( 𝐼 + 1 ) ∧ ( 𝐼 + 1 ) ≤ 𝐽 ) ) )
49 43 46 48 mpbir2and ⊢ ( 𝜑 → 𝐽 = ( 𝐼 + 1 ) )