| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-5 |
|- 5 = ( 4 + 1 ) |
| 2 |
1
|
fveq2i |
|- ( ! ` 5 ) = ( ! ` ( 4 + 1 ) ) |
| 3 |
|
4nn0 |
|- 4 e. NN0 |
| 4 |
|
facp1 |
|- ( 4 e. NN0 -> ( ! ` ( 4 + 1 ) ) = ( ( ! ` 4 ) x. ( 4 + 1 ) ) ) |
| 5 |
3 4
|
ax-mp |
|- ( ! ` ( 4 + 1 ) ) = ( ( ! ` 4 ) x. ( 4 + 1 ) ) |
| 6 |
2 5
|
eqtri |
|- ( ! ` 5 ) = ( ( ! ` 4 ) x. ( 4 + 1 ) ) |
| 7 |
|
fac4 |
|- ( ! ` 4 ) = ; 2 4 |
| 8 |
|
4p1e5 |
|- ( 4 + 1 ) = 5 |
| 9 |
7 8
|
oveq12i |
|- ( ( ! ` 4 ) x. ( 4 + 1 ) ) = ( ; 2 4 x. 5 ) |
| 10 |
|
5nn0 |
|- 5 e. NN0 |
| 11 |
|
2nn0 |
|- 2 e. NN0 |
| 12 |
|
eqid |
|- ; 2 4 = ; 2 4 |
| 13 |
|
0nn0 |
|- 0 e. NN0 |
| 14 |
|
1nn0 |
|- 1 e. NN0 |
| 15 |
|
5cn |
|- 5 e. CC |
| 16 |
|
2cn |
|- 2 e. CC |
| 17 |
|
5t2e10 |
|- ( 5 x. 2 ) = ; 1 0 |
| 18 |
15 16 17
|
mulcomli |
|- ( 2 x. 5 ) = ; 1 0 |
| 19 |
16
|
addlidi |
|- ( 0 + 2 ) = 2 |
| 20 |
14 13 11 18 19
|
decaddi |
|- ( ( 2 x. 5 ) + 2 ) = ; 1 2 |
| 21 |
|
4cn |
|- 4 e. CC |
| 22 |
|
5t4e20 |
|- ( 5 x. 4 ) = ; 2 0 |
| 23 |
15 21 22
|
mulcomli |
|- ( 4 x. 5 ) = ; 2 0 |
| 24 |
10 11 3 12 13 11 20 23
|
decmul1c |
|- ( ; 2 4 x. 5 ) = ; ; 1 2 0 |
| 25 |
9 24
|
eqtri |
|- ( ( ! ` 4 ) x. ( 4 + 1 ) ) = ; ; 1 2 0 |
| 26 |
6 25
|
eqtri |
|- ( ! ` 5 ) = ; ; 1 2 0 |