nndi

Description: Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
2	1	oveq2d	$⊢ x = C \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} C)$
3		oveq2	$⊢ x = C \to A \cdot_{𝑜} x = A \cdot_{𝑜} C$
4	3	oveq2d	$⊢ x = C \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)$
5	2 4	eqeq12d	$⊢ x = C \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C))$
6	5	imbi2d	$⊢ x = C \to (((A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)) \leftrightarrow ((A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)))$
7		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
8	7	oveq2d	$⊢ x = \emptyset \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} \emptyset)$
9		oveq2	$⊢ x = \emptyset \to A \cdot_{𝑜} x = A \cdot_{𝑜} \emptyset$
10	9	oveq2d	$⊢ x = \emptyset \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset)$
11	8 10	eqeq12d	$⊢ x = \emptyset \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset))$
12		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
13	12	oveq2d	$⊢ x = y \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} y)$
14		oveq2	$⊢ x = y \to A \cdot_{𝑜} x = A \cdot_{𝑜} y$
15	14	oveq2d	$⊢ x = y \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)$
16	13 15	eqeq12d	$⊢ x = y \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))$
17		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
18	17	oveq2d	$⊢ x = suc y \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} suc y)$
19		oveq2	$⊢ x = suc y \to A \cdot_{𝑜} x = A \cdot_{𝑜} suc y$
20	19	oveq2d	$⊢ x = suc y \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y)$
21	18 20	eqeq12d	$⊢ x = suc y \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))$
22		nna0	$⊢ B \in ω \to B +_{𝑜} \emptyset = B$
23	22	adantl	$⊢ (A \in ω \land B \in ω) \to B +_{𝑜} \emptyset = B$
24	23	oveq2d	$⊢ (A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} \emptyset) = A \cdot_{𝑜} B$
25		nnmcl	$⊢ (A \in ω \land B \in ω) \to A \cdot_{𝑜} B \in ω$
26		nna0	$⊢ A \cdot_{𝑜} B \in ω \to (A \cdot_{𝑜} B) +_{𝑜} \emptyset = A \cdot_{𝑜} B$
27	25 26	syl	$⊢ (A \in ω \land B \in ω) \to (A \cdot_{𝑜} B) +_{𝑜} \emptyset = A \cdot_{𝑜} B$
28	24 27	eqtr4d	$⊢ (A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} \emptyset$
29		nnm0	$⊢ A \in ω \to A \cdot_{𝑜} \emptyset = \emptyset$
30	29	adantr	$⊢ (A \in ω \land B \in ω) \to A \cdot_{𝑜} \emptyset = \emptyset$
31	30	oveq2d	$⊢ (A \in ω \land B \in ω) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} \emptyset$
32	28 31	eqtr4d	$⊢ (A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset)$
33		oveq1	$⊢ A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A = ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A$
34		nnasuc	$⊢ (B \in ω \land y \in ω) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
35	34	3adant1	$⊢ (A \in ω \land B \in ω \land y \in ω) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
36	35	oveq2d	$⊢ (A \in ω \land B \in ω \land y \in ω) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = A \cdot_{𝑜} suc (B +_{𝑜} y)$
37		nnacl	$⊢ (B \in ω \land y \in ω) \to B +_{𝑜} y \in ω$
38		nnmsuc	$⊢ (A \in ω \land B +_{𝑜} y \in ω) \to A \cdot_{𝑜} suc (B +_{𝑜} y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
39	37 38	sylan2	$⊢ (A \in ω \land (B \in ω \land y \in ω)) \to A \cdot_{𝑜} suc (B +_{𝑜} y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
40	39	3impb	$⊢ (A \in ω \land B \in ω \land y \in ω) \to A \cdot_{𝑜} suc (B +_{𝑜} y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
41	36 40	eqtrd	$⊢ (A \in ω \land B \in ω \land y \in ω) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
42		nnmsuc	$⊢ (A \in ω \land y \in ω) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
43	42	3adant2	$⊢ (A \in ω \land B \in ω \land y \in ω) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
44	43	oveq2d	$⊢ (A \in ω \land B \in ω \land y \in ω) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
45		nnmcl	$⊢ (A \in ω \land y \in ω) \to A \cdot_{𝑜} y \in ω$
46		nnaass	$⊢ (A \cdot_{𝑜} B \in ω \land A \cdot_{𝑜} y \in ω \land A \in ω) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
47	25 46	syl3an1	$⊢ ((A \in ω \land B \in ω) \land A \cdot_{𝑜} y \in ω \land A \in ω) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
48	45 47	syl3an2	$⊢ ((A \in ω \land B \in ω) \land (A \in ω \land y \in ω) \land A \in ω) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
49	48	3exp	$⊢ (A \in ω \land B \in ω) \to ((A \in ω \land y \in ω) \to (A \in ω \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)))$
50	49	exp4b	$⊢ A \in ω \to (B \in ω \to (A \in ω \to (y \in ω \to (A \in ω \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)))))$
51	50	pm2.43a	$⊢ A \in ω \to (B \in ω \to (y \in ω \to (A \in ω \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A))))$
52	51	com4r	$⊢ A \in ω \to (A \in ω \to (B \in ω \to (y \in ω \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A))))$
53	52	pm2.43i	$⊢ A \in ω \to (B \in ω \to (y \in ω \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)))$
54	53	3imp	$⊢ (A \in ω \land B \in ω \land y \in ω) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
55	44 54	eqtr4d	$⊢ (A \in ω \land B \in ω \land y \in ω) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y) = ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A$
56	41 55	eqeq12d	$⊢ (A \in ω \land B \in ω \land y \in ω) \to (A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y) \leftrightarrow (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A = ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A)$
57	33 56	imbitrrid	$⊢ (A \in ω \land B \in ω \land y \in ω) \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))$
58	57	3exp	$⊢ A \in ω \to (B \in ω \to (y \in ω \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))))$
59	58	com3r	$⊢ y \in ω \to (A \in ω \to (B \in ω \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))))$
60	59	impd	$⊢ y \in ω \to ((A \in ω \land B \in ω) \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y)))$
61	11 16 21 32 60	finds2	$⊢ x \in ω \to ((A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x))$
62	6 61	vtoclga	$⊢ C \in ω \to ((A \in ω \land B \in ω) \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C))$
63	62	expdcom	$⊢ A \in ω \to (B \in ω \to (C \in ω \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)))$
64	63	3imp	$⊢ (A \in ω \land B \in ω \land C \in ω) \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)$

Metamath Proof Explorer

Theorem nndi

Proof