Step |
Hyp |
Ref |
Expression |
1 |
|
elfz3nn0 |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 ) |
2 |
|
facp1 |
⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) ) |
3 |
1 2
|
syl |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) ) |
4 |
|
fznn0sub |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 ) |
5 |
|
facp1 |
⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) |
6 |
4 5
|
syl |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) |
7 |
1
|
nn0cnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℂ ) |
8 |
|
1cnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 1 ∈ ℂ ) |
9 |
|
elfznn0 |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 ) |
10 |
9
|
nn0cnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℂ ) |
11 |
7 8 10
|
addsubd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) = ( ( 𝑁 − 𝐾 ) + 1 ) ) |
12 |
11
|
fveq2d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ) |
13 |
11
|
oveq2d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) |
14 |
6 12 13
|
3eqtr4d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) |
15 |
14
|
oveq1d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) |
16 |
4
|
faccld |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ ) |
17 |
16
|
nncnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ ) |
18 |
|
nn0p1nn |
⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ ) |
19 |
4 18
|
syl |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ ) |
20 |
11 19
|
eqeltrd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℕ ) |
21 |
20
|
nncnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ ) |
22 |
9
|
faccld |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℕ ) |
23 |
22
|
nncnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℂ ) |
24 |
17 21 23
|
mul32d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) |
25 |
15 24
|
eqtrd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) |
26 |
3 25
|
oveq12d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) ) |
27 |
1
|
faccld |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℕ ) |
28 |
27
|
nncnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℂ ) |
29 |
|
nn0p1nn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ ) |
30 |
1 29
|
syl |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℕ ) |
31 |
30
|
nncnd |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℂ ) |
32 |
16 22
|
nnmulcld |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ ) |
33 |
|
nncn |
⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ) |
34 |
|
nnne0 |
⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) |
35 |
33 34
|
jca |
⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) ) |
36 |
32 35
|
syl |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) ) |
37 |
20
|
nnne0d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 ) |
38 |
21 37
|
jca |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 ) ) |
39 |
|
divmuldiv |
⊢ ( ( ( ( ! ‘ 𝑁 ) ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℂ ) ∧ ( ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) ∧ ( ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 ) ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) ) |
40 |
28 31 36 38 39
|
syl22anc |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) ) |
41 |
26 40
|
eqtr4d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) ) |
42 |
|
fzelp1 |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) |
43 |
|
bcval2 |
⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) |
44 |
42 43
|
syl |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) |
45 |
|
bcval2 |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) |
46 |
45
|
oveq1d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) ) |
47 |
41 44 46
|
3eqtr4d |
⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) ) |