Metamath Proof Explorer

Theorem npcan1

Description: Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018)

Ref Expression
Assertion npcan1 
|- ( A e. CC -> ( ( A - 1 ) + 1 ) = A )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. CC -> A e. CC )
2 1cnd 
 |-  ( A e. CC -> 1 e. CC )
3 1 2 npcand 
 |-  ( A e. CC -> ( ( A - 1 ) + 1 ) = A )