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