Metamath Proof Explorer

Theorem ex-fac

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

Ref Expression
Assertion ex-fac ( ! ‘ 5 ) = 1 2 0

Proof

Step Hyp Ref Expression
1 df-5 ⊢ 5 = ( 4 + 1 )
2 1 fveq2i ⊢ ( ! ‘ 5 ) = ( ! ‘ ( 4 + 1 ) )
3 4nn0 ⊢ 4 ∈ ℕ0
4 facp1 ⊢ ( 4 ∈ ℕ0 → ( ! ‘ ( 4 + 1 ) ) = ( ( ! ‘ 4 ) · ( 4 + 1 ) ) )
5 3 4 ax-mp ⊢ ( ! ‘ ( 4 + 1 ) ) = ( ( ! ‘ 4 ) · ( 4 + 1 ) )
6 2 5 eqtri ⊢ ( ! ‘ 5 ) = ( ( ! ‘ 4 ) · ( 4 + 1 ) )
7 fac4 ⊢ ( ! ‘ 4 ) = 2 4
8 4p1e5 ⊢ ( 4 + 1 ) = 5
9 7 8 oveq12i ⊢ ( ( ! ‘ 4 ) · ( 4 + 1 ) ) = ( 2 4 · 5 )
10 5nn0 ⊢ 5 ∈ ℕ0
11 2nn0 ⊢ 2 ∈ ℕ0
12 eqid ⊢ 2 4 = 2 4
13 0nn0 ⊢ 0 ∈ ℕ0
14 1nn0 ⊢ 1 ∈ ℕ0
15 5cn ⊢ 5 ∈ ℂ
16 2cn ⊢ 2 ∈ ℂ
17 5t2e10 ⊢ ( 5 · 2 ) = 1 0
18 15 16 17 mulcomli ⊢ ( 2 · 5 ) = 1 0
19 16 addlidi ⊢ ( 0 + 2 ) = 2
20 14 13 11 18 19 decaddi ⊢ ( ( 2 · 5 ) + 2 ) = 1 2
21 4cn ⊢ 4 ∈ ℂ
22 5t4e20 ⊢ ( 5 · 4 ) = 2 0
23 15 21 22 mulcomli ⊢ ( 4 · 5 ) = 2 0
24 10 11 3 12 13 11 20 23 decmul1c ⊢ ( 2 4 · 5 ) = 1 2 0
25 9 24 eqtri ⊢ ( ( ! ‘ 4 ) · ( 4 + 1 ) ) = 1 2 0
26 6 25 eqtri ⊢ ( ! ‘ 5 ) = 1 2 0