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