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 x T T
fourierdlem26.6 φ X
fourierdlem26.7 φ E X = B
fourierdlem26.8 φ Y X X + 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 x T T
6 fourierdlem26.6 φ X
7 fourierdlem26.7 φ E X = B
8 fourierdlem26.8 φ Y X X + T
9 5 a1i φ E = x x + B x T T
10 simpr φ x = Y x = Y
11 10 oveq2d φ x = Y B x = B Y
12 11 oveq1d φ x = Y B x T = B Y T
13 12 fveq2d φ x = Y B x T = B Y T
14 13 oveq1d φ x = Y B x T T = B Y T T
15 10 14 oveq12d φ x = Y x + B x T T = Y + B Y T 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 X X + T Y X < Y Y X + T
21 16 19 20 syl2anc φ Y X X + 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 Y T
30 29 flcld φ B Y T
31 30 zred φ B Y T
32 31 18 remulcld φ B Y T T
33 23 32 readdcld φ Y + B Y T T
34 9 15 23 33 fvmptd φ E Y = Y + B Y T 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 Y T = B - X - Y X T
45 2 6 resubcld φ B X
46 45 recnd φ B X
47 18 recnd φ T
48 46 41 47 28 divsubdird φ B - X - Y X T = B X T Y X T
49 41 47 28 divnegd φ Y X T = Y X T
50 36 35 negsubdi2d φ Y X = X Y
51 50 oveq1d φ Y X T = X Y T
52 49 51 eqtrd φ Y X T = X Y T
53 52 oveq2d φ B X T + Y X T = B X T + X Y T
54 45 18 28 redivcld φ B X T
55 54 recnd φ B X T
56 41 47 28 divcld φ Y X T
57 55 56 negsubd φ B X T + Y X T = B X T Y X T
58 1cnd φ 1
59 55 58 npcand φ B X T - 1 + 1 = B X T
60 59 eqcomd φ B X T = B X T - 1 + 1
61 60 oveq1d φ B X T + X Y T = B X T 1 + 1 + X Y T
62 55 58 subcld φ B X T 1
63 35 36 subcld φ X Y
64 63 47 28 divcld φ X Y T
65 62 58 64 addassd φ B X T 1 + 1 + X Y T = B X T 1 + 1 + X Y T
66 61 65 eqtrd φ B X T + X Y T = B X T 1 + 1 + X Y T
67 53 57 66 3eqtr3d φ B X T Y X T = B X T 1 + 1 + X Y T
68 44 48 67 3eqtrd φ B Y T = B X T 1 + 1 + X Y T
69 68 fveq2d φ B Y T = B X T 1 + 1 + X Y T
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 φ X X + T = X T + X
75 8 74 eleqtrd φ Y X T + X
76 18 6 readdcld φ T + X
77 elioc2 X * T + X Y X T + X Y X < Y Y T + X
78 16 76 77 syl2anc φ Y X T + 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 - Y T
89 47 63 47 28 divdird φ T + X - Y T = T T + X Y T
90 47 28 dividd φ T T = 1
91 90 eqcomd φ 1 = T T
92 91 oveq1d φ 1 + X Y T = T T + X Y T
93 89 92 eqtr4d φ T + X - Y T = 1 + X Y T
94 88 93 breqtrd φ 0 1 + X Y T
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 Y T < 0
99 70 18 28 redivcld φ X Y T
100 1red φ 1
101 ltaddneg X Y T 1 X Y T < 0 1 + X Y T < 1
102 99 100 101 syl2anc φ X Y T < 0 1 + X Y T < 1
103 98 102 mpbid φ 1 + X Y T < 1
104 54 flcld φ B X T
105 104 zcnd φ B X T
106 105 47 mulcld φ B X T T
107 35 106 pncan2d φ X + B X T T - X = B X T T
108 107 eqcomd φ B X T T = X + B X T T - X
109 108 oveq1d φ B X T T T = X + B X T T - X T
110 105 47 28 divcan4d φ B X T T T = B X T
111 id x = X x = X
112 oveq2 x = X B x = B X
113 112 oveq1d x = X B x T = B X T
114 113 fveq2d x = X B x T = B X T
115 114 oveq1d x = X B x T T = B X T T
116 111 115 oveq12d x = X x + B x T T = X + B X T T
117 116 adantl φ x = X x + B x T T = X + B X T T
118 reflcl B X T B X T
119 54 118 syl φ B X T
120 119 18 remulcld φ B X T T
121 6 120 readdcld φ X + B X T T
122 9 117 6 121 fvmptd φ E X = X + B X T T
123 122 eqcomd φ X + B X T T = E X
124 123 oveq1d φ X + B X T T - X = E X X
125 124 oveq1d φ X + B X T T - X T = E X X T
126 7 oveq1d φ E X X = B X
127 126 oveq1d φ E X X T = B X T
128 125 127 eqtrd φ X + B X T T - X T = B X T
129 109 110 128 3eqtr3d φ B X T = B X T
130 129 104 eqeltrrd φ B X T
131 1zzd φ 1
132 130 131 zsubcld φ B X T 1
133 100 99 readdcld φ 1 + X Y T
134 flbi2 B X T 1 1 + X Y T B X T 1 + 1 + X Y T = B X T 1 0 1 + X Y T 1 + X Y T < 1
135 132 133 134 syl2anc φ B X T 1 + 1 + X Y T = B X T 1 0 1 + X Y T 1 + X Y T < 1
136 94 103 135 mpbir2and φ B X T 1 + 1 + X Y T = B X T 1
137 129 eqcomd φ B X T = B X T
138 137 oveq1d φ B X T 1 = B X T 1
139 69 136 138 3eqtrd φ B Y T = B X T 1
140 139 oveq1d φ B Y T T = B X T 1 T
141 140 oveq2d φ Y + B Y T T = Y + B X T 1 T
142 38 oveq1d φ Y + B X T 1 T = X + Y X + B X T 1 T
143 105 58 47 subdird φ B X T 1 T = B X T T 1 T
144 143 oveq2d φ X + Y X + B X T 1 T = X + Y X + B X T 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 X T T - 1 T = X + Y X + B X T T 1 T
148 147 eqcomd φ X + Y X + B X T T 1 T = X + Y - X + B X T T - 1 T
149 35 41 106 add32d φ X + Y X + B X T T = X + B X T T + Y X
150 149 oveq1d φ X + Y - X + B X T T - 1 T = X + B X T T + Y X - 1 T
151 123 oveq1d φ X + B X T T + Y X = E X + Y - X
152 47 mulid2d φ 1 T = T
153 151 152 oveq12d φ X + B X T 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 X T T - 1 T = A + Y - X
166 144 148 165 3eqtrd φ X + Y X + B X T 1 T = A + Y - X
167 142 166 eqtrd φ Y + B X T 1 T = A + Y - X
168 34 141 167 3eqtrd φ E Y = A + Y - X