Metamath Proof Explorer


Theorem xp1d2m1eqxm1d2

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 XX+121=X12

Proof

Step Hyp Ref Expression
1 peano2cn XX+1
2 1 halfcld XX+12
3 peano2cnm X+12X+121
4 2 3 syl XX+121
5 peano2cnm XX1
6 5 halfcld XX12
7 2cnd X2
8 2ne0 20
9 8 a1i X20
10 1cnd X1
11 2 10 7 subdird XX+1212=X+12212
12 1 7 9 divcan1d XX+122=X+1
13 7 mulid2d X12=2
14 12 13 oveq12d XX+12212=X+1-2
15 5 7 9 divcan1d XX122=X1
16 2m1e1 21=1
17 16 a1i X21=1
18 17 oveq2d XX21=X1
19 id XX
20 19 7 10 subsub3d XX21=X+1-2
21 15 18 20 3eqtr2rd XX+1-2=X122
22 11 14 21 3eqtrd XX+1212=X122
23 4 6 7 9 22 mulcan2ad XX+121=X12