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