# Metamath Proof Explorer

## 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 ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \mathrm{suc}{A}{\cdot }_{𝑜}{B}=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{B}$

### Proof

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