Metamath Proof Explorer


Theorem nnaordr

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

Ref Expression
Assertion nnaordr ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴𝐵 ↔ ( 𝐴 +o 𝐶 ) ∈ ( 𝐵 +o 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nnaord ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴𝐵 ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
2 nnacom ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐶 +o 𝐴 ) = ( 𝐴 +o 𝐶 ) )
3 2 ancoms ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 +o 𝐴 ) = ( 𝐴 +o 𝐶 ) )
4 3 3adant2 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 +o 𝐴 ) = ( 𝐴 +o 𝐶 ) )
5 nnacom ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 +o 𝐵 ) = ( 𝐵 +o 𝐶 ) )
6 5 ancoms ( ( 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 +o 𝐵 ) = ( 𝐵 +o 𝐶 ) )
7 6 3adant1 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 +o 𝐵 ) = ( 𝐵 +o 𝐶 ) )
8 4 7 eleq12d ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ↔ ( 𝐴 +o 𝐶 ) ∈ ( 𝐵 +o 𝐶 ) ) )
9 1 8 bitrd ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴𝐵 ↔ ( 𝐴 +o 𝐶 ) ∈ ( 𝐵 +o 𝐶 ) ) )