iprodfac

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

		Ref	Expression
	Assertion	iprodfac	$⊢ A \in ℕ_{0} \to A! = \prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})$

Proof

Step	Hyp	Ref	Expression
1		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
2		1zzd	$⊢ A \in ℕ_{0} \to 1 \in ℤ$
3		facne0	$⊢ A \in ℕ_{0} \to A! \neq 0$
4		eqid	$⊢ (x \in ℕ ⟼ \frac{{(1 + (\frac{1}{x}))}^{A}}{1 + (\frac{A}{x})}) = (x \in ℕ ⟼ \frac{{(1 + (\frac{1}{x}))}^{A}}{1 + (\frac{A}{x})})$
5	4	faclim	$⊢ A \in ℕ_{0} \to seq 1 (\times (x \in ℕ ⟼ \frac{{(1 + (\frac{1}{x}))}^{A}}{1 + (\frac{A}{x})})) ⇝ A!$
6		oveq2	$⊢ x = k \to \frac{1}{x} = \frac{1}{k}$
7	6	oveq2d	$⊢ x = k \to 1 + (\frac{1}{x}) = 1 + (\frac{1}{k})$
8	7	oveq1d	$⊢ x = k \to {(1 + (\frac{1}{x}))}^{A} = {(1 + (\frac{1}{k}))}^{A}$
9		oveq2	$⊢ x = k \to \frac{A}{x} = \frac{A}{k}$
10	9	oveq2d	$⊢ x = k \to 1 + (\frac{A}{x}) = 1 + (\frac{A}{k})$
11	8 10	oveq12d	$⊢ x = k \to \frac{{(1 + (\frac{1}{x}))}^{A}}{1 + (\frac{A}{x})} = \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})}$
12		ovex	$⊢ \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})} \in V$
13	11 4 12	fvmpt	$⊢ k \in ℕ \to (x \in ℕ ⟼ \frac{{(1 + (\frac{1}{x}))}^{A}}{1 + (\frac{A}{x})}) (k) = \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})}$
14	13	adantl	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to (x \in ℕ ⟼ \frac{{(1 + (\frac{1}{x}))}^{A}}{1 + (\frac{A}{x})}) (k) = \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})}$
15		1rp	$⊢ 1 \in ℝ^{+}$
16	15	a1i	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to 1 \in ℝ^{+}$
17		simpr	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to k \in ℕ$
18	17	nnrpd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to k \in ℝ^{+}$
19	18	rpreccld	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to \frac{1}{k} \in ℝ^{+}$
20	16 19	rpaddcld	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to 1 + (\frac{1}{k}) \in ℝ^{+}$
21		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
22	21	adantr	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to A \in ℤ$
23	20 22	rpexpcld	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to {(1 + (\frac{1}{k}))}^{A} \in ℝ^{+}$
24		1cnd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to 1 \in ℂ$
25		nn0nndivcl	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to \frac{A}{k} \in ℝ$
26	25	recnd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to \frac{A}{k} \in ℂ$
27	24 26	addcomd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to 1 + (\frac{A}{k}) = (\frac{A}{k}) + 1$
28		nn0ge0div	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to 0 \leq \frac{A}{k}$
29	25 28	ge0p1rpd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to (\frac{A}{k}) + 1 \in ℝ^{+}$
30	27 29	eqeltrd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to 1 + (\frac{A}{k}) \in ℝ^{+}$
31	23 30	rpdivcld	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})} \in ℝ^{+}$
32	31	rpcnd	$⊢ (A \in ℕ_{0} \land k \in ℕ) \to \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})} \in ℂ$
33	1 2 3 5 14 32	iprodn0	$⊢ A \in ℕ_{0} \to \prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})}) = A!$
34	33	eqcomd	$⊢ A \in ℕ_{0} \to A! = \prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})$

Metamath Proof Explorer

Theorem iprodfac

Proof