Description: A complex number increased by 1, then divided by 2, then decreased by 1 equals the complex number decreased by 1 and then divided by 2. (Contributed by AV, 24-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | xp1d2m1eqxm1d2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano2cn | |
|
2 | 1 | halfcld | |
3 | peano2cnm | |
|
4 | 2 3 | syl | |
5 | peano2cnm | |
|
6 | 5 | halfcld | |
7 | 2cnd | |
|
8 | 2ne0 | |
|
9 | 8 | a1i | |
10 | 1cnd | |
|
11 | 2 10 7 | subdird | |
12 | 1 7 9 | divcan1d | |
13 | 7 | mulid2d | |
14 | 12 13 | oveq12d | |
15 | 5 7 9 | divcan1d | |
16 | 2m1e1 | |
|
17 | 16 | a1i | |
18 | 17 | oveq2d | |
19 | id | |
|
20 | 19 7 10 | subsub3d | |
21 | 15 18 20 | 3eqtr2rd | |
22 | 11 14 21 | 3eqtrd | |
23 | 4 6 7 9 22 | mulcan2ad | |