iprodgam

Description: An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018)

		Ref	Expression
	Hypothesis	iprodgam.1	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
	Assertion	iprodgam	$⊢ φ \to Γ (A) = \frac{\prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})}{A}$

Proof

Step	Hyp	Ref	Expression
1		iprodgam.1	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
2		eflgam	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A)} = Γ (A)$
3	1 2	syl	$⊢ φ \to e^{\log Γ (A)} = Γ (A)$
4		oveq1	$⊢ z = A \to z \log (\frac{k + 1}{k}) = A \log (\frac{k + 1}{k})$
5		oveq1	$⊢ z = A \to \frac{z}{k} = \frac{A}{k}$
6	5	fvoveq1d	$⊢ z = A \to \log ((\frac{z}{k}) + 1) = \log ((\frac{A}{k}) + 1)$
7	4 6	oveq12d	$⊢ z = A \to z \log (\frac{k + 1}{k}) - \log ((\frac{z}{k}) + 1) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
8	7	sumeq2sdv	$⊢ z = A \to \sum_{k \in ℕ} (z \log (\frac{k + 1}{k}) - \log ((\frac{z}{k}) + 1)) = \sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))$
9		fveq2	$⊢ z = A \to \log z = \log A$
10	8 9	oveq12d	$⊢ z = A \to \sum_{k \in ℕ} (z \log (\frac{k + 1}{k}) - \log ((\frac{z}{k}) + 1)) - \log z = \sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A$
11		df-lgam	$⊢ \log Γ = (z \in (ℂ ∖ (ℤ ∖ ℕ)) ⟼ \sum_{k \in ℕ} (z \log (\frac{k + 1}{k}) - \log ((\frac{z}{k}) + 1)) - \log z)$
12		ovex	$⊢ \sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A \in V$
13	10 11 12	fvmpt	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A) = \sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A$
14	1 13	syl	$⊢ φ \to \log Γ (A) = \sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A$
15	14	fveq2d	$⊢ φ \to e^{\log Γ (A)} = e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A}$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17		1zzd	$⊢ φ \to 1 \in ℤ$
18		oveq1	$⊢ j = k \to j + 1 = k + 1$
19		id	$⊢ j = k \to j = k$
20	18 19	oveq12d	$⊢ j = k \to \frac{j + 1}{j} = \frac{k + 1}{k}$
21	20	fveq2d	$⊢ j = k \to \log (\frac{j + 1}{j}) = \log (\frac{k + 1}{k})$
22	21	oveq2d	$⊢ j = k \to A \log (\frac{j + 1}{j}) = A \log (\frac{k + 1}{k})$
23		oveq2	$⊢ j = k \to \frac{A}{j} = \frac{A}{k}$
24	23	fvoveq1d	$⊢ j = k \to \log ((\frac{A}{j}) + 1) = \log ((\frac{A}{k}) + 1)$
25	22 24	oveq12d	$⊢ j = k \to A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
26		eqid	$⊢ (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1)) = (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1))$
27		ovex	$⊢ A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1) \in V$
28	25 26 27	fvmpt	$⊢ k \in ℕ \to (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1)) (k) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
29	28	adantl	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1)) (k) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
30	1	eldifad	$⊢ φ \to A \in ℂ$
31	30	adantr	$⊢ (φ \land k \in ℕ) \to A \in ℂ$
32		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
33	32	adantl	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ$
34	33	nncnd	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℂ$
35		nncn	$⊢ k \in ℕ \to k \in ℂ$
36	35	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℂ$
37		nnne0	$⊢ k \in ℕ \to k \neq 0$
38	37	adantl	$⊢ (φ \land k \in ℕ) \to k \neq 0$
39	34 36 38	divcld	$⊢ (φ \land k \in ℕ) \to \frac{k + 1}{k} \in ℂ$
40	33	nnne0d	$⊢ (φ \land k \in ℕ) \to k + 1 \neq 0$
41	34 36 40 38	divne0d	$⊢ (φ \land k \in ℕ) \to \frac{k + 1}{k} \neq 0$
42	39 41	logcld	$⊢ (φ \land k \in ℕ) \to \log (\frac{k + 1}{k}) \in ℂ$
43	31 42	mulcld	$⊢ (φ \land k \in ℕ) \to A \log (\frac{k + 1}{k}) \in ℂ$
44	31 36 38	divcld	$⊢ (φ \land k \in ℕ) \to \frac{A}{k} \in ℂ$
45		1cnd	$⊢ (φ \land k \in ℕ) \to 1 \in ℂ$
46	44 45	addcld	$⊢ (φ \land k \in ℕ) \to (\frac{A}{k}) + 1 \in ℂ$
47	1	adantr	$⊢ (φ \land k \in ℕ) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
48		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
49	47 48	dmgmdivn0	$⊢ (φ \land k \in ℕ) \to (\frac{A}{k}) + 1 \neq 0$
50	46 49	logcld	$⊢ (φ \land k \in ℕ) \to \log ((\frac{A}{k}) + 1) \in ℂ$
51	43 50	subcld	$⊢ (φ \land k \in ℕ) \to A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1) \in ℂ$
52	26 1	lgamcvg	$⊢ φ \to seq 1 (+ (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1))) ⇝ (\log Γ (A) + \log A)$
53		seqex	$⊢ seq 1 (+ (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1))) \in V$
54		ovex	$⊢ \log Γ (A) + \log A \in V$
55	53 54	breldm	$⊢ seq 1 (+ (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1))) ⇝ (\log Γ (A) + \log A) \to seq 1 (+ (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1))) \in dom ⇝$
56	52 55	syl	$⊢ φ \to seq 1 (+ (j \in ℕ ⟼ A \log (\frac{j + 1}{j}) - \log ((\frac{A}{j}) + 1))) \in dom ⇝$
57	16 17 29 51 56	isumcl	$⊢ φ \to \sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) \in ℂ$
58	1	dmgmn0	$⊢ φ \to A \neq 0$
59	30 58	logcld	$⊢ φ \to \log A \in ℂ$
60		efsub	$⊢ (\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) \in ℂ \land \log A \in ℂ) \to e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A} = \frac{e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))}}{e^{\log A}}$
61	57 59 60	syl2anc	$⊢ φ \to e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A} = \frac{e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))}}{e^{\log A}}$
62	16 17 29 51 56	iprodefisum	$⊢ φ \to \prod_{k \in ℕ} e^{A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)} = e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))}$
63		efsub	$⊢ (A \log (\frac{k + 1}{k}) \in ℂ \land \log ((\frac{A}{k}) + 1) \in ℂ) \to e^{A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)} = \frac{e^{A \log (\frac{k + 1}{k})}}{e^{\log ((\frac{A}{k}) + 1)}}$
64	43 50 63	syl2anc	$⊢ (φ \land k \in ℕ) \to e^{A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)} = \frac{e^{A \log (\frac{k + 1}{k})}}{e^{\log ((\frac{A}{k}) + 1)}}$
65	36 45 36 38	divdird	$⊢ (φ \land k \in ℕ) \to \frac{k + 1}{k} = (\frac{k}{k}) + (\frac{1}{k})$
66	36 38	dividd	$⊢ (φ \land k \in ℕ) \to \frac{k}{k} = 1$
67	66	oveq1d	$⊢ (φ \land k \in ℕ) \to (\frac{k}{k}) + (\frac{1}{k}) = 1 + (\frac{1}{k})$
68	65 67	eqtrd	$⊢ (φ \land k \in ℕ) \to \frac{k + 1}{k} = 1 + (\frac{1}{k})$
69	68	fveq2d	$⊢ (φ \land k \in ℕ) \to \log (\frac{k + 1}{k}) = \log (1 + (\frac{1}{k}))$
70	69	oveq2d	$⊢ (φ \land k \in ℕ) \to A \log (\frac{k + 1}{k}) = A \log (1 + (\frac{1}{k}))$
71	70	fveq2d	$⊢ (φ \land k \in ℕ) \to e^{A \log (\frac{k + 1}{k})} = e^{A \log (1 + (\frac{1}{k}))}$
72		1rp	$⊢ 1 \in ℝ^{+}$
73	72	a1i	$⊢ (φ \land k \in ℕ) \to 1 \in ℝ^{+}$
74	48	nnrpd	$⊢ (φ \land k \in ℕ) \to k \in ℝ^{+}$
75	74	rpreccld	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℝ^{+}$
76	73 75	rpaddcld	$⊢ (φ \land k \in ℕ) \to 1 + (\frac{1}{k}) \in ℝ^{+}$
77	76	rpcnd	$⊢ (φ \land k \in ℕ) \to 1 + (\frac{1}{k}) \in ℂ$
78	76	rpne0d	$⊢ (φ \land k \in ℕ) \to 1 + (\frac{1}{k}) \neq 0$
79	77 78 31	cxpefd	$⊢ (φ \land k \in ℕ) \to {(1 + (\frac{1}{k}))}^{A} = e^{A \log (1 + (\frac{1}{k}))}$
80	71 79	eqtr4d	$⊢ (φ \land k \in ℕ) \to e^{A \log (\frac{k + 1}{k})} = {(1 + (\frac{1}{k}))}^{A}$
81		eflog	$⊢ ((\frac{A}{k}) + 1 \in ℂ \land (\frac{A}{k}) + 1 \neq 0) \to e^{\log ((\frac{A}{k}) + 1)} = (\frac{A}{k}) + 1$
82	46 49 81	syl2anc	$⊢ (φ \land k \in ℕ) \to e^{\log ((\frac{A}{k}) + 1)} = (\frac{A}{k}) + 1$
83	44 45	addcomd	$⊢ (φ \land k \in ℕ) \to (\frac{A}{k}) + 1 = 1 + (\frac{A}{k})$
84	82 83	eqtrd	$⊢ (φ \land k \in ℕ) \to e^{\log ((\frac{A}{k}) + 1)} = 1 + (\frac{A}{k})$
85	80 84	oveq12d	$⊢ (φ \land k \in ℕ) \to \frac{e^{A \log (\frac{k + 1}{k})}}{e^{\log ((\frac{A}{k}) + 1)}} = \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})}$
86	64 85	eqtrd	$⊢ (φ \land k \in ℕ) \to e^{A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)} = \frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})}$
87	86	prodeq2dv	$⊢ φ \to \prod_{k \in ℕ} e^{A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)} = \prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})$
88	62 87	eqtr3d	$⊢ φ \to e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))} = \prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})$
89		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
90	30 58 89	syl2anc	$⊢ φ \to e^{\log A} = A$
91	88 90	oveq12d	$⊢ φ \to \frac{e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))}}{e^{\log A}} = \frac{\prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})}{A}$
92	61 91	eqtrd	$⊢ φ \to e^{\sum_{k \in ℕ} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) - \log A} = \frac{\prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})}{A}$
93	15 92	eqtrd	$⊢ φ \to e^{\log Γ (A)} = \frac{\prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})}{A}$
94	3 93	eqtr3d	$⊢ φ \to Γ (A) = \frac{\prod_{k \in ℕ} (\frac{{(1 + (\frac{1}{k}))}^{A}}{1 + (\frac{A}{k})})}{A}$

Metamath Proof Explorer

Theorem iprodgam

Proof