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

Proof

Step Hyp Ref Expression
1 fourierdlem6.a 
 |-  ( ph -> A e. RR )
2 fourierdlem6.b 
 |-  ( ph -> B e. RR )
3 fourierdlem6.altb 
 |-  ( ph -> A < B )
4 fourierdlem6.t 
 |-  T = ( B - A )
5 fourierdlem6.5 
 |-  ( ph -> X e. RR )
6 fourierdlem6.i 
 |-  ( ph -> I e. ZZ )
7 fourierdlem6.j 
 |-  ( ph -> J e. ZZ )
8 fourierdlem6.iltj 
 |-  ( ph -> I < J )
9 fourierdlem6.iel 
 |-  ( ph -> ( X + ( I x. T ) ) e. ( A [,] B ) )
10 fourierdlem6.jel 
 |-  ( ph -> ( X + ( J x. T ) ) e. ( A [,] B ) )
11 7 zred 
 |-  ( ph -> J e. RR )
12 6 zred 
 |-  ( ph -> I e. RR )
13 11 12 resubcld 
 |-  ( ph -> ( J - I ) e. RR )
14 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
15 4 14 eqeltrid 
 |-  ( ph -> T e. RR )
16 13 15 remulcld 
 |-  ( ph -> ( ( J - I ) x. T ) e. RR )
17 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
18 3 17 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
19 18 4 breqtrrdi 
 |-  ( ph -> 0 < T )
20 15 19 elrpd 
 |-  ( ph -> T e. RR+ )
21 1 2 10 9 iccsuble 
 |-  ( ph -> ( ( X + ( J x. T ) ) - ( X + ( I x. T ) ) ) <_ ( B - A ) )
22 11 recnd 
 |-  ( ph -> J e. CC )
23 12 recnd 
 |-  ( ph -> I e. CC )
24 15 recnd 
 |-  ( ph -> T e. CC )
25 22 23 24 subdird 
 |-  ( ph -> ( ( J - I ) x. T ) = ( ( J x. T ) - ( I x. T ) ) )
26 5 recnd 
 |-  ( ph -> X e. CC )
27 11 15 remulcld 
 |-  ( ph -> ( J x. T ) e. RR )
28 27 recnd 
 |-  ( ph -> ( J x. T ) e. CC )
29 12 15 remulcld 
 |-  ( ph -> ( I x. T ) e. RR )
30 29 recnd 
 |-  ( ph -> ( I x. T ) e. CC )
31 26 28 30 pnpcand 
 |-  ( ph -> ( ( X + ( J x. T ) ) - ( X + ( I x. T ) ) ) = ( ( J x. T ) - ( I x. T ) ) )
32 25 31 eqtr4d 
 |-  ( ph -> ( ( J - I ) x. T ) = ( ( X + ( J x. T ) ) - ( X + ( I x. T ) ) ) )
33 4 a1i 
 |-  ( ph -> T = ( B - A ) )
34 21 32 33 3brtr4d 
 |-  ( ph -> ( ( J - I ) x. T ) <_ T )
35 16 15 20 34 lediv1dd 
 |-  ( ph -> ( ( ( J - I ) x. T ) / T ) <_ ( T / T ) )
36 13 recnd 
 |-  ( ph -> ( J - I ) e. CC )
37 19 gt0ne0d 
 |-  ( ph -> T =/= 0 )
38 36 24 37 divcan4d 
 |-  ( ph -> ( ( ( J - I ) x. T ) / T ) = ( J - I ) )
39 24 37 dividd 
 |-  ( ph -> ( T / T ) = 1 )
40 35 38 39 3brtr3d 
 |-  ( ph -> ( J - I ) <_ 1 )
41 1red 
 |-  ( ph -> 1 e. RR )
42 11 12 41 lesubadd2d 
 |-  ( ph -> ( ( J - I ) <_ 1 <-> J <_ ( I + 1 ) ) )
43 40 42 mpbid 
 |-  ( ph -> J <_ ( I + 1 ) )
44 zltp1le 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( I < J <-> ( I + 1 ) <_ J ) )
45 6 7 44 syl2anc 
 |-  ( ph -> ( I < J <-> ( I + 1 ) <_ J ) )
46 8 45 mpbid 
 |-  ( ph -> ( I + 1 ) <_ J )
47 12 41 readdcld 
 |-  ( ph -> ( I + 1 ) e. RR )
48 11 47 letri3d 
 |-  ( ph -> ( J = ( I + 1 ) <-> ( J <_ ( I + 1 ) /\ ( I + 1 ) <_ J ) ) )
49 43 46 48 mpbir2and 
 |-  ( ph -> J = ( I + 1 ) )