Metamath Proof Explorer

Theorem fourierdlem4

Description: E is a function that maps any point to a periodic corresponding point in ( A , B ] . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem4.a 
|- ( ph -> A e. RR )
fourierdlem4.b 
|- ( ph -> B e. RR )
fourierdlem4.altb 
|- ( ph -> A < B )
fourierdlem4.t 
|- T = ( B - A )
fourierdlem4.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
Assertion fourierdlem4 
|- ( ph -> E : RR --> ( A (,] B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem4.a 
 |-  ( ph -> A e. RR )
2 fourierdlem4.b 
 |-  ( ph -> B e. RR )
3 fourierdlem4.altb 
 |-  ( ph -> A < B )
4 fourierdlem4.t 
 |-  T = ( B - A )
5 fourierdlem4.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
6 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
7 2 adantr 
 |-  ( ( ph /\ x e. RR ) -> B e. RR )
8 7 6 resubcld 
 |-  ( ( ph /\ x e. RR ) -> ( B - x ) e. RR )
9 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
10 4 9 eqeltrid 
 |-  ( ph -> T e. RR )
11 10 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. RR )
12 4 a1i 
 |-  ( ph -> T = ( B - A ) )
13 2 recnd 
 |-  ( ph -> B e. CC )
14 1 recnd 
 |-  ( ph -> A e. CC )
15 1 3 gtned 
 |-  ( ph -> B =/= A )
16 13 14 15 subne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
17 12 16 eqnetrd 
 |-  ( ph -> T =/= 0 )
18 17 adantr 
 |-  ( ( ph /\ x e. RR ) -> T =/= 0 )
19 8 11 18 redivcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) e. RR )
20 19 flcld 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
21 20 zred 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
22 21 11 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
23 6 22 readdcld 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR )
24 1 adantr 
 |-  ( ( ph /\ x e. RR ) -> A e. RR )
25 24 6 resubcld 
 |-  ( ( ph /\ x e. RR ) -> ( A - x ) e. RR )
26 25 11 18 redivcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( A - x ) / T ) e. RR )
27 26 11 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A - x ) / T ) x. T ) e. RR )
28 13 addridd 
 |-  ( ph -> ( B + 0 ) = B )
29 28 eqcomd 
 |-  ( ph -> B = ( B + 0 ) )
30 13 14 subcld 
 |-  ( ph -> ( B - A ) e. CC )
31 30 subidd 
 |-  ( ph -> ( ( B - A ) - ( B - A ) ) = 0 )
32 31 eqcomd 
 |-  ( ph -> 0 = ( ( B - A ) - ( B - A ) ) )
33 32 oveq2d 
 |-  ( ph -> ( B + 0 ) = ( B + ( ( B - A ) - ( B - A ) ) ) )
34 13 30 30 addsub12d 
 |-  ( ph -> ( B + ( ( B - A ) - ( B - A ) ) ) = ( ( B - A ) + ( B - ( B - A ) ) ) )
35 13 14 nncand 
 |-  ( ph -> ( B - ( B - A ) ) = A )
36 35 oveq2d 
 |-  ( ph -> ( ( B - A ) + ( B - ( B - A ) ) ) = ( ( B - A ) + A ) )
37 30 14 addcomd 
 |-  ( ph -> ( ( B - A ) + A ) = ( A + ( B - A ) ) )
38 12 eqcomd 
 |-  ( ph -> ( B - A ) = T )
39 38 oveq2d 
 |-  ( ph -> ( A + ( B - A ) ) = ( A + T ) )
40 37 39 eqtrd 
 |-  ( ph -> ( ( B - A ) + A ) = ( A + T ) )
41 34 36 40 3eqtrd 
 |-  ( ph -> ( B + ( ( B - A ) - ( B - A ) ) ) = ( A + T ) )
42 29 33 41 3eqtrd 
 |-  ( ph -> B = ( A + T ) )
43 42 adantr 
 |-  ( ( ph /\ x e. RR ) -> B = ( A + T ) )
44 43 oveq1d 
 |-  ( ( ph /\ x e. RR ) -> ( B - x ) = ( ( A + T ) - x ) )
45 14 adantr 
 |-  ( ( ph /\ x e. RR ) -> A e. CC )
46 11 recnd 
 |-  ( ( ph /\ x e. RR ) -> T e. CC )
47 6 recnd 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
48 45 46 47 addsubd 
 |-  ( ( ph /\ x e. RR ) -> ( ( A + T ) - x ) = ( ( A - x ) + T ) )
49 44 48 eqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( B - x ) = ( ( A - x ) + T ) )
50 49 oveq1d 
 |-  ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) = ( ( ( A - x ) + T ) / T ) )
51 45 47 subcld 
 |-  ( ( ph /\ x e. RR ) -> ( A - x ) e. CC )
