This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐶 ) ) )