Step |
Hyp |
Ref |
Expression |
1 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
2 |
|
fallrisefac |
⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 FallFac 0 ) = ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) ) |
3 |
1 2
|
mpan2 |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) ) |
4 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
5 |
|
exp0 |
⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 ) |
6 |
4 5
|
mp1i |
⊢ ( 𝐴 ∈ ℂ → ( - 1 ↑ 0 ) = 1 ) |
7 |
|
negcl |
⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ ) |
8 |
|
risefac0 |
⊢ ( - 𝐴 ∈ ℂ → ( - 𝐴 RiseFac 0 ) = 1 ) |
9 |
7 8
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 RiseFac 0 ) = 1 ) |
10 |
6 9
|
oveq12d |
⊢ ( 𝐴 ∈ ℂ → ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) = ( 1 · 1 ) ) |
11 |
|
1t1e1 |
⊢ ( 1 · 1 ) = 1 |
12 |
10 11
|
eqtrdi |
⊢ ( 𝐴 ∈ ℂ → ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) = 1 ) |
13 |
3 12
|
eqtrd |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 ) |