This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → A ∈ ℝ
fourierdlem6.b ⊢ φ → B ∈ ℝ
fourierdlem6.altb ⊢ φ → A < B
fourierdlem6.t ⊢ T = B − A
fourierdlem6.5 ⊢ φ → X ∈ ℝ
fourierdlem6.i ⊢ φ → I ∈ ℤ
fourierdlem6.j ⊢ φ → J ∈ ℤ
fourierdlem6.iltj ⊢ φ → I < J
fourierdlem6.iel ⊢ φ → X + I ⁢ T ∈ A B
fourierdlem6.jel ⊢ φ → X + J ⁢ T ∈ A B
Assertion fourierdlem6 ⊢ φ → J = I + 1

Proof

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