Theorem 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	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 ·o 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐵 ) )

Proof

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