Theorem 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	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
	lgamcvg.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
Assertion	gamcvg	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , 𝐺 ) ) ⇝ ( ( Γ ‘ 𝐴 ) · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		lgamcvg.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
2		lgamcvg.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
4		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
5		efcn	⊢ exp ∈ ( ℂ –cn→ ℂ )
6	5	a1i	⊢ ( 𝜑 → exp ∈ ( ℂ –cn→ ℂ ) )
7	2	eldifad	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ℂ )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
10	9	peano2nnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
11	10	nnrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℝ+ )
12	9	nnrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
13	11 12	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ+ )
14	13	relogcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℝ )
15	14	recnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℂ )
16	8 15	mulcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) ∈ ℂ )
17	9	nncnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
18	9	nnne0d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
19	8 17 18	divcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐴 / 𝑚 ) ∈ ℂ )
20		1cnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℂ )
21	19 20	addcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 / 𝑚 ) + 1 ) ∈ ℂ )
22	2	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
23	22 9	dmgmdivn0	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 / 𝑚 ) + 1 ) ≠ 0 )
24	21 23	logcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ∈ ℂ )
25	16 24	subcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ∈ ℂ )
26	25 1	fmptd	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ℂ )
27	26	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ )
28	3 4 27	serf	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℂ )
29	1 2	lgamcvg	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )
30		lgamcl	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 𝐴 ) ∈ ℂ )
31	2 30	syl	⊢ ( 𝜑 → ( log Γ ‘ 𝐴 ) ∈ ℂ )
32	2	dmgmn0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
33	7 32	logcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
34	31 33	addcld	⊢ ( 𝜑 → ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ∈ ℂ )
35	3 4 6 28 29 34	climcncf	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , 𝐺 ) ) ⇝ ( exp ‘ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) )
36		efadd	⊢ ( ( ( log Γ ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( log Γ ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐴 ) ) ) )
37	31 33 36	syl2anc	⊢ ( 𝜑 → ( exp ‘ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( log Γ ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐴 ) ) ) )
38		eflgam	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )
39	2 38	syl	⊢ ( 𝜑 → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )
40		eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
41	7 32 40	syl2anc	⊢ ( 𝜑 → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
42	39 41	oveq12d	⊢ ( 𝜑 → ( ( exp ‘ ( log Γ ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( ( Γ ‘ 𝐴 ) · 𝐴 ) )
43	37 42	eqtrd	⊢ ( 𝜑 → ( exp ‘ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) = ( ( Γ ‘ 𝐴 ) · 𝐴 ) )
44	35 43	breqtrd	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , 𝐺 ) ) ⇝ ( ( Γ ‘ 𝐴 ) · 𝐴 ) )