Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  onmsuc Structured version   Unicode version

Theorem onmsuc 6765
 Description: Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
Assertion
Ref Expression
onmsuc

Proof of Theorem onmsuc
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 peano2 4857 . . . . 5
2 nnon 4843 . . . . 5
31, 2syl 16 . . . 4
4 omv 6748 . . . 4
53, 4sylan2 461 . . 3
61adantl 453 . . . 4
7 fvres 5737 . . . 4
86, 7syl 16 . . 3
95, 8eqtr4d 2470 . 2
10 ovex 6098 . . . . 5
11 oveq1 6080 . . . . . 6
12 eqid 2435 . . . . . 6
13 ovex 6098 . . . . . 6
1411, 12, 13fvmpt 5798 . . . . 5
1510, 14ax-mp 8 . . . 4
16 nnon 4843 . . . . . . 7
17 omv 6748 . . . . . . 7
1816, 17sylan2 461 . . . . . 6
19 fvres 5737 . . . . . . 7
2019adantl 453 . . . . . 6
2118, 20eqtr4d 2470 . . . . 5
2221fveq2d 5724 . . . 4
2315, 22syl5eqr 2481 . . 3
24 frsuc 6686 . . . 4