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 ) ) )