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 addid1d
 |-  ( 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 ) )