Metamath Proof Explorer

Theorem nnaordr

Description: Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002)

Ref Expression
Assertion nnaordr ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ∈ B ↔ A + 𝑜 C ∈ B + 𝑜 C

Proof

Step Hyp Ref Expression
1 nnaord ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ∈ B ↔ C + 𝑜 A ∈ C + 𝑜 B
2 nnacom ⊢ C ∈ ω ∧ A ∈ ω → C + 𝑜 A = A + 𝑜 C
3 2 ancoms ⊢ A ∈ ω ∧ C ∈ ω → C + 𝑜 A = A + 𝑜 C
4 3 3adant2 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C + 𝑜 A = A + 𝑜 C
5 nnacom ⊢ C ∈ ω ∧ B ∈ ω → C + 𝑜 B = B + 𝑜 C
6 5 ancoms ⊢ B ∈ ω ∧ C ∈ ω → C + 𝑜 B = B + 𝑜 C
7 6 3adant1 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C + 𝑜 B = B + 𝑜 C
8 4 7 eleq12d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C + 𝑜 A ∈ C + 𝑜 B ↔ A + 𝑜 C ∈ B + 𝑜 C
9 1 8 bitrd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ∈ B ↔ A + 𝑜 C ∈ B + 𝑜 C