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 ⊢φ→A∈ℝ
fourierdlem4.b ⊢φ→B∈ℝ
fourierdlem4.altb ⊢φ→A<B
fourierdlem4.t ⊢T=B−A
fourierdlem4.e ⊢E=x∈ℝ⟼x+B−xT⁢T
Assertion fourierdlem4 ⊢φ→E:ℝ⟶AB

Proof

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