lgamgulmlem6

Description: The series G is uniformly convergent on the compact region U , which describes a circle of radius R with holes of size 1 / R around the poles of the gamma function. (Contributed by Mario Carneiro, 9-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)))$
	lgamgulm.t	$⊢ T = (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π))$
Assertion	lgamgulmlem6	$⊢ φ \to (seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U) \land (seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O) \to \exists r \in ℝ \forall z \in U \|O\| \leq r))$

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		lgamgulm.t	$⊢ T = (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π))$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		1zzd	$⊢ φ \to 1 \in ℤ$
7		cnex	$⊢ ℂ \in V$
8	2 7	rabex2	$⊢ U \in V$
9	8	a1i	$⊢ φ \to U \in V$
10	1 2	lgamgulmlem1	$⊢ φ \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
11	10	ad2antrr	$⊢ ((φ \land m \in ℕ) \land z \in U) \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
12		simpr	$⊢ ((φ \land m \in ℕ) \land z \in U) \to z \in U$
13	11 12	sseldd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to z \in (ℂ ∖ (ℤ ∖ ℕ))$
14	13	eldifad	$⊢ ((φ \land m \in ℕ) \land z \in U) \to z \in ℂ$
15		simplr	$⊢ ((φ \land m \in ℕ) \land z \in U) \to m \in ℕ$
16	15	peano2nnd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to m + 1 \in ℕ$
17	16	nnrpd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to m + 1 \in ℝ^{+}$
18	15	nnrpd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to m \in ℝ^{+}$
19	17 18	rpdivcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to \frac{m + 1}{m} \in ℝ^{+}$
20	19	relogcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to \log (\frac{m + 1}{m}) \in ℝ$
21	20	recnd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to \log (\frac{m + 1}{m}) \in ℂ$
22	14 21	mulcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to z \log (\frac{m + 1}{m}) \in ℂ$
23	15	nncnd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to m \in ℂ$
24	15	nnne0d	$⊢ ((φ \land m \in ℕ) \land z \in U) \to m \neq 0$
25	14 23 24	divcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to \frac{z}{m} \in ℂ$
26		1cnd	$⊢ ((φ \land m \in ℕ) \land z \in U) \to 1 \in ℂ$
27	25 26	addcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to (\frac{z}{m}) + 1 \in ℂ$
28	13 15	dmgmdivn0	$⊢ ((φ \land m \in ℕ) \land z \in U) \to (\frac{z}{m}) + 1 \neq 0$
29	27 28	logcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to \log ((\frac{z}{m}) + 1) \in ℂ$
30	22 29	subcld	$⊢ ((φ \land m \in ℕ) \land z \in U) \to z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1) \in ℂ$
31	30	fmpttd	$⊢ (φ \land m \in ℕ) \to (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) : U ⟶ ℂ$
32	7 8	elmap	$⊢ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) \in (ℂ^{U}) \leftrightarrow (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) : U ⟶ ℂ$
33	31 32	sylibr	$⊢ (φ \land m \in ℕ) \to (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) \in (ℂ^{U})$
34	33 3	fmptd	$⊢ φ \to G : ℕ ⟶ ℂ^{U}$
35		nnex	$⊢ ℕ \in V$
36	35	mptex	$⊢ (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π)) \in V$
37	4 36	eqeltri	$⊢ T \in V$
38	37	a1i	$⊢ φ \to T \in V$
39	1	adantr	$⊢ (φ \land m \in ℕ) \to R \in ℕ$
40	39	nnred	$⊢ (φ \land m \in ℕ) \to R \in ℝ$
41		2re	$⊢ 2 \in ℝ$
42	41	a1i	$⊢ (φ \land m \in ℕ) \to 2 \in ℝ$
43		1red	$⊢ (φ \land m \in ℕ) \to 1 \in ℝ$
44	40 43	readdcld	$⊢ (φ \land m \in ℕ) \to R + 1 \in ℝ$
45	42 44	remulcld	$⊢ (φ \land m \in ℕ) \to 2 (R + 1) \in ℝ$
46		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
47	46	nnsqcld	$⊢ (φ \land m \in ℕ) \to m^{2} \in ℕ$
48	45 47	nndivred	$⊢ (φ \land m \in ℕ) \to \frac{2 (R + 1)}{m^{2}} \in ℝ$
49	40 48	remulcld	$⊢ (φ \land m \in ℕ) \to R (\frac{2 (R + 1)}{m^{2}}) \in ℝ$
50	46	peano2nnd	$⊢ (φ \land m \in ℕ) \to m + 1 \in ℕ$
51	50	nnrpd	$⊢ (φ \land m \in ℕ) \to m + 1 \in ℝ^{+}$
52	46	nnrpd	$⊢ (φ \land m \in ℕ) \to m \in ℝ^{+}$
53	51 52	rpdivcld	$⊢ (φ \land m \in ℕ) \to \frac{m + 1}{m} \in ℝ^{+}$
54	53	relogcld	$⊢ (φ \land m \in ℕ) \to \log (\frac{m + 1}{m}) \in ℝ$
55	40 54	remulcld	$⊢ (φ \land m \in ℕ) \to R \log (\frac{m + 1}{m}) \in ℝ$
56	39	peano2nnd	$⊢ (φ \land m \in ℕ) \to R + 1 \in ℕ$
57	56	nnrpd	$⊢ (φ \land m \in ℕ) \to R + 1 \in ℝ^{+}$
58	57 52	rpmulcld	$⊢ (φ \land m \in ℕ) \to (R + 1) m \in ℝ^{+}$
59	58	relogcld	$⊢ (φ \land m \in ℕ) \to \log (R + 1) m \in ℝ$
60		pire	$⊢ π \in ℝ$
61	60	a1i	$⊢ (φ \land m \in ℕ) \to π \in ℝ$
62	59 61	readdcld	$⊢ (φ \land m \in ℕ) \to \log (R + 1) m + π \in ℝ$
63	55 62	readdcld	$⊢ (φ \land m \in ℕ) \to R \log (\frac{m + 1}{m}) + \log (R + 1) m + π \in ℝ$
64	49 63	ifcld	$⊢ (φ \land m \in ℕ) \to if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π) \in ℝ$
65	64 4	fmptd	$⊢ φ \to T : ℕ ⟶ ℝ$
66	65	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to T (n) \in ℝ$
67	1 2 3 4	lgamgulmlem5	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|G (n) (y)\| \leq T (n)$
68	1 2 3 4	lgamgulmlem4	$⊢ φ \to seq 1 (+ T) \in dom ⇝$
69	5 6 9 34 38 66 67 68	mtest	$⊢ φ \to seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U)$
70		1zzd	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to 1 \in ℤ$
71	8	a1i	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to U \in V$
72	34	adantr	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to G : ℕ ⟶ ℂ^{U}$
73	37	a1i	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to T \in V$
74	66	adantlr	$⊢ ((φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \land n \in ℕ) \to T (n) \in ℝ$
75	67	adantlr	$⊢ ((φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \land (n \in ℕ \land y \in U)) \to \|G (n) (y)\| \leq T (n)$
76	68	adantr	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to seq 1 (+ T) \in dom ⇝$
77		simpr	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)$
78	5 70 71 72 73 74 75 76 77	mtestbdd	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to \exists r \in ℝ \forall y \in U \|(z \in U ⟼ O) (y)\| \leq r$
79		nfcv	$⊢ \underline{Ⅎ} z abs$
80		nffvmpt1	$⊢ \underline{Ⅎ} z (z \in U ⟼ O) (y)$
81	79 80	nffv	$⊢ \underline{Ⅎ} z \|(z \in U ⟼ O) (y)\|$
82		nfcv	$⊢ \underline{Ⅎ} z \leq$
83		nfcv	$⊢ \underline{Ⅎ} z r$
84	81 82 83	nfbr	$⊢ Ⅎ z \|(z \in U ⟼ O) (y)\| \leq r$
85		nfv	$⊢ Ⅎ y \|(z \in U ⟼ O) (z)\| \leq r$
86		2fveq3	$⊢ y = z \to \|(z \in U ⟼ O) (y)\| = \|(z \in U ⟼ O) (z)\|$
87	86	breq1d	$⊢ y = z \to (\|(z \in U ⟼ O) (y)\| \leq r \leftrightarrow \|(z \in U ⟼ O) (z)\| \leq r)$
88	84 85 87	cbvralw	$⊢ \forall y \in U \|(z \in U ⟼ O) (y)\| \leq r \leftrightarrow \forall z \in U \|(z \in U ⟼ O) (z)\| \leq r$
89		ulmcl	$⊢ seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O) \to (z \in U ⟼ O) : U ⟶ ℂ$
90	89	adantl	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to (z \in U ⟼ O) : U ⟶ ℂ$
91		eqid	$⊢ (z \in U ⟼ O) = (z \in U ⟼ O)$
92	91	fmpt	$⊢ \forall z \in U O \in ℂ \leftrightarrow (z \in U ⟼ O) : U ⟶ ℂ$
93	90 92	sylibr	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to \forall z \in U O \in ℂ$
94	91	fvmpt2	$⊢ (z \in U \land O \in ℂ) \to (z \in U ⟼ O) (z) = O$
95	94	fveq2d	$⊢ (z \in U \land O \in ℂ) \to \|(z \in U ⟼ O) (z)\| = \|O\|$
96	95	breq1d	$⊢ (z \in U \land O \in ℂ) \to (\|(z \in U ⟼ O) (z)\| \leq r \leftrightarrow \|O\| \leq r)$
97	96	ralimiaa	$⊢ \forall z \in U O \in ℂ \to \forall z \in U (\|(z \in U ⟼ O) (z)\| \leq r \leftrightarrow \|O\| \leq r)$
98		ralbi	$⊢ \forall z \in U (\|(z \in U ⟼ O) (z)\| \leq r \leftrightarrow \|O\| \leq r) \to (\forall z \in U \|(z \in U ⟼ O) (z)\| \leq r \leftrightarrow \forall z \in U \|O\| \leq r)$
99	93 97 98	3syl	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to (\forall z \in U \|(z \in U ⟼ O) (z)\| \leq r \leftrightarrow \forall z \in U \|O\| \leq r)$
100	88 99	bitrid	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to (\forall y \in U \|(z \in U ⟼ O) (y)\| \leq r \leftrightarrow \forall z \in U \|O\| \leq r)$
101	100	rexbidv	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to (\exists r \in ℝ \forall y \in U \|(z \in U ⟼ O) (y)\| \leq r \leftrightarrow \exists r \in ℝ \forall z \in U \|O\| \leq r)$
102	78 101	mpbid	$⊢ (φ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O)) \to \exists r \in ℝ \forall z \in U \|O\| \leq r$
103	102	ex	$⊢ φ \to (seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O) \to \exists r \in ℝ \forall z \in U \|O\| \leq r)$
104	69 103	jca	$⊢ φ \to (seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U) \land (seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ O) \to \exists r \in ℝ \forall z \in U \|O\| \leq r))$

Metamath Proof Explorer

Theorem lgamgulmlem6

Proof