Metamath Proof Explorer

Theorem fourierdlem7

Description: The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem7.a 
|- ( ph -> A e. RR )
fourierdlem7.b 
|- ( ph -> B e. RR )
fourierdlem7.altb 
|- ( ph -> A < B )
fourierdlem7.t 
|- T = ( B - A )
fourierdlem7.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem7.x 
|- ( ph -> X e. RR )
fourierdlem7.y 
|- ( ph -> Y e. RR )
fourierdlem7.xlty 
|- ( ph -> X <_ Y )
Assertion fourierdlem7 
|- ( ph -> ( ( E ` Y ) - Y ) <_ ( ( E ` X ) - X ) )

Proof

Step Hyp Ref Expression
1 fourierdlem7.a 
 |-  ( ph -> A e. RR )
2 fourierdlem7.b 
 |-  ( ph -> B e. RR )
3 fourierdlem7.altb 
 |-  ( ph -> A < B )
4 fourierdlem7.t 
 |-  T = ( B - A )
5 fourierdlem7.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
6 fourierdlem7.x 
 |-  ( ph -> X e. RR )
7 fourierdlem7.y 
 |-  ( ph -> Y e. RR )
8 fourierdlem7.xlty 
 |-  ( ph -> X <_ Y )
9 2 7 resubcld 
 |-  ( ph -> ( B - Y ) e. RR )
10 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
11 4 10 eqeltrid 
 |-  ( ph -> T e. RR )
12 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
13 3 12 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
14 13 4 breqtrrdi 
 |-  ( ph -> 0 < T )
15 14 gt0ne0d 
 |-  ( ph -> T =/= 0 )
16 9 11 15 redivcld 
 |-  ( ph -> ( ( B - Y ) / T ) e. RR )
17 2 6 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
18 17 11 15 redivcld 
 |-  ( ph -> ( ( B - X ) / T ) e. RR )
19 11 14 elrpd 
 |-  ( ph -> T e. RR+ )
20 6 7 2 8 lesub2dd 
 |-  ( ph -> ( B - Y ) <_ ( B - X ) )
21 9 17 19 20 lediv1dd 
 |-  ( ph -> ( ( B - Y ) / T ) <_ ( ( B - X ) / T ) )
22 flwordi 
 |-  ( ( ( ( B - Y ) / T ) e. RR /\ ( ( B - X ) / T ) e. RR /\ ( ( B - Y ) / T ) <_ ( ( B - X ) / T ) ) -> ( |_ ` ( ( B - Y ) / T ) ) <_ ( |_ ` ( ( B - X ) / T ) ) )
23 16 18 21 22 syl3anc 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) <_ ( |_ ` ( ( B - X ) / T ) ) )
24 16 flcld 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. ZZ )
25 24 zred 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. RR )
26 18 flcld 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
27 26 zred 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
28 25 27 19 lemul1d 
 |-  ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) <_ ( |_ ` ( ( B - X ) / T ) ) <-> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) <_ ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
29 23 28 mpbid 
 |-  ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) <_ ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
30 5 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
31 id 
 |-  ( x = Y -> x = Y )
32 oveq2 
 |-  ( x = Y -> ( B - x ) = ( B - Y ) )
33 32 oveq1d 
 |-  ( x = Y -> ( ( B - x ) / T ) = ( ( B - Y ) / T ) )
34 33 fveq2d 
 |-  ( x = Y -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - Y ) / T ) ) )
35 34 oveq1d 
 |-  ( x = Y -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
36 31 35 oveq12d 
 |-  ( x = Y -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
37 36 adantl 
 |-  ( ( ph /\ x = Y ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
38 25 11 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. RR )
39 7 38 readdcld 
 |-  ( ph -> ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) e. RR )
40 30 37 7 39 fvmptd 
 |-  ( ph -> ( E ` Y ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
41 40 oveq1d 
 |-  ( ph -> ( ( E ` Y ) - Y ) = ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) )
42 7 recnd 
 |-  ( ph -> Y e. CC )
43 38 recnd 
 |-  ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. CC )
44 42 43 pncan2d 
 |-  ( ph -> ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
45 41 44 eqtrd 
 |-  ( ph -> ( ( E ` Y ) - Y ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
46 id 
 |-  ( x = X -> x = X )
47 oveq2 
 |-  ( x = X -> ( B - x ) = ( B - X ) )
48 47 oveq1d 
 |-  ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
49 48 fveq2d 
 |-  ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
50 49 oveq1d 
 |-  ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
51 46 50 oveq12d 
 |-  ( x = X -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
52 51 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
53 27 11 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
54 6 53 readdcld 
 |-  ( ph -> ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
55 30 52 6 54 fvmptd 
 |-  ( ph -> ( E ` X ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
56 55 oveq1d 
 |-  ( ph -> ( ( E ` X ) - X ) = ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) )
57 6 recnd 
 |-  ( ph -> X e. CC )
58 53 recnd 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
59 57 58 pncan2d 
 |-  ( ph -> ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
60 56 59 eqtrd 
 |-  ( ph -> ( ( E ` X ) - X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
61 29 45 60 3brtr4d 
 |-  ( ph -> ( ( E ` Y ) - Y ) <_ ( ( E ` X ) - X ) )