Metamath Proof Explorer

Theorem negsubi

Description: Relationship between subtraction and negative. Theorem I.3 of Apostol p. 18. (Contributed by NM, 26-Nov-1994) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypotheses negidi.1 A
pncan3i.2 B
Assertion negsubi A + B = A B


Step Hyp Ref Expression
1 negidi.1 A
2 pncan3i.2 B
3 negsub A B A + B = A B
4 1 2 3 mp2an A + B = A B