Metamath Proof Explorer

Theorem nnaord

Description: Ordering property of addition. Proposition 8.4 of TakeutiZaring p. 58, limited to natural numbers, and its converse. (Contributed by NM, 7-Mar-1996) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnaordi 
 |-  ( ( B e. _om /\ C e. _om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
2 1 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
3 oveq2 
 |-  ( A = B -> ( C +o A ) = ( C +o B ) )
4 3 a1i 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A = B -> ( C +o A ) = ( C +o B ) ) )
5 nnaordi 
 |-  ( ( A e. _om /\ C e. _om ) -> ( B e. A -> ( C +o B ) e. ( C +o A ) ) )
6 5 3adant2 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( B e. A -> ( C +o B ) e. ( C +o A ) ) )
7 4 6 orim12d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A = B \/ B e. A ) -> ( ( C +o A ) = ( C +o B ) \/ ( C +o B ) e. ( C +o A ) ) ) )
8 7 con3d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( -. ( ( C +o A ) = ( C +o B ) \/ ( C +o B ) e. ( C +o A ) ) -> -. ( A = B \/ B e. A ) ) )
9 df-3an 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) <-> ( ( A e. _om /\ B e. _om ) /\ C e. _om ) )
10 ancom 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ C e. _om ) <-> ( C e. _om /\ ( A e. _om /\ B e. _om ) ) )
11 anandi 
 |-  ( ( C e. _om /\ ( A e. _om /\ B e. _om ) ) <-> ( ( C e. _om /\ A e. _om ) /\ ( C e. _om /\ B e. _om ) ) )
12 9 10 11 3bitri 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) <-> ( ( C e. _om /\ A e. _om ) /\ ( C e. _om /\ B e. _om ) ) )
13 nnacl 
 |-  ( ( C e. _om /\ A e. _om ) -> ( C +o A ) e. _om )
14 nnord 
 |-  ( ( C +o A ) e. _om -> Ord ( C +o A ) )
15 13 14 syl 
 |-  ( ( C e. _om /\ A e. _om ) -> Ord ( C +o A ) )
16 nnacl 
 |-  ( ( C e. _om /\ B e. _om ) -> ( C +o B ) e. _om )
17 nnord 
 |-  ( ( C +o B ) e. _om -> Ord ( C +o B ) )
18 16 17 syl 
 |-  ( ( C e. _om /\ B e. _om ) -> Ord ( C +o B ) )
19 15 18 anim12i 
 |-  ( ( ( C e. _om /\ A e. _om ) /\ ( C e. _om /\ B e. _om ) ) -> ( Ord ( C +o A ) /\ Ord ( C +o B ) ) )
20 12 19 sylbi 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( Ord ( C +o A ) /\ Ord ( C +o B ) ) )
21 ordtri2 
 |-  ( ( Ord ( C +o A ) /\ Ord ( C +o B ) ) -> ( ( C +o A ) e. ( C +o B ) <-> -. ( ( C +o A ) = ( C +o B ) \/ ( C +o B ) e. ( C +o A ) ) ) )
22 20 21 syl 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C +o A ) e. ( C +o B ) <-> -. ( ( C +o A ) = ( C +o B ) \/ ( C +o B ) e. ( C +o A ) ) ) )
23 nnord 
 |-  ( A e. _om -> Ord A )
24 nnord 
 |-  ( B e. _om -> Ord B )
25 23 24 anim12i 
 |-  ( ( A e. _om /\ B e. _om ) -> ( Ord A /\ Ord B ) )
26 25 3adant3 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( Ord A /\ Ord B ) )
27 ordtri2 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
28 26 27 syl 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
29 8 22 28 3imtr4d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C +o A ) e. ( C +o B ) -> A e. B ) )
30 2 29 impbid 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )