lgamcvglem

	Ref	Expression
Hypotheses	lgamucov.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|x + k\|)\}$
	lgamucov.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
	lgamcvglem.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
Assertion	lgamcvglem	$⊢ φ \to (\log Γ (A) \in ℂ \land seq 1 (+ G) ⇝ (\log Γ (A) + \log A))$

Proof

Step	Hyp	Ref	Expression
1		lgamucov.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|x + k\|)\}$
2		lgamucov.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
3		lgamcvglem.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
4	1 2	lgamucov2	$⊢ φ \to \exists r \in ℕ A \in U$
5		fveq2	$⊢ z = A \to \log Γ (z) = \log Γ (A)$
6	5	eleq1d	$⊢ z = A \to (\log Γ (z) \in ℂ \leftrightarrow \log Γ (A) \in ℂ)$
7		simprl	$⊢ (φ \land (r \in ℕ \land A \in U)) \to r \in ℕ$
8		fveq2	$⊢ x = t \to \|x\| = \|t\|$
9	8	breq1d	$⊢ x = t \to (\|x\| \leq r \leftrightarrow \|t\| \leq r)$
10		fvoveq1	$⊢ x = t \to \|x + k\| = \|t + k\|$
11	10	breq2d	$⊢ x = t \to (\frac{1}{r} \leq \|x + k\| \leftrightarrow \frac{1}{r} \leq \|t + k\|)$
12	11	ralbidv	$⊢ x = t \to (\forall k \in ℕ_{0} \frac{1}{r} \leq \|x + k\| \leftrightarrow \forall k \in ℕ_{0} \frac{1}{r} \leq \|t + k\|)$
13	9 12	anbi12d	$⊢ x = t \to ((\|x\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|x + k\|) \leftrightarrow (\|t\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|t + k\|))$
14	13	cbvrabv	$⊢ \{x \in ℂ \| (\|x\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|x + k\|)\} = \{t \in ℂ \| (\|t\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|t + k\|)\}$
15	1 14	eqtri	$⊢ U = \{t \in ℂ \| (\|t\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|t + k\|)\}$
16		eqid	$⊢ (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
17	7 15 16	lgamgulm2	$⊢ (φ \land (r \in ℕ \land A \in U)) \to (\forall z \in U \log Γ (z) \in ℂ \land seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z))$
18	17	simpld	$⊢ (φ \land (r \in ℕ \land A \in U)) \to \forall z \in U \log Γ (z) \in ℂ$
19		simprr	$⊢ (φ \land (r \in ℕ \land A \in U)) \to A \in U$
20	6 18 19	rspcdva	$⊢ (φ \land (r \in ℕ \land A \in U)) \to \log Γ (A) \in ℂ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22		1zzd	$⊢ (φ \land (r \in ℕ \land A \in U)) \to 1 \in ℤ$
23		1z	$⊢ 1 \in ℤ$
24		seqfn	$⊢ 1 \in ℤ \to seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) Fn ℤ_{\geq 1}$
25	23 24	ax-mp	$⊢ seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) Fn ℤ_{\geq 1}$
26	21	fneq2i	$⊢ seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) Fn ℕ \leftrightarrow seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) Fn ℤ_{\geq 1}$
27	25 26	mpbir	$⊢ seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) Fn ℕ$
28	17	simprd	$⊢ (φ \land (r \in ℕ \land A \in U)) \to seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z)$
29		ulmf2	$⊢ (seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) Fn ℕ \land seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z)) \to seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) : ℕ ⟶ ℂ^{U}$
30	27 28 29	sylancr	$⊢ (φ \land (r \in ℕ \land A \in U)) \to seq 1 (\circ_{f} +, (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))) : ℕ ⟶ ℂ^{U}$
31		seqex	$⊢ seq 1 (+ G) \in V$
32	31	a1i	$⊢ (φ \land (r \in ℕ \land A \in U)) \to seq 1 (+ G) \in V$
33		cnex	$⊢ ℂ \in V$
34	1 33	rabex2	$⊢ U \in V$
35	34	a1i	$⊢ ((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \to U \in V$
36		simpr	$⊢ ((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \to n \in ℕ$
37	36 21	eleqtrdi	$⊢ ((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \to n \in ℤ_{\geq 1}$
38		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
39	38	a1i	$⊢ ((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
40		ovexd	$⊢ (((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land (m \in ℕ \land z \in U)) \to z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1) \in V$
41	35 37 39 40	seqof2	$⊢ ((φ \land (r \in ℕ \land A \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))$
42		simplr	$⊢ ((((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \land m \in ℕ) \to z = A$
43	42	oveq1d	$⊢ ((((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \land m \in ℕ) \to z \log (\frac{m + 1}{m}) = A \log (\frac{m + 1}{m})$
44	42	oveq1d	$⊢ ((((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \land m \in ℕ) \to \frac{z}{m} = \frac{A}{m}$
45	44	fvoveq1d	$⊢ ((((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \land m \in ℕ) \to \log ((\frac{z}{m}) + 1) = \log ((\frac{A}{m}) + 1)$
46	43 45	oveq12d	$⊢ ((((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \land m \in ℕ) \to z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1) = A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1)$
47	46	mpteq2dva	$⊢ (((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \to (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
48	47 3	eqtr4di	$⊢ (((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \to (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) = G$
49	48	seqeq3d	$⊢ (((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \to seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) = seq 1 (+ G)$
50	49	fveq1d	$⊢ (((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \land z = A) \to seq 1 (+ (m \in ℕ ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1))) (n) = seq 1 (+ G) (n)$
51		simplrr	$⊢ ((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \to A \in U$
52		fvexd	$⊢ ((φ \land (r \in ℕ \land A \in U)) \land n \in ℕ) \to seq 1 (+ G) (n) \in V$
53	41 50 51 52	fvmptd	$⊢ ((φ \land (r \in ℕ \land A \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) (A) = seq 1 (+ G) (n)$
54	21 22 30 19 32 53 28	ulmclm	$⊢ (φ \land (r \in ℕ \land A \in U)) \to seq 1 (+ G) ⇝ (z \in U ⟼ \log Γ (z) + \log z) (A)$
55		fveq2	$⊢ z = A \to \log z = \log A$
56	5 55	oveq12d	$⊢ z = A \to \log Γ (z) + \log z = \log Γ (A) + \log A$
57		eqid	$⊢ (z \in U ⟼ \log Γ (z) + \log z) = (z \in U ⟼ \log Γ (z) + \log z)$
58		ovex	$⊢ \log Γ (A) + \log A \in V$
59	56 57 58	fvmpt	$⊢ A \in U \to (z \in U ⟼ \log Γ (z) + \log z) (A) = \log Γ (A) + \log A$
60	19 59	syl	$⊢ (φ \land (r \in ℕ \land A \in U)) \to (z \in U ⟼ \log Γ (z) + \log z) (A) = \log Γ (A) + \log A$
61	54 60	breqtrd	$⊢ (φ \land (r \in ℕ \land A \in U)) \to seq 1 (+ G) ⇝ (\log Γ (A) + \log A)$
62	20 61	jca	$⊢ (φ \land (r \in ℕ \land A \in U)) \to (\log Γ (A) \in ℂ \land seq 1 (+ G) ⇝ (\log Γ (A) + \log A))$
63	4 62	rexlimddv	$⊢ φ \to (\log Γ (A) \in ℂ \land seq 1 (+ G) ⇝ (\log Γ (A) + \log A))$

Metamath Proof Explorer

Theorem lgamcvglem

Proof