gamcvg

Description: The pointwise exponential of the series G converges to _G ( A ) x. A . (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Hypotheses	lgamcvg.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
	lgamcvg.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
Assertion	gamcvg	$⊢ φ \to (\exp \circ seq 1 (+ G)) ⇝ Γ (A) A$

Proof

Step	Hyp	Ref	Expression
1		lgamcvg.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
2		lgamcvg.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4		1zzd	$⊢ φ \to 1 \in ℤ$
5		efcn	$⊢ \exp : ℂ \underset{cn}{⟶} ℂ$
6	5	a1i	$⊢ φ \to \exp : ℂ \underset{cn}{⟶} ℂ$
7	2	eldifad	$⊢ φ \to A \in ℂ$
8	7	adantr	$⊢ (φ \land m \in ℕ) \to A \in ℂ$
9		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
10	9	peano2nnd	$⊢ (φ \land m \in ℕ) \to m + 1 \in ℕ$
11	10	nnrpd	$⊢ (φ \land m \in ℕ) \to m + 1 \in ℝ^{+}$
12	9	nnrpd	$⊢ (φ \land m \in ℕ) \to m \in ℝ^{+}$
13	11 12	rpdivcld	$⊢ (φ \land m \in ℕ) \to \frac{m + 1}{m} \in ℝ^{+}$
14	13	relogcld	$⊢ (φ \land m \in ℕ) \to \log (\frac{m + 1}{m}) \in ℝ$
15	14	recnd	$⊢ (φ \land m \in ℕ) \to \log (\frac{m + 1}{m}) \in ℂ$
16	8 15	mulcld	$⊢ (φ \land m \in ℕ) \to A \log (\frac{m + 1}{m}) \in ℂ$
17	9	nncnd	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
18	9	nnne0d	$⊢ (φ \land m \in ℕ) \to m \neq 0$
19	8 17 18	divcld	$⊢ (φ \land m \in ℕ) \to \frac{A}{m} \in ℂ$
20		1cnd	$⊢ (φ \land m \in ℕ) \to 1 \in ℂ$
21	19 20	addcld	$⊢ (φ \land m \in ℕ) \to (\frac{A}{m}) + 1 \in ℂ$
22	2	adantr	$⊢ (φ \land m \in ℕ) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
23	22 9	dmgmdivn0	$⊢ (φ \land m \in ℕ) \to (\frac{A}{m}) + 1 \neq 0$
24	21 23	logcld	$⊢ (φ \land m \in ℕ) \to \log ((\frac{A}{m}) + 1) \in ℂ$
25	16 24	subcld	$⊢ (φ \land m \in ℕ) \to A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1) \in ℂ$
26	25 1	fmptd	$⊢ φ \to G : ℕ ⟶ ℂ$
27	26	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to G (n) \in ℂ$
28	3 4 27	serf	$⊢ φ \to seq 1 (+ G) : ℕ ⟶ ℂ$
29	1 2	lgamcvg	$⊢ φ \to seq 1 (+ G) ⇝ (\log Γ (A) + \log A)$
30		lgamcl	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A) \in ℂ$
31	2 30	syl	$⊢ φ \to \log Γ (A) \in ℂ$
32	2	dmgmn0	$⊢ φ \to A \neq 0$
33	7 32	logcld	$⊢ φ \to \log A \in ℂ$
34	31 33	addcld	$⊢ φ \to \log Γ (A) + \log A \in ℂ$
35	3 4 6 28 29 34	climcncf	$⊢ φ \to (\exp \circ seq 1 (+ G)) ⇝ e^{\log Γ (A) + \log A}$
36		efadd	$⊢ (\log Γ (A) \in ℂ \land \log A \in ℂ) \to e^{\log Γ (A) + \log A} = e^{\log Γ (A)} e^{\log A}$
37	31 33 36	syl2anc	$⊢ φ \to e^{\log Γ (A) + \log A} = e^{\log Γ (A)} e^{\log A}$
38		eflgam	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A)} = Γ (A)$
39	2 38	syl	$⊢ φ \to e^{\log Γ (A)} = Γ (A)$
40		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
41	7 32 40	syl2anc	$⊢ φ \to e^{\log A} = A$
42	39 41	oveq12d	$⊢ φ \to e^{\log Γ (A)} e^{\log A} = Γ (A) A$
43	37 42	eqtrd	$⊢ φ \to e^{\log Γ (A) + \log A} = Γ (A) A$
44	35 43	breqtrd	$⊢ φ \to (\exp \circ seq 1 (+ G)) ⇝ Γ (A) A$

Metamath Proof Explorer

Theorem gamcvg

Proof