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∈𝑵→A<𝑵B↔C+𝑵A<𝑵C+𝑵B

Proof

Step Hyp Ref Expression
1 dmaddpi ⊢dom⁡+𝑵=𝑵×𝑵
2 ltrelpi ⊢<𝑵⊆𝑵×𝑵
3 0npi ⊢¬∅∈𝑵
4 pinn ⊢A∈𝑵→A∈ω
5 pinn ⊢B∈𝑵→B∈ω
6 pinn ⊢C∈𝑵→C∈ω
7 nnaord ⊢A∈ω∧B∈ω∧C∈ω→A∈B↔C+𝑜A∈C+𝑜B
8 4 5 6 7 syl3an ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A∈B↔C+𝑜A∈C+𝑜B
9 8 3expa ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A∈B↔C+𝑜A∈C+𝑜B
10 ltpiord ⊢A∈𝑵∧B∈𝑵→A<𝑵B↔A∈B
11 10 adantr ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A<𝑵B↔A∈B
12 addclpi ⊢C∈𝑵∧A∈𝑵→C+𝑵A∈𝑵
13 addclpi ⊢C∈𝑵∧B∈𝑵→C+𝑵B∈𝑵
14 ltpiord ⊢C+𝑵A∈𝑵∧C+𝑵B∈𝑵→C+𝑵A<𝑵C+𝑵B↔C+𝑵A∈C+𝑵B
15 12 13 14 syl2an ⊢C∈𝑵∧A∈𝑵∧C∈𝑵∧B∈𝑵→C+𝑵A<𝑵C+𝑵B↔C+𝑵A∈C+𝑵B
16 addpiord ⊢C∈𝑵∧A∈𝑵→C+𝑵A=C+𝑜A
17 16 adantr ⊢C∈𝑵∧A∈𝑵∧C∈𝑵∧B∈𝑵→C+𝑵A=C+𝑜A
18 addpiord ⊢C∈𝑵∧B∈𝑵→C+𝑵B=C+𝑜B
19 18 adantl ⊢C∈𝑵∧A∈𝑵∧C∈𝑵∧B∈𝑵→C+𝑵B=C+𝑜B
20 17 19 eleq12d ⊢C∈𝑵∧A∈𝑵∧C∈𝑵∧B∈𝑵→C+𝑵A∈C+𝑵B↔C+𝑜A∈C+𝑜B
21 15 20 bitrd ⊢C∈𝑵∧A∈𝑵∧C∈𝑵∧B∈𝑵→C+𝑵A<𝑵C+𝑵B↔C+𝑜A∈C+𝑜B
22 21 anandis ⊢C∈𝑵∧A∈𝑵∧B∈𝑵→C+𝑵A<𝑵C+𝑵B↔C+𝑜A∈C+𝑜B
23 22 ancoms ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→C+𝑵A<𝑵C+𝑵B↔C+𝑜A∈C+𝑜B
24 9 11 23 3bitr4d ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A<𝑵B↔C+𝑵A<𝑵C+𝑵B
25 24 3impa ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A<𝑵B↔C+𝑵A<𝑵C+𝑵B
26 1 2 3 25 ndmovord ⊢C∈𝑵→A<𝑵B↔C+𝑵A<𝑵C+𝑵B