Metamath Proof Explorer


Theorem fourierdlem19

Description: If two elements of D have the same periodic image in ( A (,] B ) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem19.a φ A
fourierdlem19.b φ B
fourierdlem19.altb φ A < B
fourierdlem19.x φ X
fourierdlem19.d D = y A + X B + X | k y + k T C
fourierdlem19.t T = B A
fourierdlem19.e E = x x + B x T T
fourierdlem19.w φ W D
fourierdlem19.z φ Z D
fourierdlem19.ezew φ E Z = E W
Assertion fourierdlem19 φ ¬ W < Z

Proof

Step Hyp Ref Expression
1 fourierdlem19.a φ A
2 fourierdlem19.b φ B
3 fourierdlem19.altb φ A < B
4 fourierdlem19.x φ X
5 fourierdlem19.d D = y A + X B + X | k y + k T C
6 fourierdlem19.t T = B A
7 fourierdlem19.e E = x x + B x T T
8 fourierdlem19.w φ W D
9 fourierdlem19.z φ Z D
10 fourierdlem19.ezew φ E Z = E W
11 1 4 readdcld φ A + X
12 11 rexrd φ A + X *
13 2 4 readdcld φ B + X
14 13 rexrd φ B + X *
15 ssrab2 y A + X B + X | k y + k T C A + X B + X
16 5 15 eqsstri D A + X B + X
17 16 9 sseldi φ Z A + X B + X
18 iocleub A + X * B + X * Z A + X B + X Z B + X
19 12 14 17 18 syl3anc φ Z B + X
20 19 adantr φ W < Z Z B + X
21 13 adantr φ W < Z B + X
22 iocssre A + X * B + X A + X B + X
23 12 13 22 syl2anc φ A + X B + X
24 16 8 sseldi φ W A + X B + X
25 23 24 sseldd φ W
26 2 1 resubcld φ B A
27 6 26 eqeltrid φ T
28 25 27 readdcld φ W + T
29 28 adantr φ W < Z W + T
30 23 17 sseldd φ Z
31 30 adantr φ W < Z Z
32 6 eqcomi B A = T
33 32 a1i φ B A = T
34 2 recnd φ B
35 1 recnd φ A
36 27 recnd φ T
37 34 35 36 subaddd φ B A = T A + T = B
38 33 37 mpbid φ A + T = B
39 38 eqcomd φ B = A + T
40 39 oveq1d φ B + X = A + T + X
41 4 recnd φ X
42 35 36 41 add32d φ A + T + X = A + X + T
43 40 42 eqtrd φ B + X = A + X + T
44 iocgtlb A + X * B + X * W A + X B + X A + X < W
45 12 14 24 44 syl3anc φ A + X < W
46 11 25 27 45 ltadd1dd φ A + X + T < W + T
47 43 46 eqbrtrd φ B + X < W + T
48 47 adantr φ W < Z B + X < W + T
49 7 a1i φ E = x x + B x T T
50 id x = W x = W
51 oveq2 x = W B x = B W
52 51 oveq1d x = W B x T = B W T
53 52 fveq2d x = W B x T = B W T
54 53 oveq1d x = W B x T T = B W T T
55 50 54 oveq12d x = W x + B x T T = W + B W T T
56 55 adantl φ x = W x + B x T T = W + B W T T
57 2 25 resubcld φ B W
58 1 2 posdifd φ A < B 0 < B A
59 3 58 mpbid φ 0 < B A
60 59 6 breqtrrdi φ 0 < T
61 60 gt0ne0d φ T 0
62 57 27 61 redivcld φ B W T
63 62 flcld φ B W T
64 63 zred φ B W T
65 64 27 remulcld φ B W T T
66 25 65 readdcld φ W + B W T T
67 49 56 25 66 fvmptd φ E W = W + B W T T
68 67 66 eqeltrd φ E W
69 68 recnd φ E W
70 69 adantr φ W < Z E W
71 65 recnd φ B W T T
72 71 adantr φ W < Z B W T T
73 36 adantr φ W < Z T
74 70 72 73 subsubd φ W < Z E W B W T T T = E W - B W T T + T
75 74 eqcomd φ W < Z E W - B W T T + T = E W B W T T T
76 2 30 resubcld φ B Z
77 76 27 61 redivcld φ B Z T
78 77 flcld φ B Z T
79 78 zred φ B Z T
80 79 adantr φ W < Z B Z T
81 27 adantr φ W < Z T
82 80 81 remulcld φ W < Z B Z T T
83 64 adantr φ W < Z B W T
84 83 81 remulcld φ W < Z B W T T
85 84 81 resubcld φ W < Z B W T T T
86 68 adantr φ W < Z E W
87 79 27 remulcld φ B Z T T
88 87 recnd φ B Z T T
89 88 36 pncand φ B Z T T + T - T = B Z T T
90 89 eqcomd φ B Z T T = B Z T T + T - T
91 90 adantr φ W < Z B Z T T = B Z T T + T - T
92 82 81 readdcld φ W < Z B Z T T + T
93 79 recnd φ B Z T
94 93 36 adddirp1d φ B Z T + 1 T = B Z T T + T
95 94 eqcomd φ B Z T T + T = B Z T + 1 T
96 95 adantr φ W < Z B Z T T + T = B Z T + 1 T
97 1red φ W < Z 1
98 80 97 readdcld φ W < Z B Z T + 1
99 0red φ 0
100 99 27 60 ltled φ 0 T
101 100 adantr φ W < Z 0 T
102 86 31 resubcld φ W < Z E W Z
103 25 adantr φ W < Z W
104 86 103 resubcld φ W < Z E W W
105 27 60 elrpd φ T +
106 105 adantr φ W < Z T +
107 simpr φ W < Z W < Z
108 103 31 86 107 ltsub2dd φ W < Z E W Z < E W W
109 102 104 106 108 ltdiv1dd φ W < Z E W Z T < E W W T
110 id x = Z x = Z
111 oveq2 x = Z B x = B Z
112 111 oveq1d x = Z B x T = B Z T
113 112 fveq2d x = Z B x T = B Z T
114 113 oveq1d x = Z B x T T = B Z T T
115 110 114 oveq12d x = Z x + B x T T = Z + B Z T T
116 115 adantl φ x = Z x + B x T T = Z + B Z T T
117 30 87 readdcld φ Z + B Z T T
118 49 116 30 117 fvmptd φ E Z = Z + B Z T T
119 10 118 eqtr3d φ E W = Z + B Z T T
120 119 oveq1d φ E W Z = Z + B Z T T - Z
121 30 recnd φ Z
122 121 88 pncan2d φ Z + B Z T T - Z = B Z T T
123 120 122 eqtrd φ E W Z = B Z T T
124 123 oveq1d φ E W Z T = B Z T T T
125 93 36 61 divcan4d φ B Z T T T = B Z T
126 124 125 eqtr2d φ B Z T = E W Z T
127 126 adantr φ W < Z B Z T = E W Z T
128 67 oveq1d φ E W W = W + B W T T - W
129 128 oveq1d φ E W W T = W + B W T T - W T
130 25 recnd φ W
131 130 71 pncan2d φ W + B W T T - W = B W T T
132 131 oveq1d φ W + B W T T - W T = B W T T T
133 64 recnd φ B W T
134 133 36 61 divcan4d φ B W T T T = B W T
135 129 132 134 3eqtrrd φ B W T = E W W T
136 135 adantr φ W < Z B W T = E W W T
137 109 127 136 3brtr4d φ W < Z B Z T < B W T
138 78 adantr φ W < Z B Z T
139 63 adantr φ W < Z B W T
140 zltp1le B Z T B W T B Z T < B W T B Z T + 1 B W T
141 138 139 140 syl2anc φ W < Z B Z T < B W T B Z T + 1 B W T
142 137 141 mpbid φ W < Z B Z T + 1 B W T
143 98 83 81 101 142 lemul1ad φ W < Z B Z T + 1 T B W T T
144 96 143 eqbrtrd φ W < Z B Z T T + T B W T T
145 92 84 81 144 lesub1dd φ W < Z B Z T T + T - T B W T T T
146 91 145 eqbrtrd φ W < Z B Z T T B W T T T
147 82 85 86 146 lesub2dd φ W < Z E W B W T T T E W B Z T T
148 75 147 eqbrtrd φ W < Z E W - B W T T + T E W B Z T T
149 67 eqcomd φ W + B W T T = E W
150 69 71 130 subadd2d φ E W B W T T = W W + B W T T = E W
151 149 150 mpbird φ E W B W T T = W
152 151 eqcomd φ W = E W B W T T
153 152 oveq1d φ W + T = E W - B W T T + T
154 153 adantr φ W < Z W + T = E W - B W T T + T
155 118 eqcomd φ Z + B Z T T = E Z
156 1 rexrd φ A *
157 iocssre A * B A B
158 156 2 157 syl2anc φ A B
159 1 2 3 6 7 fourierdlem4 φ E : A B
160 159 30 ffvelrnd φ E Z A B
161 158 160 sseldd φ E Z
162 161 recnd φ E Z
163 162 88 121 subadd2d φ E Z B Z T T = Z Z + B Z T T = E Z
164 155 163 mpbird φ E Z B Z T T = Z
165 10 oveq1d φ E Z B Z T T = E W B Z T T
166 164 165 eqtr3d φ Z = E W B Z T T
167 166 adantr φ W < Z Z = E W B Z T T
168 148 154 167 3brtr4d φ W < Z W + T Z
169 21 29 31 48 168 ltletrd φ W < Z B + X < Z
170 21 31 ltnled φ W < Z B + X < Z ¬ Z B + X
171 169 170 mpbid φ W < Z ¬ Z B + X
172 20 171 pm2.65da φ ¬ W < Z