Theorem iprodfac

Description: An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017)

	Ref	Expression
Assertion	iprodfac	⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ℕ ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
2		1zzd	⊢ ( 𝐴 ∈ ℕ0 → 1 ∈ ℤ )
3		facne0	⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) ≠ 0 )
4		eqid	⊢ ( 𝑥 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑥 ) ) ) )
5	4	faclim	⊢ ( 𝐴 ∈ ℕ0 → seq 1 ( · , ( 𝑥 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑥 ) ) ) ) ) ⇝ ( ! ‘ 𝐴 ) )
6		oveq2	⊢ ( 𝑥 = 𝑘 → ( 1 / 𝑥 ) = ( 1 / 𝑘 ) )
7	6	oveq2d	⊢ ( 𝑥 = 𝑘 → ( 1 + ( 1 / 𝑥 ) ) = ( 1 + ( 1 / 𝑘 ) ) )
8	7	oveq1d	⊢ ( 𝑥 = 𝑘 → ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) = ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) )
9		oveq2	⊢ ( 𝑥 = 𝑘 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 𝑘 ) )
10	9	oveq2d	⊢ ( 𝑥 = 𝑘 → ( 1 + ( 𝐴 / 𝑥 ) ) = ( 1 + ( 𝐴 / 𝑘 ) ) )
11	8 10	oveq12d	⊢ ( 𝑥 = 𝑘 → ( ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑥 ) ) ) = ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) )
12		ovex	⊢ ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) ∈ V
13	11 4 12	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑥 ) ) ) ) ‘ 𝑘 ) = ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑥 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑥 ) ) ) ) ‘ 𝑘 ) = ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) )
15		1rp	⊢ 1 ∈ ℝ+
16	15	a1i	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ+ )
17		simpr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
18	17	nnrpd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ+ )
19	18	rpreccld	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ+ )
20	16 19	rpaddcld	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 1 + ( 1 / 𝑘 ) ) ∈ ℝ+ )
21		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
22	21	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℤ )
23	20 22	rpexpcld	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) ∈ ℝ+ )
24		1cnd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
25		nn0nndivcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 / 𝑘 ) ∈ ℝ )
26	25	recnd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 / 𝑘 ) ∈ ℂ )
27	24 26	addcomd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 1 + ( 𝐴 / 𝑘 ) ) = ( ( 𝐴 / 𝑘 ) + 1 ) )
28		nn0ge0div	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐴 / 𝑘 ) )
29	25 28	ge0p1rpd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 / 𝑘 ) + 1 ) ∈ ℝ+ )
30	27 29	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 1 + ( 𝐴 / 𝑘 ) ) ∈ ℝ+ )
31	23 30	rpdivcld	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) ∈ ℝ+ )
32	31	rpcnd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) ∈ ℂ )
33	1 2 3 5 14 32	iprodn0	⊢ ( 𝐴 ∈ ℕ0 → ∏ 𝑘 ∈ ℕ ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) = ( ! ‘ 𝐴 ) )
34	33	eqcomd	⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ℕ ( ( ( 1 + ( 1 / 𝑘 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑘 ) ) ) )