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

Metamath Proof Explorer

Theorem sub2times

Description: Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion sub2times ( 𝐴 ∈ ℂ → ( 𝐴 − ( 2 · 𝐴 ) ) = - 𝐴 )

Proof

Step Hyp Ref Expression
1 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( 2 · 𝐴 ) ) = ( 𝐴 − ( 𝐴 + 𝐴 ) ) )
3 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
4 3 3 addcld ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 𝐴 ) ∈ ℂ )
5 3 4 negsubd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( 𝐴 + 𝐴 ) ) = ( 𝐴 − ( 𝐴 + 𝐴 ) ) )
6 3 3 negdid ⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 + 𝐴 ) = ( - 𝐴 + - 𝐴 ) )
7 6 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( 𝐴 + 𝐴 ) ) = ( 𝐴 + ( - 𝐴 + - 𝐴 ) ) )
8 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
9 3 8 8 addassd ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + - 𝐴 ) + - 𝐴 ) = ( 𝐴 + ( - 𝐴 + - 𝐴 ) ) )
10 negid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )
11 10 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + - 𝐴 ) + - 𝐴 ) = ( 0 + - 𝐴 ) )
12 8 addlidd ⊢ ( 𝐴 ∈ ℂ → ( 0 + - 𝐴 ) = - 𝐴 )
13 11 12 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + - 𝐴 ) + - 𝐴 ) = - 𝐴 )
14 7 9 13 3eqtr2d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( 𝐴 + 𝐴 ) ) = - 𝐴 )
15 2 5 14 3eqtr2d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( 2 · 𝐴 ) ) = - 𝐴 )