sadass

Description: Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016)

		Ref	Expression
	Assertion	sadass	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (A sadd B) sadd C = A sadd (B sadd C)$

Proof

Step	Hyp	Ref	Expression
1		sadcl	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0}) \to A sadd B \subseteq ℕ_{0}$
2		sadcl	$⊢ (A sadd B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (A sadd B) sadd C \subseteq ℕ_{0}$
3	1 2	stoic3	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (A sadd B) sadd C \subseteq ℕ_{0}$
4	3	sseld	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (k \in ((A sadd B) sadd C) \to k \in ℕ_{0})$
5		simp1	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to A \subseteq ℕ_{0}$
6		sadcl	$⊢ (B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to B sadd C \subseteq ℕ_{0}$
7	6	3adant1	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to B sadd C \subseteq ℕ_{0}$
8		sadcl	$⊢ (A \subseteq ℕ_{0} \land B sadd C \subseteq ℕ_{0}) \to A sadd (B sadd C) \subseteq ℕ_{0}$
9	5 7 8	syl2anc	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to A sadd (B sadd C) \subseteq ℕ_{0}$
10	9	sseld	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (k \in (A sadd (B sadd C)) \to k \in ℕ_{0})$
11		simpl1	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to A \subseteq ℕ_{0}$
12		simpl2	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to B \subseteq ℕ_{0}$
13		simpl3	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to C \subseteq ℕ_{0}$
14		simpr	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
15		1nn0	$⊢ 1 \in ℕ_{0}$
16	15	a1i	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to 1 \in ℕ_{0}$
17	14 16	nn0addcld	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
18	11 12 13 17	sadasslem	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to ((A sadd B) sadd C) \cap (0 ..^k + 1) = (A sadd (B sadd C)) \cap (0 ..^k + 1)$
19	18	eleq2d	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to (k \in (((A sadd B) sadd C) \cap (0 ..^k + 1)) \leftrightarrow k \in ((A sadd (B sadd C)) \cap (0 ..^k + 1)))$
20		elin	$⊢ k \in (((A sadd B) sadd C) \cap (0 ..^k + 1)) \leftrightarrow (k \in ((A sadd B) sadd C) \land k \in (0 ..^k + 1))$
21		elin	$⊢ k \in ((A sadd (B sadd C)) \cap (0 ..^k + 1)) \leftrightarrow (k \in (A sadd (B sadd C)) \land k \in (0 ..^k + 1))$
22	19 20 21	3bitr3g	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to ((k \in ((A sadd B) sadd C) \land k \in (0 ..^k + 1)) \leftrightarrow (k \in (A sadd (B sadd C)) \land k \in (0 ..^k + 1)))$
23		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
24	14 23	eleqtrdi	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
25		eluzfz2	$⊢ k \in ℤ_{\geq 0} \to k \in (0 \dots k)$
26	24 25	syl	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to k \in (0 \dots k)$
27	14	nn0zd	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℤ$
28		fzval3	$⊢ k \in ℤ \to (0 \dots k) = (0 ..^k + 1)$
29	27 28	syl	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to (0 \dots k) = (0 ..^k + 1)$
30	26 29	eleqtrd	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to k \in (0 ..^k + 1)$
31	30	biantrud	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to (k \in ((A sadd B) sadd C) \leftrightarrow (k \in ((A sadd B) sadd C) \land k \in (0 ..^k + 1)))$
32	30	biantrud	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to (k \in (A sadd (B sadd C)) \leftrightarrow (k \in (A sadd (B sadd C)) \land k \in (0 ..^k + 1)))$
33	22 31 32	3bitr4d	$⊢ ((A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \land k \in ℕ_{0}) \to (k \in ((A sadd B) sadd C) \leftrightarrow k \in (A sadd (B sadd C)))$
34	33	ex	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (k \in ℕ_{0} \to (k \in ((A sadd B) sadd C) \leftrightarrow k \in (A sadd (B sadd C))))$
35	4 10 34	pm5.21ndd	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (k \in ((A sadd B) sadd C) \leftrightarrow k \in (A sadd (B sadd C)))$
36	35	eqrdv	$⊢ (A \subseteq ℕ_{0} \land B \subseteq ℕ_{0} \land C \subseteq ℕ_{0}) \to (A sadd B) sadd C = A sadd (B sadd C)$

Metamath Proof Explorer

Theorem sadass

Proof