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	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( 𝐴 / 2 ) ) = ( 𝐴 / 2 ) )

Proof

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