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