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 
|- ( ( A e. _om /\ B e. _om ) -> ( suc A .o B ) = ( ( A .o B ) +o B ) )

Proof

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