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	mullidd	$$⊢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}$$