Step |
Hyp |
Ref |
Expression |
1 |
|
nn0cn |
|- ( N e. NN0 -> N e. CC ) |
2 |
1
|
2timesd |
|- ( N e. NN0 -> ( 2 x. N ) = ( N + N ) ) |
3 |
2
|
oveq2d |
|- ( N e. NN0 -> ( -u 1 ^ ( 2 x. N ) ) = ( -u 1 ^ ( N + N ) ) ) |
4 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
5 |
|
m1expeven |
|- ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = 1 ) |
6 |
4 5
|
syl |
|- ( N e. NN0 -> ( -u 1 ^ ( 2 x. N ) ) = 1 ) |
7 |
|
neg1cn |
|- -u 1 e. CC |
8 |
|
expadd |
|- ( ( -u 1 e. CC /\ N e. NN0 /\ N e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) ) |
9 |
7 8
|
mp3an1 |
|- ( ( N e. NN0 /\ N e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) ) |
10 |
9
|
anidms |
|- ( N e. NN0 -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) ) |
11 |
3 6 10
|
3eqtr3rd |
|- ( N e. NN0 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
12 |
11
|
adantl |
|- ( ( X e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
13 |
|
negneg |
|- ( X e. CC -> -u -u X = X ) |
14 |
13
|
adantr |
|- ( ( X e. CC /\ N e. NN0 ) -> -u -u X = X ) |
15 |
14
|
oveq1d |
|- ( ( X e. CC /\ N e. NN0 ) -> ( -u -u X FallFac N ) = ( X FallFac N ) ) |
16 |
12 15
|
oveq12d |
|- ( ( X e. CC /\ N e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( -u -u X FallFac N ) ) = ( 1 x. ( X FallFac N ) ) ) |
17 |
|
expcl |
|- ( ( -u 1 e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC ) |
18 |
7 17
|
mpan |
|- ( N e. NN0 -> ( -u 1 ^ N ) e. CC ) |
19 |
18
|
adantl |
|- ( ( X e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC ) |
20 |
|
negcl |
|- ( X e. CC -> -u X e. CC ) |
21 |
20
|
negcld |
|- ( X e. CC -> -u -u X e. CC ) |
22 |
|
fallfaccl |
|- ( ( -u -u X e. CC /\ N e. NN0 ) -> ( -u -u X FallFac N ) e. CC ) |
23 |
21 22
|
sylan |
|- ( ( X e. CC /\ N e. NN0 ) -> ( -u -u X FallFac N ) e. CC ) |
24 |
19 19 23
|
mulassd |
|- ( ( X e. CC /\ N e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( -u -u X FallFac N ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) ) |
25 |
|
fallfaccl |
|- ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) e. CC ) |
26 |
25
|
mulid2d |
|- ( ( X e. CC /\ N e. NN0 ) -> ( 1 x. ( X FallFac N ) ) = ( X FallFac N ) ) |
27 |
16 24 26
|
3eqtr3rd |
|- ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) ) |
28 |
|
risefallfac |
|- ( ( -u X e. CC /\ N e. NN0 ) -> ( -u X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) |
29 |
20 28
|
sylan |
|- ( ( X e. CC /\ N e. NN0 ) -> ( -u X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) |
30 |
29
|
oveq2d |
|- ( ( X e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u X RiseFac N ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) ) |
31 |
27 30
|
eqtr4d |
|- ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) = ( ( -u 1 ^ N ) x. ( -u X RiseFac N ) ) ) |