Metamath Proof Explorer

Theorem ltapi

Description: Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion ltapi 
|- ( C e. N. -> ( A  ( C +N A )

Proof

Step Hyp Ref Expression
1 dmaddpi 
 |-  dom +N = ( N. X. N. )
2 ltrelpi 
 |-
3 0npi 
 |-  -. (/) e. N.
4 pinn 
 |-  ( A e. N. -> A e. _om )
5 pinn 
 |-  ( B e. N. -> B e. _om )
6 pinn 
 |-  ( C e. N. -> C e. _om )
7 nnaord 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
8 4 5 6 7 syl3an 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
9 8 3expa 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
10 ltpiord 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A  A e. B ) )
11 10 adantr 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A  A e. B ) )
12 addclpi 
 |-  ( ( C e. N. /\ A e. N. ) -> ( C +N A ) e. N. )
13 addclpi 
 |-  ( ( C e. N. /\ B e. N. ) -> ( C +N B ) e. N. )
14 ltpiord 
 |-  ( ( ( C +N A ) e. N. /\ ( C +N B ) e. N. ) -> ( ( C +N A )  ( C +N A ) e. ( C +N B ) ) )
15 12 13 14 syl2an 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( ( C +N A )  ( C +N A ) e. ( C +N B ) ) )
16 addpiord 
 |-  ( ( C e. N. /\ A e. N. ) -> ( C +N A ) = ( C +o A ) )
17 16 adantr 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( C +N A ) = ( C +o A ) )
18 addpiord 
 |-  ( ( C e. N. /\ B e. N. ) -> ( C +N B ) = ( C +o B ) )
19 18 adantl 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( C +N B ) = ( C +o B ) )
20 17 19 eleq12d 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( ( C +N A ) e. ( C +N B ) <-> ( C +o A ) e. ( C +o B ) ) )
21 15 20 bitrd 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( ( C +N A )  ( C +o A ) e. ( C +o B ) ) )
22 21 anandis 
 |-  ( ( C e. N. /\ ( A e. N. /\ B e. N. ) ) -> ( ( C +N A )  ( C +o A ) e. ( C +o B ) ) )
23 22 ancoms 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( C +N A )  ( C +o A ) e. ( C +o B ) ) )
24 9 11 23 3bitr4d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A  ( C +N A )
25 24 3impa 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A  ( C +N A )
26 1 2 3 25 ndmovord 
 |-  ( C e. N. -> ( A  ( C +N A )