nnaass

Description: Addition of natural numbers is associative. Theorem 4K(1) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = C \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} C$
2		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
3	2	oveq2d	$⊢ x = C \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} C)$
4	1 3	eqeq12d	$⊢ x = C \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C))$
5	4	imbi2d	$⊢ x = C \to (((A \in ω \land B \in ω) \to (A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x)) \leftrightarrow ((A \in ω \land B \in ω) \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C)))$
6		oveq2	$⊢ x = \emptyset \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} \emptyset$
7		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
8	7	oveq2d	$⊢ x = \emptyset \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} \emptyset)$
9	6 8	eqeq12d	$⊢ x = \emptyset \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} (B +_{𝑜} \emptyset))$
10		oveq2	$⊢ x = y \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} y$
11		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
12	11	oveq2d	$⊢ x = y \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} y)$
13	10 12	eqeq12d	$⊢ x = y \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y))$
14		oveq2	$⊢ x = suc y \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} suc y$
15		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
16	15	oveq2d	$⊢ x = suc y \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} suc y)$
17	14 16	eqeq12d	$⊢ x = suc y \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y))$
18		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
19		nna0	$⊢ A +_{𝑜} B \in ω \to (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} B$
20	18 19	syl	$⊢ (A \in ω \land B \in ω) \to (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} B$
21		nna0	$⊢ B \in ω \to B +_{𝑜} \emptyset = B$
22	21	oveq2d	$⊢ B \in ω \to A +_{𝑜} (B +_{𝑜} \emptyset) = A +_{𝑜} B$
23	22	adantl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} (B +_{𝑜} \emptyset) = A +_{𝑜} B$
24	20 23	eqtr4d	$⊢ (A \in ω \land B \in ω) \to (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} (B +_{𝑜} \emptyset)$
25		suceq	$⊢ (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to suc ((A +_{𝑜} B) +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y))$
26		nnasuc	$⊢ (A +_{𝑜} B \in ω \land y \in ω) \to (A +_{𝑜} B) +_{𝑜} suc y = suc ((A +_{𝑜} B) +_{𝑜} y)$
27	18 26	sylan	$⊢ ((A \in ω \land B \in ω) \land y \in ω) \to (A +_{𝑜} B) +_{𝑜} suc y = suc ((A +_{𝑜} B) +_{𝑜} y)$
28		nnasuc	$⊢ (B \in ω \land y \in ω) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
29	28	oveq2d	$⊢ (B \in ω \land y \in ω) \to A +_{𝑜} (B +_{𝑜} suc y) = A +_{𝑜} suc (B +_{𝑜} y)$
30	29	adantl	$⊢ (A \in ω \land (B \in ω \land y \in ω)) \to A +_{𝑜} (B +_{𝑜} suc y) = A +_{𝑜} suc (B +_{𝑜} y)$
31		nnacl	$⊢ (B \in ω \land y \in ω) \to B +_{𝑜} y \in ω$
32		nnasuc	$⊢ (A \in ω \land B +_{𝑜} y \in ω) \to A +_{𝑜} suc (B +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y))$
33	31 32	sylan2	$⊢ (A \in ω \land (B \in ω \land y \in ω)) \to A +_{𝑜} suc (B +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y))$
34	30 33	eqtrd	$⊢ (A \in ω \land (B \in ω \land y \in ω)) \to A +_{𝑜} (B +_{𝑜} suc y) = suc (A +_{𝑜} (B +_{𝑜} y))$
35	34	anassrs	$⊢ ((A \in ω \land B \in ω) \land y \in ω) \to A +_{𝑜} (B +_{𝑜} suc y) = suc (A +_{𝑜} (B +_{𝑜} y))$
36	27 35	eqeq12d	$⊢ ((A \in ω \land B \in ω) \land y \in ω) \to ((A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y) \leftrightarrow suc ((A +_{𝑜} B) +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y)))$
37	25 36	imbitrrid	$⊢ ((A \in ω \land B \in ω) \land y \in ω) \to ((A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to (A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y))$
38	37	expcom	$⊢ y \in ω \to ((A \in ω \land B \in ω) \to ((A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to (A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y)))$
39	9 13 17 24 38	finds2	$⊢ x \in ω \to ((A \in ω \land B \in ω) \to (A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x))$
40	5 39	vtoclga	$⊢ C \in ω \to ((A \in ω \land B \in ω) \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C))$
41	40	com12	$⊢ (A \in ω \land B \in ω) \to (C \in ω \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C))$
42	41	3impia	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C)$

Metamath Proof Explorer

Theorem nnaass

Proof