Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | nnmsuc | |- ( ( A e. _om /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnon | |- ( A e. _om -> A e. On ) |
|
2 | onmsuc | |- ( ( A e. On /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) ) |
|
3 | 1 2 | sylan | |- ( ( A e. _om /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) ) |