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

Metamath Proof Explorer

Theorem fallfacval4

Description: Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018)

Ref Expression
Assertion fallfacval4 ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 FallFac 𝑁 ) = ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) ∈ Fin )
2 elfzelz ⊢ ( 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) → 𝑘 ∈ ℤ )
3 2 zcnd ⊢ ( 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) → 𝑘 ∈ ℂ )
4 3 adantl ⊢ ( ( 𝑁 ∈ ( 0 ... 𝐴 ) ∧ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) ) → 𝑘 ∈ ℂ )
5 1 4 fprodcl ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ∏ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) 𝑘 ∈ ℂ )
6 fzfid ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 1 ... ( 𝐴 − 𝑁 ) ) ∈ Fin )
7 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) → 𝑘 ∈ ℕ )
8 7 adantl ⊢ ( ( 𝑁 ∈ ( 0 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) ) → 𝑘 ∈ ℕ )
9 8 nncnd ⊢ ( ( 𝑁 ∈ ( 0 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) ) → 𝑘 ∈ ℂ )
10 6 9 fprodcl ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ∈ ℂ )
11 8 nnne0d ⊢ ( ( 𝑁 ∈ ( 0 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) ) → 𝑘 ≠ 0 )
12 6 9 11 fprodn0 ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ≠ 0 )
13 5 10 12 divcan3d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 · ∏ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) 𝑘 ) / ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ) = ∏ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) 𝑘 )
14 fznn0sub ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 − 𝑁 ) ∈ ℕ0 )
15 14 nn0red ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 − 𝑁 ) ∈ ℝ )
16 15 ltp1d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 − 𝑁 ) < ( ( 𝐴 − 𝑁 ) + 1 ) )
17 fzdisj ⊢ ( ( 𝐴 − 𝑁 ) < ( ( 𝐴 − 𝑁 ) + 1 ) → ( ( 1 ... ( 𝐴 − 𝑁 ) ) ∩ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) ) = ∅ )
18 16 17 syl ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( 1 ... ( 𝐴 − 𝑁 ) ) ∩ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) ) = ∅ )
19 nn0p1nn ⊢ ( ( 𝐴 − 𝑁 ) ∈ ℕ0 → ( ( 𝐴 − 𝑁 ) + 1 ) ∈ ℕ )
20 14 19 syl ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( 𝐴 − 𝑁 ) + 1 ) ∈ ℕ )
21 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
22 20 21 eleqtrdi ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( 𝐴 − 𝑁 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
23 14 nn0zd ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 − 𝑁 ) ∈ ℤ )
24 elfzel2 ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝐴 ∈ ℤ )
25 elfzle1 ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 0 ≤ 𝑁 )
26 24 zred ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝐴 ∈ ℝ )
27 elfzelz ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝑁 ∈ ℤ )
28 27 zred ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝑁 ∈ ℝ )
29 26 28 subge02d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 0 ≤ 𝑁 ↔ ( 𝐴 − 𝑁 ) ≤ 𝐴 ) )
30 25 29 mpbid ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 − 𝑁 ) ≤ 𝐴 )
31 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ ( 𝐴 − 𝑁 ) ) ↔ ( ( 𝐴 − 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 − 𝑁 ) ≤ 𝐴 ) )
32 23 24 30 31 syl3anbrc ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝐴 ∈ ( ℤ≥ ‘ ( 𝐴 − 𝑁 ) ) )
33 fzsplit2 ⊢ ( ( ( ( 𝐴 − 𝑁 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐴 ∈ ( ℤ≥ ‘ ( 𝐴 − 𝑁 ) ) ) → ( 1 ... 𝐴 ) = ( ( 1 ... ( 𝐴 − 𝑁 ) ) ∪ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) ) )
34 22 32 33 syl2anc ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 1 ... 𝐴 ) = ( ( 1 ... ( 𝐴 − 𝑁 ) ) ∪ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) ) )
35 fzfid ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 1 ... 𝐴 ) ∈ Fin )
36 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℕ )
37 36 nncnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℂ )
38 37 adantl ⊢ ( ( 𝑁 ∈ ( 0 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → 𝑘 ∈ ℂ )
39 18 34 35 38 fprodsplit ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 = ( ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 · ∏ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) 𝑘 ) )
40 39 oveq1d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 / ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ) = ( ( ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 · ∏ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) 𝑘 ) / ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ) )
41 24 zcnd ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝐴 ∈ ℂ )
42 27 zcnd ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝑁 ∈ ℂ )
43 1cnd ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 1 ∈ ℂ )
44 41 42 43 subsubd ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 − ( 𝑁 − 1 ) ) = ( ( 𝐴 − 𝑁 ) + 1 ) )
45 44 oveq1d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( 𝐴 − ( 𝑁 − 1 ) ) ... 𝐴 ) = ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) )
46 45 prodeq1d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ∏ 𝑘 ∈ ( ( 𝐴 − ( 𝑁 − 1 ) ) ... 𝐴 ) 𝑘 = ∏ 𝑘 ∈ ( ( ( 𝐴 − 𝑁 ) + 1 ) ... 𝐴 ) 𝑘 )
47 13 40 46 3eqtr4rd ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ∏ 𝑘 ∈ ( ( 𝐴 − ( 𝑁 − 1 ) ) ... 𝐴 ) 𝑘 = ( ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 / ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ) )
48 fallfacval3 ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( ( 𝐴 − ( 𝑁 − 1 ) ) ... 𝐴 ) 𝑘 )
49 elfz3nn0 ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝐴 ∈ ℕ0 )
50 fprodfac ⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
51 49 50 syl ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
52 fprodfac ⊢ ( ( 𝐴 − 𝑁 ) ∈ ℕ0 → ( ! ‘ ( 𝐴 − 𝑁 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 )
53 14 52 syl ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ! ‘ ( 𝐴 − 𝑁 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 )
54 51 53 oveq12d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝑁 ) ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 / ∏ 𝑘 ∈ ( 1 ... ( 𝐴 − 𝑁 ) ) 𝑘 ) )
55 47 48 54 3eqtr4d ⊢ ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 FallFac 𝑁 ) = ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝑁 ) ) ) )