This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℂ → X + 1 2 − 1 = X − 1 2

Proof

Step Hyp Ref Expression
1 peano2cn ⊢ X ∈ ℂ → X + 1 ∈ ℂ
2 1 halfcld ⊢ X ∈ ℂ → X + 1 2 ∈ ℂ
3 peano2cnm ⊢ X + 1 2 ∈ ℂ → X + 1 2 − 1 ∈ ℂ
4 2 3 syl ⊢ X ∈ ℂ → X + 1 2 − 1 ∈ ℂ
5 peano2cnm ⊢ X ∈ ℂ → X − 1 ∈ ℂ
6 5 halfcld ⊢ X ∈ ℂ → X − 1 2 ∈ ℂ
7 2cnd ⊢ X ∈ ℂ → 2 ∈ ℂ
8 2ne0 ⊢ 2 ≠ 0
9 8 a1i ⊢ X ∈ ℂ → 2 ≠ 0
10 1cnd ⊢ X ∈ ℂ → 1 ∈ ℂ
11 2 10 7 subdird ⊢ X ∈ ℂ → X + 1 2 − 1 ⋅ 2 = X + 1 2 ⋅ 2 − 1 ⋅ 2
12 1 7 9 divcan1d ⊢ X ∈ ℂ → X + 1 2 ⋅ 2 = X + 1
13 7 mullidd ⊢ X ∈ ℂ → 1 ⋅ 2 = 2
14 12 13 oveq12d ⊢ X ∈ ℂ → X + 1 2 ⋅ 2 − 1 ⋅ 2 = X + 1 - 2
15 5 7 9 divcan1d ⊢ X ∈ ℂ → X − 1 2 ⋅ 2 = X − 1
16 2m1e1 ⊢ 2 − 1 = 1
17 16 a1i ⊢ X ∈ ℂ → 2 − 1 = 1
18 17 oveq2d ⊢ X ∈ ℂ → X − 2 − 1 = X − 1
19 id ⊢ X ∈ ℂ → X ∈ ℂ
20 19 7 10 subsub3d ⊢ X ∈ ℂ → X − 2 − 1 = X + 1 - 2
21 15 18 20 3eqtr2rd ⊢ X ∈ ℂ → X + 1 - 2 = X − 1 2 ⋅ 2
22 11 14 21 3eqtrd ⊢ X ∈ ℂ → X + 1 2 − 1 ⋅ 2 = X − 1 2 ⋅ 2
23 4 6 7 9 22 mulcan2ad ⊢ X ∈ ℂ → X + 1 2 − 1 = X − 1 2