Theorem fprodfac

Description: Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017)

	Ref	Expression
Assertion	fprodfac	⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
2		facnn	⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) = ( seq 1 ( · , I ) ‘ 𝐴 ) )
3		vex	⊢ 𝑘 ∈ V
4		fvi	⊢ ( 𝑘 ∈ V → ( I ‘ 𝑘 ) = 𝑘 )
5	3 4	mp1i	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( I ‘ 𝑘 ) = 𝑘 )
6		elnnuz	⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
7	6	biimpi	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
8		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℕ )
9	8	nncnd	⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℂ )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → 𝑘 ∈ ℂ )
11	5 7 10	fprodser	⊢ ( 𝐴 ∈ ℕ → ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 = ( seq 1 ( · , I ) ‘ 𝐴 ) )
12	2 11	eqtr4d	⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
13		prod0	⊢ ∏ 𝑘 ∈ ∅ 𝑘 = 1
14	13	eqcomi	⊢ 1 = ∏ 𝑘 ∈ ∅ 𝑘
15		fveq2	⊢ ( 𝐴 = 0 → ( ! ‘ 𝐴 ) = ( ! ‘ 0 ) )
16		fac0	⊢ ( ! ‘ 0 ) = 1
17	15 16	eqtrdi	⊢ ( 𝐴 = 0 → ( ! ‘ 𝐴 ) = 1 )
18		oveq2	⊢ ( 𝐴 = 0 → ( 1 ... 𝐴 ) = ( 1 ... 0 ) )
19		fz10	⊢ ( 1 ... 0 ) = ∅
20	18 19	eqtrdi	⊢ ( 𝐴 = 0 → ( 1 ... 𝐴 ) = ∅ )
21	20	prodeq1d	⊢ ( 𝐴 = 0 → ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 = ∏ 𝑘 ∈ ∅ 𝑘 )
22	14 17 21	3eqtr4a	⊢ ( 𝐴 = 0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
23	12 22	jaoi	⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
24	1 23	sylbi	⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )