lgamgulm2

Description: Rewrite the limit of the sequence G in terms of the log-Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Hypotheses	lgamgulm.r	$⊢ φ \to R \in ℕ$
	lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
	lgamgulm.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
Assertion	lgamgulm2	$⊢ φ \to (\forall z \in U \log Γ (z) \in ℂ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z))$

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	$⊢ φ \to R \in ℕ$
2		lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
3		lgamgulm.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
4	1 2	lgamgulmlem1	$⊢ φ \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
5	4	sselda	$⊢ (φ \land z \in U) \to z \in (ℂ ∖ (ℤ ∖ ℕ))$
6		ovex	$⊢ \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z \in V$
7		df-lgam	$⊢ \log Γ = (z \in (ℂ ∖ (ℤ ∖ ℕ)) ⟼ \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z)$
8	7	fvmpt2	$⊢ (z \in (ℂ ∖ (ℤ ∖ ℕ)) \land \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z \in V) \to \log Γ (z) = \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z$
9	5 6 8	sylancl	$⊢ (φ \land z \in U) \to \log Γ (z) = \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z$
10		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
11		1zzd	$⊢ (φ \land z \in U) \to 1 \in ℤ$
12		oveq1	$⊢ m = n \to m + 1 = n + 1$
13		id	$⊢ m = n \to m = n$
14	12 13	oveq12d	$⊢ m = n \to \frac{m + 1}{m} = \frac{n + 1}{n}$
15	14	fveq2d	$⊢ m = n \to \log (\frac{m + 1}{m}) = \log (\frac{n + 1}{n})$
16	15	oveq2d	$⊢ m = n \to z \log (\frac{m + 1}{m}) = z \log (\frac{n + 1}{n})$
17		oveq2	$⊢ m = n \to \frac{z}{m} = \frac{z}{n}$
18	17	fvoveq1d	$⊢ m = n \to \log ((\frac{z}{m}) + 1) = \log ((\frac{z}{n}) + 1)$
19	16 18	oveq12d	$⊢ m = n \to z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1) = z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)$
20		eqid	$⊢ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) = (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))$
21		ovex	$⊢ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1) \in V$
22	19 20 21	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) (n) = z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)$
23	22	adantl	$⊢ ((φ \land z \in U) \land n \in ℕ) \to (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) (n) = z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)$
24	5	eldifad	$⊢ (φ \land z \in U) \to z \in ℂ$
25	24	adantr	$⊢ ((φ \land z \in U) \land n \in ℕ) \to z \in ℂ$
26		simpr	$⊢ ((φ \land z \in U) \land n \in ℕ) \to n \in ℕ$
27	26	peano2nnd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to n + 1 \in ℕ$
28	27	nnrpd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to n + 1 \in ℝ^{+}$
29	26	nnrpd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to n \in ℝ^{+}$
30	28 29	rpdivcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to \frac{n + 1}{n} \in ℝ^{+}$
31	30	relogcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to \log (\frac{n + 1}{n}) \in ℝ$
32	31	recnd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to \log (\frac{n + 1}{n}) \in ℂ$
33	25 32	mulcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to z \log (\frac{n + 1}{n}) \in ℂ$
34	26	nncnd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to n \in ℂ$
35	26	nnne0d	$⊢ ((φ \land z \in U) \land n \in ℕ) \to n \neq 0$
36	25 34 35	divcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to \frac{z}{n} \in ℂ$
37		1cnd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to 1 \in ℂ$
38	36 37	addcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to (\frac{z}{n}) + 1 \in ℂ$
39	5	adantr	$⊢ ((φ \land z \in U) \land n \in ℕ) \to z \in (ℂ ∖ (ℤ ∖ ℕ))$
40	39 26	dmgmdivn0	$⊢ ((φ \land z \in U) \land n \in ℕ) \to (\frac{z}{n}) + 1 \neq 0$
41	38 40	logcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to \log ((\frac{z}{n}) + 1) \in ℂ$
42	33 41	subcld	$⊢ ((φ \land z \in U) \land n \in ℕ) \to z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1) \in ℂ$
43		1z	$⊢ 1 \in ℤ$
44		seqfn	$⊢ 1 \in ℤ \to seq 1 (\circ_{f} +, G) Fn ℤ_{\geq 1}$
45	43 44	ax-mp	$⊢ seq 1 (\circ_{f} +, G) Fn ℤ_{\geq 1}$
46	10	fneq2i	$⊢ seq 1 (\circ_{f} +, G) Fn ℕ \leftrightarrow seq 1 (\circ_{f} +, G) Fn ℤ_{\geq 1}$
47	45 46	mpbir	$⊢ seq 1 (\circ_{f} +, G) Fn ℕ$
48	1 2 3	lgamgulm	$⊢ φ \to seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U)$
49		ulmdm	$⊢ seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U) \leftrightarrow seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G))$
50	48 49	sylib	$⊢ φ \to seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G))$
51		ulmf2	$⊢ (seq 1 (\circ_{f} +, G) Fn ℕ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G))) \to seq 1 (\circ_{f} +, G) : ℕ ⟶ ℂ^{U}$
52	47 50 51	sylancr	$⊢ φ \to seq 1 (\circ_{f} +, G) : ℕ ⟶ ℂ^{U}$
53	52	adantr	$⊢ (φ \land z \in U) \to seq 1 (\circ_{f} +, G) : ℕ ⟶ ℂ^{U}$
54		simpr	$⊢ (φ \land z \in U) \to z \in U$
55		seqex	$⊢ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) \in V$
56	55	a1i	$⊢ (φ \land z \in U) \to seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) \in V$
57	3	a1i	$⊢ ((φ \land z \in U) \land n \in ℕ) \to G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
58	57	seqeq3d	$⊢ ((φ \land z \in U) \land n \in ℕ) \to seq 1 (\circ_{f} +, G) = seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))))$
59	58	fveq1d	$⊢ ((φ \land z \in U) \land n \in ℕ) \to seq 1 (\circ_{f} +, G) (n) = seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) (n)$
60		cnex	$⊢ ℂ \in V$
61	2 60	rabex2	$⊢ U \in V$
62	61	a1i	$⊢ (φ \land n \in ℕ) \to U \in V$
63		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
64	63 10	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
65		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
66	65	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
67		ovexd	$⊢ ((φ \land n \in ℕ) \land (m \in ℕ \land z \in U)) \to z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1) \in V$
68	62 64 66 67	seqof2	$⊢ (φ \land n \in ℕ) \to seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) (n) = (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n))$
69	68	adantlr	$⊢ ((φ \land z \in U) \land n \in ℕ) \to seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) (n) = (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n))$
70	59 69	eqtrd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to seq 1 (\circ_{f} +, G) (n) = (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n))$
71	70	fveq1d	$⊢ ((φ \land z \in U) \land n \in ℕ) \to seq 1 (\circ_{f} +, G) (n) (z) = (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)) (z)$
72	54	adantr	$⊢ ((φ \land z \in U) \land n \in ℕ) \to z \in U$
73		fvex	$⊢ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n) \in V$
74		eqid	$⊢ (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)) = (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n))$
75	74	fvmpt2	$⊢ (z \in U \land seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n) \in V) \to (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)) (z) = seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)$
76	72 73 75	sylancl	$⊢ ((φ \land z \in U) \land n \in ℕ) \to (z \in U ⟼ seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)) (z) = seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)$
77	71 76	eqtrd	$⊢ ((φ \land z \in U) \land n \in ℕ) \to seq 1 (\circ_{f} +, G) (n) (z) = seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n)$
78	50	adantr	$⊢ (φ \land z \in U) \to seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G))$
79	10 11 53 54 56 77 78	ulmclm	$⊢ (φ \land z \in U) \to seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) ⇝ \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z)$
80	10 11 23 42 79	isumclim	$⊢ (φ \land z \in U) \to \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) = \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z)$
81		ulmcl	$⊢ seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) : U ⟶ ℂ$
82	50 81	syl	$⊢ φ \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) : U ⟶ ℂ$
83	82	ffvelcdmda	$⊢ (φ \land z \in U) \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z) \in ℂ$
84	80 83	eqeltrd	$⊢ (φ \land z \in U) \to \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) \in ℂ$
85	5	dmgmn0	$⊢ (φ \land z \in U) \to z \neq 0$
86	24 85	logcld	$⊢ (φ \land z \in U) \to \log z \in ℂ$
87	84 86	subcld	$⊢ (φ \land z \in U) \to \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z \in ℂ$
88	9 87	eqeltrd	$⊢ (φ \land z \in U) \to \log Γ (z) \in ℂ$
89	88	ralrimiva	$⊢ φ \to \forall z \in U \log Γ (z) \in ℂ$
90		ffn	$⊢ \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) : U ⟶ ℂ \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) Fn U$
91	50 81 90	3syl	$⊢ φ \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) Fn U$
92		nfcv	$⊢ \underline{Ⅎ} z \underset{u}{⇝} (U)$
93		nfcv	$⊢ \underline{Ⅎ} z 1$
94		nfcv	$⊢ \underline{Ⅎ} z \circ_{f} +$
95		nfcv	$⊢ \underline{Ⅎ} z ℕ$
96		nfmpt1	$⊢ \underline{Ⅎ} z (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))$
97	95 96	nfmpt	$⊢ \underline{Ⅎ} z (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
98	3 97	nfcxfr	$⊢ \underline{Ⅎ} z G$
99	93 94 98	nfseq	$⊢ \underline{Ⅎ} z seq 1 (\circ_{f} +, G)$
100	92 99	nffv	$⊢ \underline{Ⅎ} z \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G))$
101	100	dffn5f	$⊢ \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) Fn U \leftrightarrow \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) = (z \in U ⟼ \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z))$
102	91 101	sylib	$⊢ φ \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) = (z \in U ⟼ \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z))$
103	9	oveq1d	$⊢ (φ \land z \in U) \to \log Γ (z) + \log z = \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z + \log z$
104	84 86	npcand	$⊢ (φ \land z \in U) \to \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) - \log z + \log z = \sum_{n \in ℕ} (z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1))$
105	103 104 80	3eqtrrd	$⊢ (φ \land z \in U) \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z) = \log Γ (z) + \log z$
106	105	mpteq2dva	$⊢ φ \to (z \in U ⟼ \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) (z)) = (z \in U ⟼ \log Γ (z) + \log z)$
107	102 106	eqtrd	$⊢ φ \to \underset{u}{⇝} (U) (seq 1 (\circ_{f} +, G)) = (z \in U ⟼ \log Γ (z) + \log z)$
108	50 107	breqtrd	$⊢ φ \to seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z)$
109	89 108	jca	$⊢ φ \to (\forall z \in U \log Γ (z) \in ℂ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z))$

Metamath Proof Explorer

Theorem lgamgulm2

Proof