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

Metamath Proof Explorer

Theorem nnaword

Proof