Metamath Proof Explorer


Theorem nnaword

Description: Weak ordering property of addition. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnaord
 |-  ( ( B e. _om /\ A e. _om /\ C e. _om ) -> ( B e. A <-> ( C +o B ) e. ( C +o A ) ) )
2 1 3com12
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( B e. A <-> ( C +o B ) e. ( C +o A ) ) )
3 2 notbid
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( -. B e. A <-> -. ( C +o B ) e. ( C +o A ) ) )
4 nnord
 |-  ( A e. _om -> Ord A )
5 nnord
 |-  ( B e. _om -> Ord B )
6 ordtri1
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )
7 4 5 6 syl2an
 |-  ( ( A e. _om /\ B e. _om ) -> ( A C_ B <-> -. B e. A ) )
8 7 3adant3
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B <-> -. B e. A ) )
9 nnacl
 |-  ( ( C e. _om /\ A e. _om ) -> ( C +o A ) e. _om )
10 9 ancoms
 |-  ( ( A e. _om /\ C e. _om ) -> ( C +o A ) e. _om )
11 10 3adant2
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C +o A ) e. _om )
12 nnacl
 |-  ( ( C e. _om /\ B e. _om ) -> ( C +o B ) e. _om )
13 12 ancoms
 |-  ( ( B e. _om /\ C e. _om ) -> ( C +o B ) e. _om )
14 13 3adant1
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C +o B ) e. _om )
15 nnord
 |-  ( ( C +o A ) e. _om -> Ord ( C +o A ) )
16 nnord
 |-  ( ( C +o B ) e. _om -> Ord ( C +o B ) )
17 ordtri1
 |-  ( ( Ord ( C +o A ) /\ Ord ( C +o B ) ) -> ( ( C +o A ) C_ ( C +o B ) <-> -. ( C +o B ) e. ( C +o A ) ) )
18 15 16 17 syl2an
 |-  ( ( ( C +o A ) e. _om /\ ( C +o B ) e. _om ) -> ( ( C +o A ) C_ ( C +o B ) <-> -. ( C +o B ) e. ( C +o A ) ) )
19 11 14 18 syl2anc
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C +o A ) C_ ( C +o B ) <-> -. ( C +o B ) e. ( C +o A ) ) )
20 3 8 19 3bitr4d
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )