nnmsucr

Description: Multiplication with successor. Exercise 16 of Enderton p. 82. (Contributed by NM, 21-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = B \to suc A \cdot_{𝑜} x = suc A \cdot_{𝑜} B$
2		oveq2	$⊢ x = B \to A \cdot_{𝑜} x = A \cdot_{𝑜} B$
3		id	$⊢ x = B \to x = B$
4	2 3	oveq12d	$⊢ x = B \to (A \cdot_{𝑜} x) +_{𝑜} x = (A \cdot_{𝑜} B) +_{𝑜} B$
5	1 4	eqeq12d	$⊢ x = B \to (suc A \cdot_{𝑜} x = (A \cdot_{𝑜} x) +_{𝑜} x \leftrightarrow suc A \cdot_{𝑜} B = (A \cdot_{𝑜} B) +_{𝑜} B)$
6	5	imbi2d	$⊢ x = B \to ((A \in ω \to suc A \cdot_{𝑜} x = (A \cdot_{𝑜} x) +_{𝑜} x) \leftrightarrow (A \in ω \to suc A \cdot_{𝑜} B = (A \cdot_{𝑜} B) +_{𝑜} B))$
7		oveq2	$⊢ x = \emptyset \to suc A \cdot_{𝑜} x = suc A \cdot_{𝑜} \emptyset$
8		oveq2	$⊢ x = \emptyset \to A \cdot_{𝑜} x = A \cdot_{𝑜} \emptyset$
9		id	$⊢ x = \emptyset \to x = \emptyset$
10	8 9	oveq12d	$⊢ x = \emptyset \to (A \cdot_{𝑜} x) +_{𝑜} x = (A \cdot_{𝑜} \emptyset) +_{𝑜} \emptyset$
11	7 10	eqeq12d	$⊢ x = \emptyset \to (suc A \cdot_{𝑜} x = (A \cdot_{𝑜} x) +_{𝑜} x \leftrightarrow suc A \cdot_{𝑜} \emptyset = (A \cdot_{𝑜} \emptyset) +_{𝑜} \emptyset)$
12		oveq2	$⊢ x = y \to suc A \cdot_{𝑜} x = suc A \cdot_{𝑜} y$
13		oveq2	$⊢ x = y \to A \cdot_{𝑜} x = A \cdot_{𝑜} y$
14		id	$⊢ x = y \to x = y$
15	13 14	oveq12d	$⊢ x = y \to (A \cdot_{𝑜} x) +_{𝑜} x = (A \cdot_{𝑜} y) +_{𝑜} y$
16	12 15	eqeq12d	$⊢ x = y \to (suc A \cdot_{𝑜} x = (A \cdot_{𝑜} x) +_{𝑜} x \leftrightarrow suc A \cdot_{𝑜} y = (A \cdot_{𝑜} y) +_{𝑜} y)$
17		oveq2	$⊢ x = suc y \to suc A \cdot_{𝑜} x = suc A \cdot_{𝑜} suc y$
18		oveq2	$⊢ x = suc y \to A \cdot_{𝑜} x = A \cdot_{𝑜} suc y$
19		id	$⊢ x = suc y \to x = suc y$
20	18 19	oveq12d	$⊢ x = suc y \to (A \cdot_{𝑜} x) +_{𝑜} x = (A \cdot_{𝑜} suc y) +_{𝑜} suc y$
21	17 20	eqeq12d	$⊢ x = suc y \to (suc A \cdot_{𝑜} x = (A \cdot_{𝑜} x) +_{𝑜} x \leftrightarrow suc A \cdot_{𝑜} suc y = (A \cdot_{𝑜} suc y) +_{𝑜} suc y)$
22		peano2	$⊢ A \in ω \to suc A \in ω$
23		nnm0	$⊢ suc A \in ω \to suc A \cdot_{𝑜} \emptyset = \emptyset$
24	22 23	syl	$⊢ A \in ω \to suc A \cdot_{𝑜} \emptyset = \emptyset$
25		nnm0	$⊢ A \in ω \to A \cdot_{𝑜} \emptyset = \emptyset$
26	24 25	eqtr4d	$⊢ A \in ω \to suc A \cdot_{𝑜} \emptyset = A \cdot_{𝑜} \emptyset$
27		peano1	$⊢ \emptyset \in ω$
28		nnmcl	$⊢ (A \in ω \land \emptyset \in ω) \to A \cdot_{𝑜} \emptyset \in ω$
29	27 28	mpan2	$⊢ A \in ω \to A \cdot_{𝑜} \emptyset \in ω$
30		nna0	$⊢ A \cdot_{𝑜} \emptyset \in ω \to (A \cdot_{𝑜} \emptyset) +_{𝑜} \emptyset = A \cdot_{𝑜} \emptyset$
31	29 30	syl	$⊢ A \in ω \to (A \cdot_{𝑜} \emptyset) +_{𝑜} \emptyset = A \cdot_{𝑜} \emptyset$
32	26 31	eqtr4d	$⊢ A \in ω \to suc A \cdot_{𝑜} \emptyset = (A \cdot_{𝑜} \emptyset) +_{𝑜} \emptyset$
33		oveq1	$⊢ suc A \cdot_{𝑜} y = (A \cdot_{𝑜} y) +_{𝑜} y \to (suc A \cdot_{𝑜} y) +_{𝑜} suc A = ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A$
34		peano2b	$⊢ A \in ω \leftrightarrow suc A \in ω$
35		nnmsuc	$⊢ (suc A \in ω \land y \in ω) \to suc A \cdot_{𝑜} suc y = (suc A \cdot_{𝑜} y) +_{𝑜} suc A$
36	34 35	sylanb	$⊢ (A \in ω \land y \in ω) \to suc A \cdot_{𝑜} suc y = (suc A \cdot_{𝑜} y) +_{𝑜} suc A$
37		nnmcl	$⊢ (A \in ω \land y \in ω) \to A \cdot_{𝑜} y \in ω$
38		peano2b	$⊢ y \in ω \leftrightarrow suc y \in ω$
39		nnaass	$⊢ (A \cdot_{𝑜} y \in ω \land A \in ω \land suc y \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} A) +_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y)$
40	38 39	syl3an3b	$⊢ (A \cdot_{𝑜} y \in ω \land A \in ω \land y \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} A) +_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y)$
41	37 40	syl3an1	$⊢ ((A \in ω \land y \in ω) \land A \in ω \land y \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} A) +_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y)$
42	41	3expb	$⊢ ((A \in ω \land y \in ω) \land (A \in ω \land y \in ω)) \to ((A \cdot_{𝑜} y) +_{𝑜} A) +_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y)$
43	42	anidms	$⊢ (A \in ω \land y \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} A) +_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y)$
44		nnmsuc	$⊢ (A \in ω \land y \in ω) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
45	44	oveq1d	$⊢ (A \in ω \land y \in ω) \to (A \cdot_{𝑜} suc y) +_{𝑜} suc y = ((A \cdot_{𝑜} y) +_{𝑜} A) +_{𝑜} suc y$
46		nnaass	$⊢ (A \cdot_{𝑜} y \in ω \land y \in ω \land suc A \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
47	34 46	syl3an3b	$⊢ (A \cdot_{𝑜} y \in ω \land y \in ω \land A \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
48	37 47	syl3an1	$⊢ ((A \in ω \land y \in ω) \land y \in ω \land A \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
49	48	3expb	$⊢ ((A \in ω \land y \in ω) \land (y \in ω \land A \in ω)) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
50	49	an42s	$⊢ ((A \in ω \land y \in ω) \land (A \in ω \land y \in ω)) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
51	50	anidms	$⊢ (A \in ω \land y \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
52		nnacom	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} y = y +_{𝑜} A$
53		suceq	$⊢ A +_{𝑜} y = y +_{𝑜} A \to suc (A +_{𝑜} y) = suc (y +_{𝑜} A)$
54	52 53	syl	$⊢ (A \in ω \land y \in ω) \to suc (A +_{𝑜} y) = suc (y +_{𝑜} A)$
55		nnasuc	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
56		nnasuc	$⊢ (y \in ω \land A \in ω) \to y +_{𝑜} suc A = suc (y +_{𝑜} A)$
57	56	ancoms	$⊢ (A \in ω \land y \in ω) \to y +_{𝑜} suc A = suc (y +_{𝑜} A)$
58	54 55 57	3eqtr4d	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} suc y = y +_{𝑜} suc A$
59	58	oveq2d	$⊢ (A \in ω \land y \in ω) \to (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y) = (A \cdot_{𝑜} y) +_{𝑜} (y +_{𝑜} suc A)$
60	51 59	eqtr4d	$⊢ (A \in ω \land y \in ω) \to ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A = (A \cdot_{𝑜} y) +_{𝑜} (A +_{𝑜} suc y)$
61	43 45 60	3eqtr4d	$⊢ (A \in ω \land y \in ω) \to (A \cdot_{𝑜} suc y) +_{𝑜} suc y = ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A$
62	36 61	eqeq12d	$⊢ (A \in ω \land y \in ω) \to (suc A \cdot_{𝑜} suc y = (A \cdot_{𝑜} suc y) +_{𝑜} suc y \leftrightarrow (suc A \cdot_{𝑜} y) +_{𝑜} suc A = ((A \cdot_{𝑜} y) +_{𝑜} y) +_{𝑜} suc A)$
63	33 62	imbitrrid	$⊢ (A \in ω \land y \in ω) \to (suc A \cdot_{𝑜} y = (A \cdot_{𝑜} y) +_{𝑜} y \to suc A \cdot_{𝑜} suc y = (A \cdot_{𝑜} suc y) +_{𝑜} suc y)$
64	63	expcom	$⊢ y \in ω \to (A \in ω \to (suc A \cdot_{𝑜} y = (A \cdot_{𝑜} y) +_{𝑜} y \to suc A \cdot_{𝑜} suc y = (A \cdot_{𝑜} suc y) +_{𝑜} suc y))$
65	11 16 21 32 64	finds2	$⊢ x \in ω \to (A \in ω \to suc A \cdot_{𝑜} x = (A \cdot_{𝑜} x) +_{𝑜} x)$
66	6 65	vtoclga	$⊢ B \in ω \to (A \in ω \to suc A \cdot_{𝑜} B = (A \cdot_{𝑜} B) +_{𝑜} B)$
67	66	impcom	$⊢ (A \in ω \land B \in ω) \to suc A \cdot_{𝑜} B = (A \cdot_{𝑜} B) +_{𝑜} B$

Metamath Proof Explorer

Theorem nnmsucr

Proof