nnaord

Description: Ordering property of addition. Proposition 8.4 of TakeutiZaring p. 58, limited to natural numbers, and its converse. (Contributed by NM, 7-Mar-1996) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nnaordi	$⊢ (B \in ω \land C \in ω) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$
2	1	3adant1	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$
3		oveq2	$⊢ A = B \to C +_{𝑜} A = C +_{𝑜} B$
4	3	a1i	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A = B \to C +_{𝑜} A = C +_{𝑜} B)$
5		nnaordi	$⊢ (A \in ω \land C \in ω) \to (B \in A \to C +_{𝑜} B \in (C +_{𝑜} A))$
6	5	3adant2	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (B \in A \to C +_{𝑜} B \in (C +_{𝑜} A))$
7	4 6	orim12d	$⊢ (A \in ω \land B \in ω \land C \in ω) \to ((A = B \lor B \in A) \to (C +_{𝑜} A = C +_{𝑜} B \lor C +_{𝑜} B \in (C +_{𝑜} A)))$
8	7	con3d	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (\neg (C +_{𝑜} A = C +_{𝑜} B \lor C +_{𝑜} B \in (C +_{𝑜} A)) \to \neg (A = B \lor B \in A))$
9		df-3an	$⊢ (A \in ω \land B \in ω \land C \in ω) \leftrightarrow ((A \in ω \land B \in ω) \land C \in ω)$
10		ancom	$⊢ ((A \in ω \land B \in ω) \land C \in ω) \leftrightarrow (C \in ω \land (A \in ω \land B \in ω))$
11		anandi	$⊢ (C \in ω \land (A \in ω \land B \in ω)) \leftrightarrow ((C \in ω \land A \in ω) \land (C \in ω \land B \in ω))$
12	9 10 11	3bitri	$⊢ (A \in ω \land B \in ω \land C \in ω) \leftrightarrow ((C \in ω \land A \in ω) \land (C \in ω \land B \in ω))$
13		nnacl	$⊢ (C \in ω \land A \in ω) \to C +_{𝑜} A \in ω$
14		nnord	$⊢ C +_{𝑜} A \in ω \to Ord (C +_{𝑜} A)$
15	13 14	syl	$⊢ (C \in ω \land A \in ω) \to Ord (C +_{𝑜} A)$
16		nnacl	$⊢ (C \in ω \land B \in ω) \to C +_{𝑜} B \in ω$
17		nnord	$⊢ C +_{𝑜} B \in ω \to Ord (C +_{𝑜} B)$
18	16 17	syl	$⊢ (C \in ω \land B \in ω) \to Ord (C +_{𝑜} B)$
19	15 18	anim12i	$⊢ ((C \in ω \land A \in ω) \land (C \in ω \land B \in ω)) \to (Ord (C +_{𝑜} A) \land Ord (C +_{𝑜} B))$
20	12 19	sylbi	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (Ord (C +_{𝑜} A) \land Ord (C +_{𝑜} B))$
21		ordtri2	$⊢ (Ord (C +_{𝑜} A) \land Ord (C +_{𝑜} B)) \to (C +_{𝑜} A \in (C +_{𝑜} B) \leftrightarrow \neg (C +_{𝑜} A = C +_{𝑜} B \lor C +_{𝑜} B \in (C +_{𝑜} A)))$
22	20 21	syl	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (C +_{𝑜} A \in (C +_{𝑜} B) \leftrightarrow \neg (C +_{𝑜} A = C +_{𝑜} B \lor C +_{𝑜} B \in (C +_{𝑜} A)))$
23		nnord	$⊢ A \in ω \to Ord A$
24		nnord	$⊢ B \in ω \to Ord B$
25	23 24	anim12i	$⊢ (A \in ω \land B \in ω) \to (Ord A \land Ord B)$
26	25	3adant3	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (Ord A \land Ord B)$
27		ordtri2	$⊢ (Ord A \land Ord B) \to (A \in B \leftrightarrow \neg (A = B \lor B \in A))$
28	26 27	syl	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \in B \leftrightarrow \neg (A = B \lor B \in A))$
29	8 22 28	3imtr4d	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (C +_{𝑜} A \in (C +_{𝑜} B) \to A \in B)$
30	2 29	impbid	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \in B \leftrightarrow C +_{𝑜} A \in (C +_{𝑜} B))$

Metamath Proof Explorer

Theorem nnaord

Proof