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 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