# 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 ${⊢}{X}\in ℂ\to \left(\frac{{X}+1}{2}\right)-1=\frac{{X}-1}{2}$

### Proof

Step Hyp Ref Expression
1 peano2cn ${⊢}{X}\in ℂ\to {X}+1\in ℂ$
2 1 halfcld ${⊢}{X}\in ℂ\to \frac{{X}+1}{2}\in ℂ$
3 peano2cnm ${⊢}\frac{{X}+1}{2}\in ℂ\to \left(\frac{{X}+1}{2}\right)-1\in ℂ$
4 2 3 syl ${⊢}{X}\in ℂ\to \left(\frac{{X}+1}{2}\right)-1\in ℂ$
5 peano2cnm ${⊢}{X}\in ℂ\to {X}-1\in ℂ$
6 5 halfcld ${⊢}{X}\in ℂ\to \frac{{X}-1}{2}\in ℂ$
7 2cnd ${⊢}{X}\in ℂ\to 2\in ℂ$
8 2ne0 ${⊢}2\ne 0$
9 8 a1i ${⊢}{X}\in ℂ\to 2\ne 0$
10 1cnd ${⊢}{X}\in ℂ\to 1\in ℂ$
11 2 10 7 subdird ${⊢}{X}\in ℂ\to \left(\left(\frac{{X}+1}{2}\right)-1\right)\cdot 2=\left(\frac{{X}+1}{2}\right)\cdot 2-1\cdot 2$
12 1 7 9 divcan1d ${⊢}{X}\in ℂ\to \left(\frac{{X}+1}{2}\right)\cdot 2={X}+1$
13 7 mulid2d ${⊢}{X}\in ℂ\to 1\cdot 2=2$
14 12 13 oveq12d ${⊢}{X}\in ℂ\to \left(\frac{{X}+1}{2}\right)\cdot 2-1\cdot 2={X}+1-2$
15 5 7 9 divcan1d ${⊢}{X}\in ℂ\to \left(\frac{{X}-1}{2}\right)\cdot 2={X}-1$
16 2m1e1 ${⊢}2-1=1$
17 16 a1i ${⊢}{X}\in ℂ\to 2-1=1$
18 17 oveq2d ${⊢}{X}\in ℂ\to {X}-\left(2-1\right)={X}-1$
19 id ${⊢}{X}\in ℂ\to {X}\in ℂ$
20 19 7 10 subsub3d ${⊢}{X}\in ℂ\to {X}-\left(2-1\right)={X}+1-2$
21 15 18 20 3eqtr2rd ${⊢}{X}\in ℂ\to {X}+1-2=\left(\frac{{X}-1}{2}\right)\cdot 2$
22 11 14 21 3eqtrd ${⊢}{X}\in ℂ\to \left(\left(\frac{{X}+1}{2}\right)-1\right)\cdot 2=\left(\frac{{X}-1}{2}\right)\cdot 2$
23 4 6 7 9 22 mulcan2ad ${⊢}{X}\in ℂ\to \left(\frac{{X}+1}{2}\right)-1=\frac{{X}-1}{2}$