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

Metamath Proof Explorer

Theorem negsub

Description: Relationship between subtraction and negative. Theorem I.3 of Apostol p. 18. (Contributed by NM, 21-Jan-1997) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	negsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 𝐵 = ( 0 − 𝐵 )
2	1	oveq2i	⊢ ( 𝐴 + - 𝐵 ) = ( 𝐴 + ( 0 − 𝐵 ) )
3	2	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 + ( 0 − 𝐵 ) ) )
4		0cn	⊢ 0 ∈ ℂ
5		addsubass	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 0 ) − 𝐵 ) = ( 𝐴 + ( 0 − 𝐵 ) ) )
6	4 5	mp3an2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 0 ) − 𝐵 ) = ( 𝐴 + ( 0 − 𝐵 ) ) )
7		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
8	7	addridd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 0 ) = 𝐴 )
9	8	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 0 ) − 𝐵 ) = ( 𝐴 − 𝐵 ) )
10	3 6 9	3eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )