Metamath Proof Explorer

Theorem fourierdlem26

Description: Periodic image of a point Y that's in the period that begins with the point X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem26.1 ⊢φ→A∈ℝ
fourierdlem26.2 ⊢φ→B∈ℝ
fourierdlem26.3 ⊢φ→A<B
fourierdlem26.4 ⊢T=B−A
fourierdlem26.5 ⊢E=x∈ℝ⟼x+B−xT⁢T
fourierdlem26.6 ⊢φ→X∈ℝ
fourierdlem26.7 ⊢φ→E⁡X=B
fourierdlem26.8 ⊢φ→Y∈XX+T
Assertion fourierdlem26 ⊢φ→E⁡Y=A+Y-X

Proof

Step Hyp Ref Expression
1 fourierdlem26.1 ⊢φ→A∈ℝ
2 fourierdlem26.2 ⊢φ→B∈ℝ
3 fourierdlem26.3 ⊢φ→A<B
4 fourierdlem26.4 ⊢T=B−A
5 fourierdlem26.5 ⊢E=x∈ℝ⟼x+B−xT⁢T
6 fourierdlem26.6 ⊢φ→X∈ℝ
7 fourierdlem26.7 ⊢φ→E⁡X=B
8 fourierdlem26.8 ⊢φ→Y∈XX+T
9 5 a1i ⊢φ→E=x∈ℝ⟼x+B−xT⁢T
10 simpr ⊢φ∧x=Y→x=Y
11 10 oveq2d ⊢φ∧x=Y→B−x=B−Y
12 11 oveq1d ⊢φ∧x=Y→B−xT=B−YT
13 12 fveq2d ⊢φ∧x=Y→B−xT=B−YT
14 13 oveq1d ⊢φ∧x=Y→B−xT⁢T=B−YT⁢T
15 10 14 oveq12d ⊢φ∧x=Y→x+B−xT⁢T=Y+B−YT⁢T
16 6 rexrd ⊢φ→X∈ℝ*
17 2 1 resubcld ⊢φ→B−A∈ℝ
18 4 17 eqeltrid ⊢φ→T∈ℝ
19 6 18 readdcld ⊢φ→X+T∈ℝ
20 elioc2 ⊢X∈ℝ*∧X+T∈ℝ→Y∈XX+T↔Y∈ℝ∧X<Y∧Y≤X+T
21 16 19 20 syl2anc ⊢φ→Y∈XX+T↔Y∈ℝ∧X<Y∧Y≤X+T
22 8 21 mpbid ⊢φ→Y∈ℝ∧X<Y∧Y≤X+T
23 22 simp1d ⊢φ→Y∈ℝ
24 2 23 resubcld ⊢φ→B−Y∈ℝ
25 1 2 posdifd ⊢φ→A<B↔0<B−A
26 3 25 mpbid ⊢φ→0<B−A
27 26 4 breqtrrdi ⊢φ→0<T
28 27 gt0ne0d ⊢φ→T≠0
29 24 18 28 redivcld ⊢φ→B−YT∈ℝ
30 29 flcld ⊢φ→B−YT∈ℤ
31 30 zred ⊢φ→B−YT∈ℝ
32 31 18 remulcld ⊢φ→B−YT⁢T∈ℝ
33 23 32 readdcld ⊢φ→Y+B−YT⁢T∈ℝ
34 9 15 23 33 fvmptd ⊢φ→E⁡Y=Y+B−YT⁢T
35 6 recnd ⊢φ→X∈ℂ
36 23 recnd ⊢φ→Y∈ℂ
37 35 36 pncan3d ⊢φ→X+Y-X=Y
38 37 eqcomd ⊢φ→Y=X+Y-X
39 38 oveq2d ⊢φ→B−Y=B−X+Y-X
40 2 recnd ⊢φ→B∈ℂ
41 36 35 subcld ⊢φ→Y−X∈ℂ
42 40 35 41 subsub4d ⊢φ→B-X-Y−X=B−X+Y-X
43 39 42 eqtr4d ⊢φ→B−Y=B-X-Y−X
44 43 oveq1d ⊢φ→B−YT=B-X-Y−XT
45 2 6 resubcld ⊢φ→B−X∈ℝ
46 45 recnd ⊢φ→B−X∈ℂ
47 18 recnd ⊢φ→T∈ℂ
48 46 41 47 28 divsubdird ⊢φ→B-X-Y−XT=B−XT−Y−XT
49 41 47 28 divnegd ⊢φ→−Y−XT=−Y−XT
50 36 35 negsubdi2d ⊢φ→−Y−X=X−Y
51 50 oveq1d ⊢φ→−Y−XT=X−YT
52 49 51 eqtrd ⊢φ→−Y−XT=X−YT
53 52 oveq2d ⊢φ→B−XT+−Y−XT=B−XT+X−YT
54 45 18 28 redivcld ⊢φ→B−XT∈ℝ
55 54 recnd ⊢φ→B−XT∈ℂ
56 41 47 28 divcld ⊢φ→Y−XT∈ℂ
57 55 56 negsubd ⊢φ→B−XT+−Y−XT=B−XT−Y−XT
58 1cnd ⊢φ→1∈ℂ
59 55 58 npcand ⊢φ→B−XT-1+1=B−XT
60 59 eqcomd ⊢φ→B−XT=B−XT-1+1
61 60 oveq1d ⊢φ→B−XT+X−YT=B−XT−1+1+X−YT
62 55 58 subcld ⊢φ→B−XT−1∈ℂ
63 35 36 subcld ⊢φ→X−Y∈ℂ
64 63 47 28 divcld ⊢φ→X−YT∈ℂ
65 62 58 64 addassd ⊢φ→B−XT−1+1+X−YT=B−XT−1+1+X−YT
66 61 65 eqtrd ⊢φ→B−XT+X−YT=B−XT−1+1+X−YT
67 53 57 66 3eqtr3d ⊢φ→B−XT−Y−XT=B−XT−1+1+X−YT
68 44 48 67 3eqtrd ⊢φ→B−YT=B−XT−1+1+X−YT
69 68 fveq2d ⊢φ→B−YT=B−XT−1+1+X−YT
70 6 23 resubcld ⊢φ→X−Y∈ℝ
71 18 70 readdcld ⊢φ→T+X-Y∈ℝ
72 18 27 elrpd ⊢φ→T∈ℝ+
73 35 47 addcomd ⊢φ→X+T=T+X
74 73 oveq2d ⊢φ→XX+T=XT+X
75 8 74 eleqtrd ⊢φ→Y∈XT+X
76 18 6 readdcld ⊢φ→T+X∈ℝ
77 elioc2 ⊢X∈ℝ*∧T+X∈ℝ→Y∈XT+X↔Y∈ℝ∧X<Y∧Y≤T+X
78 16 76 77 syl2anc ⊢φ→Y∈XT+X↔Y∈ℝ∧X<Y∧Y≤T+X
79 75 78 mpbid ⊢φ→Y∈ℝ∧X<Y∧Y≤T+X
80 79 simp3d ⊢φ→Y≤T+X
81 23 6 18 lesubaddd ⊢φ→Y−X≤T↔Y≤T+X
82 80 81 mpbird ⊢φ→Y−X≤T
83 23 6 resubcld ⊢φ→Y−X∈ℝ
84 18 83 subge0d ⊢φ→0≤T−Y−X↔Y−X≤T
85 82 84 mpbird ⊢φ→0≤T−Y−X
86 47 36 35 subsub2d ⊢φ→T−Y−X=T+X-Y
87 85 86 breqtrd ⊢φ→0≤T+X-Y
88 71 72 87 divge0d ⊢φ→0≤T+X-YT
89 47 63 47 28 divdird ⊢φ→T+X-YT=TT+X−YT
90 47 28 dividd ⊢φ→TT=1
91 90 eqcomd ⊢φ→1=TT
92 91 oveq1d ⊢φ→1+X−YT=TT+X−YT
93 89 92 eqtr4d ⊢φ→T+X-YT=1+X−YT
94 88 93 breqtrd ⊢φ→0≤1+X−YT
95 22 simp2d ⊢φ→X<Y
96 6 23 sublt0d ⊢φ→X−Y<0↔X<Y
97 95 96 mpbird ⊢φ→X−Y<0
98 70 72 97 divlt0gt0d ⊢φ→X−YT<0
99 70 18 28 redivcld ⊢φ→X−YT∈ℝ
100 1red ⊢φ→1∈ℝ
101 ltaddneg ⊢X−YT∈ℝ∧1∈ℝ→X−YT<0↔1+X−YT<1
102 99 100 101 syl2anc ⊢φ→X−YT<0↔1+X−YT<1
103 98 102 mpbid ⊢φ→1+X−YT<1
104 54 flcld ⊢φ→B−XT∈ℤ
105 104 zcnd ⊢φ→B−XT∈ℂ
106 105 47 mulcld ⊢φ→B−XT⁢T∈ℂ
107 35 106 pncan2d ⊢φ→X+B−XT⁢T-X=B−XT⁢T
108 107 eqcomd ⊢φ→B−XT⁢T=X+B−XT⁢T-X
109 108 oveq1d ⊢φ→B−XT⁢TT=X+B−XT⁢T-XT
110 105 47 28 divcan4d ⊢φ→B−XT⁢TT=B−XT
111 id ⊢x=X→x=X
112 oveq2 ⊢x=X→B−x=B−X
113 112 oveq1d ⊢x=X→B−xT=B−XT
114 113 fveq2d ⊢x=X→B−xT=B−XT
115 114 oveq1d ⊢x=X→B−xT⁢T=B−XT⁢T
116 111 115 oveq12d ⊢x=X→x+B−xT⁢T=X+B−XT⁢T
117 116 adantl ⊢φ∧x=X→x+B−xT⁢T=X+B−XT⁢T
118 reflcl ⊢B−XT∈ℝ→B−XT∈ℝ
119 54 118 syl ⊢φ→B−XT∈ℝ
120 119 18 remulcld ⊢φ→B−XT⁢T∈ℝ
121 6 120 readdcld ⊢φ→X+B−XT⁢T∈ℝ
122 9 117 6 121 fvmptd ⊢φ→E⁡X=X+B−XT⁢T
123 122 eqcomd ⊢φ→X+B−XT⁢T=E⁡X
124 123 oveq1d ⊢φ→X+B−XT⁢T-X=E⁡X−X
125 124 oveq1d ⊢φ→X+B−XT⁢T-XT=E⁡X−XT
126 7 oveq1d ⊢φ→E⁡X−X=B−X
127 126 oveq1d ⊢φ→E⁡X−XT=B−XT
128 125 127 eqtrd ⊢φ→X+B−XT⁢T-XT=B−XT
129 109 110 128 3eqtr3d ⊢φ→B−XT=B−XT
130 129 104 eqeltrrd ⊢φ→B−XT∈ℤ
131 1zzd ⊢φ→1∈ℤ
132 130 131 zsubcld ⊢φ→B−XT−1∈ℤ
133 100 99 readdcld ⊢φ→1+X−YT∈ℝ
134 flbi2 ⊢B−XT−1∈ℤ∧1+X−YT∈ℝ→B−XT−1+1+X−YT=B−XT−1↔0≤1+X−YT∧1+X−YT<1
135 132 133 134 syl2anc ⊢φ→B−XT−1+1+X−YT=B−XT−1↔0≤1+X−YT∧1+X−YT<1
136 94 103 135 mpbir2and ⊢φ→B−XT−1+1+X−YT=B−XT−1
137 129 eqcomd ⊢φ→B−XT=B−XT
138 137 oveq1d ⊢φ→B−XT−1=B−XT−1
139 69 136 138 3eqtrd ⊢φ→B−YT=B−XT−1
140 139 oveq1d ⊢φ→B−YT⁢T=B−XT−1⁢T
141 140 oveq2d ⊢φ→Y+B−YT⁢T=Y+B−XT−1⁢T
142 38 oveq1d ⊢φ→Y+B−XT−1⁢T=X+Y−X+B−XT−1⁢T
143 105 58 47 subdird ⊢φ→B−XT−1⁢T=B−XT⁢T−1⁢T
144 143 oveq2d ⊢φ→X+Y−X+B−XT−1⁢T=X+Y−X+B−XT⁢T−1⁢T
145 35 41 addcld ⊢φ→X+Y-X∈ℂ
146 58 47 mulcld ⊢φ→1⁢T∈ℂ
147 145 106 146 addsubassd ⊢φ→X+Y-X+B−XT⁢T-1⁢T=X+Y−X+B−XT⁢T−1⁢T
148 147 eqcomd ⊢φ→X+Y−X+B−XT⁢T−1⁢T=X+Y-X+B−XT⁢T-1⁢T
149 35 41 106 add32d ⊢φ→X+Y−X+B−XT⁢T=X+B−XT⁢T+Y−X
150 149 oveq1d ⊢φ→X+Y-X+B−XT⁢T-1⁢T=X+B−XT⁢T+Y−X-1⁢T
151 123 oveq1d ⊢φ→X+B−XT⁢T+Y−X=E⁡X+Y-X
152 47 mullidd ⊢φ→1⁢T=T
153 151 152 oveq12d ⊢φ→X+B−XT⁢T+Y−X-1⁢T=E⁡X+Y−X-T
154 7 2 eqeltrd ⊢φ→E⁡X∈ℝ
155 154 recnd ⊢φ→E⁡X∈ℂ
156 155 41 47 addsubd ⊢φ→E⁡X+Y−X-T=E⁡X−T+Y-X
157 7 oveq1d ⊢φ→E⁡X−T=B−T
158 4 a1i ⊢φ→T=B−A
159 158 oveq2d ⊢φ→B−T=B−B−A
160 1 recnd ⊢φ→A∈ℂ
161 40 160 nncand ⊢φ→B−B−A=A
162 157 159 161 3eqtrd ⊢φ→E⁡X−T=A
163 162 oveq1d ⊢φ→E⁡X−T+Y-X=A+Y-X
164 156 163 eqtrd ⊢φ→E⁡X+Y−X-T=A+Y-X
165 150 153 164 3eqtrd ⊢φ→X+Y-X+B−XT⁢T-1⁢T=A+Y-X
166 144 148 165 3eqtrd ⊢φ→X+Y−X+B−XT−1⁢T=A+Y-X
167 142 166 eqtrd ⊢φ→Y+B−XT−1⁢T=A+Y-X
168 34 141 167 3eqtrd ⊢φ→E⁡Y=A+Y-X