# Metamath Proof Explorer

## Theorem ex-fac

Description: Example for df-fac . (Contributed by AV, 4-Sep-2021)

Ref Expression
Assertion ex-fac ${⊢}5!=120$

### Proof

Step Hyp Ref Expression
1 df-5 ${⊢}5=4+1$
2 1 fveq2i ${⊢}5!=\left(4+1\right)!$
3 4nn0 ${⊢}4\in {ℕ}_{0}$
4 facp1 ${⊢}4\in {ℕ}_{0}\to \left(4+1\right)!=4!\left(4+1\right)$
5 3 4 ax-mp ${⊢}\left(4+1\right)!=4!\left(4+1\right)$
6 2 5 eqtri ${⊢}5!=4!\left(4+1\right)$
7 fac4 ${⊢}4!=24$
8 4p1e5 ${⊢}4+1=5$
9 7 8 oveq12i ${⊢}4!\left(4+1\right)=24\cdot 5$
10 5nn0 ${⊢}5\in {ℕ}_{0}$
11 2nn0 ${⊢}2\in {ℕ}_{0}$
12 eqid ${⊢}24=24$
13 0nn0 ${⊢}0\in {ℕ}_{0}$
14 1nn0 ${⊢}1\in {ℕ}_{0}$
15 5cn ${⊢}5\in ℂ$
16 2cn ${⊢}2\in ℂ$
17 5t2e10 ${⊢}5\cdot 2=10$
18 15 16 17 mulcomli ${⊢}2\cdot 5=10$
19 16 addid2i ${⊢}0+2=2$
20 14 13 11 18 19 decaddi ${⊢}2\cdot 5+2=12$
21 4cn ${⊢}4\in ℂ$
22 5t4e20 ${⊢}5\cdot 4=20$
23 15 21 22 mulcomli ${⊢}4\cdot 5=20$
24 10 11 3 12 13 11 20 23 decmul1c ${⊢}24\cdot 5=120$
25 9 24 eqtri ${⊢}4!\left(4+1\right)=120$
26 6 25 eqtri ${⊢}5!=120$