Theorem risefac1

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

	Ref	Expression
Assertion	risefac1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		0p1e1	⊢ ( 0 + 1 ) = 1
2	1	oveq2i	⊢ ( 𝐴 RiseFac ( 0 + 1 ) ) = ( 𝐴 RiseFac 1 )
3		0nn0	⊢ 0 ∈ ℕ0
4		risefacp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 RiseFac ( 0 + 1 ) ) = ( ( 𝐴 RiseFac 0 ) · ( 𝐴 + 0 ) ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac ( 0 + 1 ) ) = ( ( 𝐴 RiseFac 0 ) · ( 𝐴 + 0 ) ) )
6		risefac0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac 0 ) = 1 )
7		addid1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )
8	6 7	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 RiseFac 0 ) · ( 𝐴 + 0 ) ) = ( 1 · 𝐴 ) )
9		mulid2	⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
10	5 8 9	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac ( 0 + 1 ) ) = 𝐴 )
11	2 10	eqtr3id	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac 1 ) = 𝐴 )