This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem facnn2

Description: Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004)

Ref Expression
Assertion facnn2 
|- ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )

Proof

Step Hyp Ref Expression
1 elnnnn0 
 |-  ( N e. NN <-> ( N e. CC /\ ( N - 1 ) e. NN0 ) )
2 facp1 
 |-  ( ( N - 1 ) e. NN0 -> ( ! ` ( ( N - 1 ) + 1 ) ) = ( ( ! ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) )
3 2 adantl 
 |-  ( ( N e. CC /\ ( N - 1 ) e. NN0 ) -> ( ! ` ( ( N - 1 ) + 1 ) ) = ( ( ! ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) )
4 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
5 4 fveq2d 
 |-  ( N e. CC -> ( ! ` ( ( N - 1 ) + 1 ) ) = ( ! ` N ) )
6 5 adantr 
 |-  ( ( N e. CC /\ ( N - 1 ) e. NN0 ) -> ( ! ` ( ( N - 1 ) + 1 ) ) = ( ! ` N ) )
7 4 oveq2d 
 |-  ( N e. CC -> ( ( ! ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) = ( ( ! ` ( N - 1 ) ) x. N ) )
8 7 adantr 
 |-  ( ( N e. CC /\ ( N - 1 ) e. NN0 ) -> ( ( ! ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) = ( ( ! ` ( N - 1 ) ) x. N ) )
9 3 6 8 3eqtr3d 
 |-  ( ( N e. CC /\ ( N - 1 ) e. NN0 ) -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
10 1 9 sylbi 
 |-  ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )