nnaordr

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

		Ref	Expression
	Assertion	nnaordr	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \in B \leftrightarrow A +_{𝑜} C \in (B +_{𝑜} C))$

Step	Hyp	Ref	Expression
1		nnaord	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \in B \leftrightarrow C +_{𝑜} A \in (C +_{𝑜} B))$
2		nnacom	$⊢ (C \in ω \land A \in ω) \to C +_{𝑜} A = A +_{𝑜} C$
3	2	ancoms	$⊢ (A \in ω \land C \in ω) \to C +_{𝑜} A = A +_{𝑜} C$
4	3	3adant2	$⊢ (A \in ω \land B \in ω \land C \in ω) \to C +_{𝑜} A = A +_{𝑜} C$
5		nnacom	$⊢ (C \in ω \land B \in ω) \to C +_{𝑜} B = B +_{𝑜} C$
6	5	ancoms	$⊢ (B \in ω \land C \in ω) \to C +_{𝑜} B = B +_{𝑜} C$
7	6	3adant1	$⊢ (A \in ω \land B \in ω \land C \in ω) \to C +_{𝑜} B = B +_{𝑜} C$
8	4 7	eleq12d	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (C +_{𝑜} A \in (C +_{𝑜} B) \leftrightarrow A +_{𝑜} C \in (B +_{𝑜} C))$
9	1 8	bitrd	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \in B \leftrightarrow A +_{𝑜} C \in (B +_{𝑜} C))$

Metamath Proof Explorer