52 51 46 46 18 divdird 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A - x ) + T ) / T ) = ( ( ( A - x ) / T ) + ( T / T ) ) )
53 4 30 eqeltrid 
 |-  ( ph -> T e. CC )
54 53 17 dividd 
 |-  ( ph -> ( T / T ) = 1 )
55 54 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( T / T ) = 1 )
56 55 oveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A - x ) / T ) + ( T / T ) ) = ( ( ( A - x ) / T ) + 1 ) )
57 50 52 56 3eqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) = ( ( ( A - x ) / T ) + 1 ) )
58 57 fveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) )
59 58 oveq1d 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) x. T ) )
60 59 22 eqeltrrd 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) x. T ) e. RR )
61 peano2re 
 |-  ( ( ( A - x ) / T ) e. RR -> ( ( ( A - x ) / T ) + 1 ) e. RR )
62 26 61 syl 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A - x ) / T ) + 1 ) e. RR )
63 reflcl 
 |-  ( ( ( ( A - x ) / T ) + 1 ) e. RR -> ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) e. RR )
64 62 63 syl 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) e. RR )
65 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
66 3 65 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
67 66 12 breqtrrd 
 |-  ( ph -> 0 < T )
68 10 67 elrpd 
 |-  ( ph -> T e. RR+ )
69 68 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. RR+ )
70 flltp1 
 |-  ( ( ( A - x ) / T ) e. RR -> ( ( A - x ) / T ) < ( ( |_ ` ( ( A - x ) / T ) ) + 1 ) )
71 26 70 syl 
 |-  ( ( ph /\ x e. RR ) -> ( ( A - x ) / T ) < ( ( |_ ` ( ( A - x ) / T ) ) + 1 ) )
72 1zzd 
 |-  ( ( ph /\ x e. RR ) -> 1 e. ZZ )
73 fladdz 
 |-  ( ( ( ( A - x ) / T ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) = ( ( |_ ` ( ( A - x ) / T ) ) + 1 ) )
74 26 72 73 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) = ( ( |_ ` ( ( A - x ) / T ) ) + 1 ) )
75 71 74 breqtrrd 
 |-  ( ( ph /\ x e. RR ) -> ( ( A - x ) / T ) < ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) )
76 26 64 69 75 ltmul1dd 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A - x ) / T ) x. T ) < ( ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) x. T ) )
77 27 60 6 76 ltadd2dd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( ( A - x ) / T ) x. T ) ) < ( x + ( ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) x. T ) ) )
78 51 46 18 divcan1d 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A - x ) / T ) x. T ) = ( A - x ) )
79 78 oveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( ( A - x ) / T ) x. T ) ) = ( x + ( A - x ) ) )
80 47 45 pncan3d 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( A - x ) ) = A )
81 79 80 eqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( ( A - x ) / T ) x. T ) ) = A )
82 59 oveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) x. T ) ) )
83 82 eqcomd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( ( A - x ) / T ) + 1 ) ) x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
84 77 81 83 3brtr3d 
 |-  ( ( ph /\ x e. RR ) -> A < ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
85 19 11 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( B - x ) / T ) x. T ) e. RR )
86 flle 
 |-  ( ( ( B - x ) / T ) e. RR -> ( |_ ` ( ( B - x ) / T ) ) <_ ( ( B - x ) / T ) )
87 19 86 syl 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) <_ ( ( B - x ) / T ) )
88 21 19 69 lemul1d 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) <_ ( ( B - x ) / T ) <-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) <_ ( ( ( B - x ) / T ) x. T ) ) )
89 87 88 mpbid 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) <_ ( ( ( B - x ) / T ) x. T ) )
90 22 85 6 89 leadd2dd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) <_ ( x + ( ( ( B - x ) / T ) x. T ) ) )
91 8 recnd 
 |-  ( ( ph /\ x e. RR ) -> ( B - x ) e. CC )
92 91 46 18 divcan1d 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( B - x ) / T ) x. T ) = ( B - x ) )
93 92 oveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( ( B - x ) / T ) x. T ) ) = ( x + ( B - x ) ) )
94 13 adantr 
 |-  ( ( ph /\ x e. RR ) -> B e. CC )
95 47 94 pncan3d 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( B - x ) ) = B )
96 93 95 eqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( ( B - x ) / T ) x. T ) ) = B )
97 90 96 breqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) <_ B )
98 24 rexrd 
 |-  ( ( ph /\ x e. RR ) -> A e. RR* )
99 elioc2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A (,] B ) <-> ( ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR /\ A < ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) <_ B ) ) )
100 98 7 99 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A (,] B ) <-> ( ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR /\ A < ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) <_ B ) ) )
101 23 84 97 100 mpbir3and 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A (,] B ) )
102 101 5 fmptd 
 |-  ( ph -> E : RR --> ( A (,] B ) )