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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 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 𝐵 ) )