Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltapi Structured version   Visualization version   GIF version

Theorem ltapi 9927
 Description: Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ltapi (𝐶N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))

Proof of Theorem ltapi
StepHypRef Expression
1 dmaddpi 9914 . 2 dom +N = (N × N)
2 ltrelpi 9913 . 2 <N ⊆ (N × N)
3 0npi 9906 . 2 ¬ ∅ ∈ N
4 pinn 9902 . . . . . 6 (𝐴N𝐴 ∈ ω)
5 pinn 9902 . . . . . 6 (𝐵N𝐵 ∈ ω)
6 pinn 9902 . . . . . 6 (𝐶N𝐶 ∈ ω)
7 nnaord 7853 . . . . . 6 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
84, 5, 6, 7syl3an 1163 . . . . 5 ((𝐴N𝐵N𝐶N) → (𝐴𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
983expa 1111 . . . 4 (((𝐴N𝐵N) ∧ 𝐶N) → (𝐴𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
10 ltpiord 9911 . . . . 5 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
1110adantr 466 . . . 4 (((𝐴N𝐵N) ∧ 𝐶N) → (𝐴 <N 𝐵𝐴𝐵))
12 addclpi 9916 . . . . . . . 8 ((𝐶N𝐴N) → (𝐶 +N 𝐴) ∈ N)
13 addclpi 9916 . . . . . . . 8 ((𝐶N𝐵N) → (𝐶 +N 𝐵) ∈ N)
14 ltpiord 9911 . . . . . . . 8 (((𝐶 +N 𝐴) ∈ N ∧ (𝐶 +N 𝐵) ∈ N) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +N 𝐴) ∈ (𝐶 +N 𝐵)))
1512, 13, 14syl2an 583 . . . . . . 7 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +N 𝐴) ∈ (𝐶 +N 𝐵)))
16 addpiord 9908 . . . . . . . . 9 ((𝐶N𝐴N) → (𝐶 +N 𝐴) = (𝐶 +𝑜 𝐴))
1716adantr 466 . . . . . . . 8 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → (𝐶 +N 𝐴) = (𝐶 +𝑜 𝐴))
18 addpiord 9908 . . . . . . . . 9 ((𝐶N𝐵N) → (𝐶 +N 𝐵) = (𝐶 +𝑜 𝐵))
1918adantl 467 . . . . . . . 8 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → (𝐶 +N 𝐵) = (𝐶 +𝑜 𝐵))
2017, 19eleq12d 2844 . . . . . . 7 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → ((𝐶 +N 𝐴) ∈ (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
2115, 20bitrd 268 . . . . . 6 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
2221anandis 657 . . . . 5 ((𝐶N ∧ (𝐴N𝐵N)) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
2322ancoms 455 . . . 4 (((𝐴N𝐵N) ∧ 𝐶N) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
249, 11, 233bitr4d 300 . . 3 (((𝐴N𝐵N) ∧ 𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
25243impa 1100 . 2 ((𝐴N𝐵N𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
261, 2, 3, 25ndmovord 6971 1 (𝐶N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145   class class class wbr 4786  (class class class)co 6793  ωcom 7212   +𝑜 coa 7710  Ncnpi 9868   +N cpli 9869
 Copyright terms: Public domain W3C validator