Metamath Proof Explorer


Theorem negsubdii

Description: Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999)

Ref Expression
Hypotheses negidi.1 𝐴 ∈ ℂ
pncan3i.2 𝐵 ∈ ℂ
Assertion negsubdii - ( 𝐴𝐵 ) = ( - 𝐴 + 𝐵 )

Proof

Step Hyp Ref Expression
1 negidi.1 𝐴 ∈ ℂ
2 pncan3i.2 𝐵 ∈ ℂ
3 2 negcli - 𝐵 ∈ ℂ
4 1 3 negdii - ( 𝐴 + - 𝐵 ) = ( - 𝐴 + - - 𝐵 )
5 1 2 negsubi ( 𝐴 + - 𝐵 ) = ( 𝐴𝐵 )
6 5 negeqi - ( 𝐴 + - 𝐵 ) = - ( 𝐴𝐵 )
7 2 negnegi - - 𝐵 = 𝐵
8 7 oveq2i ( - 𝐴 + - - 𝐵 ) = ( - 𝐴 + 𝐵 )
9 4 6 8 3eqtr3i - ( 𝐴𝐵 ) = ( - 𝐴 + 𝐵 )