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

Metamath Proof Explorer

Theorem subhalfhalf

Description: Subtracting the half of a number from the number yields the half of the number. (Contributed by AV, 28-Jun-2021)

Ref Expression
Assertion subhalfhalf ⊢ A ∈ ℂ → A − A 2 = A 2

Proof

Step Hyp Ref Expression
1 id ⊢ A ∈ ℂ → A ∈ ℂ
2 2cnd ⊢ A ∈ ℂ → 2 ∈ ℂ
3 2ne0 ⊢ 2 ≠ 0
4 3 a1i ⊢ A ∈ ℂ → 2 ≠ 0
5 1 2 4 divcan1d ⊢ A ∈ ℂ → A 2 ⋅ 2 = A
6 5 eqcomd ⊢ A ∈ ℂ → A = A 2 ⋅ 2
7 6 oveq1d ⊢ A ∈ ℂ → A − A 2 = A 2 ⋅ 2 − A 2
8 halfcl ⊢ A ∈ ℂ → A 2 ∈ ℂ
9 8 2 mulcomd ⊢ A ∈ ℂ → A 2 ⋅ 2 = 2 ⁢ A 2
10 9 oveq1d ⊢ A ∈ ℂ → A 2 ⋅ 2 − A 2 = 2 ⁢ A 2 − A 2
11 2 8 mulsubfacd ⊢ A ∈ ℂ → 2 ⁢ A 2 − A 2 = 2 − 1 ⁢ A 2
12 2m1e1 ⊢ 2 − 1 = 1
13 12 a1i ⊢ A ∈ ℂ → 2 − 1 = 1
14 13 oveq1d ⊢ A ∈ ℂ → 2 − 1 ⁢ A 2 = 1 ⁢ A 2
15 8 mullidd ⊢ A ∈ ℂ → 1 ⁢ A 2 = A 2
16 11 14 15 3eqtrd ⊢ A ∈ ℂ → 2 ⁢ A 2 − A 2 = A 2
17 7 10 16 3eqtrd ⊢ A ∈ ℂ → A − A 2 = A 2