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 𝑁 ) = ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴𝑁 ) ) ) )