Metamath Proof Explorer

Theorem nnaordr

Description: Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002)

Ref Expression
Assertion nnaordr 
|- ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )

Proof

Step Hyp Ref Expression
1 nnaord 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
2 nnacom 
 |-  ( ( C e. _om /\ A e. _om ) -> ( C +o A ) = ( A +o C ) )
3 2 ancoms 
 |-  ( ( A e. _om /\ C e. _om ) -> ( C +o A ) = ( A +o C ) )
4 3 3adant2 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C +o A ) = ( A +o C ) )
5 nnacom 
 |-  ( ( C e. _om /\ B e. _om ) -> ( C +o B ) = ( B +o C ) )
6 5 ancoms 
 |-  ( ( B e. _om /\ C e. _om ) -> ( C +o B ) = ( B +o C ) )
7 6 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C +o B ) = ( B +o C ) )
8 4 7 eleq12d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C +o A ) e. ( C +o B ) <-> ( A +o C ) e. ( B +o C ) ) )
9 1 8 bitrd 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )