Metamath Proof Explorer

Theorem nn0sub2

Description: Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005)

Ref Expression
Assertion nn0sub2 
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( N - M ) e. NN0 )

Proof

Step Hyp Ref Expression
1 nn0sub 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )
2 1 biimp3a 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( N - M ) e. NN0 )