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

Metamath Proof Explorer

Theorem fallfac1

Description: The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfac1 ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 1 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 0p1e1 ⊢ ( 0 + 1 ) = 1
2 1 oveq2i ⊢ ( 𝐴 FallFac ( 0 + 1 ) ) = ( 𝐴 FallFac 1 )
3 0nn0 ⊢ 0 ∈ ℕ0
4 fallfacp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 FallFac ( 0 + 1 ) ) = ( ( 𝐴 FallFac 0 ) · ( 𝐴 − 0 ) ) )
5 3 4 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac ( 0 + 1 ) ) = ( ( 𝐴 FallFac 0 ) · ( 𝐴 − 0 ) ) )
6 fallfac0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 )
7 subid1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 0 ) = 𝐴 )
8 6 7 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 FallFac 0 ) · ( 𝐴 − 0 ) ) = ( 1 · 𝐴 ) )
9 mullid ⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
10 5 8 9 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac ( 0 + 1 ) ) = 𝐴 )
11 2 10 eqtr3id ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 1 ) = 𝐴 )