lgamgulmlem4

	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	lgamgulmlem4	$⊢ φ \to seq 1 (+ T) \in dom ⇝$

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		2nn	$⊢ 2 \in ℕ$
6	5	a1i	$⊢ φ \to 2 \in ℕ$
7	6 1	nnmulcld	$⊢ φ \to 2 R \in ℕ$
8	7	nnzd	$⊢ φ \to 2 R \in ℤ$
9		eluzle	$⊢ n \in ℤ_{\geq 2 R} \to 2 R \leq n$
10	9	adantl	$⊢ (φ \land n \in ℤ_{\geq 2 R}) \to 2 R \leq n$
11	10	iftrued	$⊢ (φ \land n \in ℤ_{\geq 2 R}) \to if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π) = R (\frac{2 (R + 1)}{n^{2}})$
12		eluznn	$⊢ (2 R \in ℕ \land n \in ℤ_{\geq 2 R}) \to n \in ℕ$
13	7 12	sylan	$⊢ (φ \land n \in ℤ_{\geq 2 R}) \to n \in ℕ$
14		breq2	$⊢ m = n \to (2 R \leq m \leftrightarrow 2 R \leq n)$
15		oveq1	$⊢ m = n \to m^{2} = n^{2}$
16	15	oveq2d	$⊢ m = n \to \frac{2 (R + 1)}{m^{2}} = \frac{2 (R + 1)}{n^{2}}$
17	16	oveq2d	$⊢ m = n \to R (\frac{2 (R + 1)}{m^{2}}) = R (\frac{2 (R + 1)}{n^{2}})$
18		oveq1	$⊢ m = n \to m + 1 = n + 1$
19		id	$⊢ m = n \to m = n$
20	18 19	oveq12d	$⊢ m = n \to \frac{m + 1}{m} = \frac{n + 1}{n}$
21	20	fveq2d	$⊢ m = n \to \log (\frac{m + 1}{m}) = \log (\frac{n + 1}{n})$
22	21	oveq2d	$⊢ m = n \to R \log (\frac{m + 1}{m}) = R \log (\frac{n + 1}{n})$
23		oveq2	$⊢ m = n \to (R + 1) m = (R + 1) n$
24	23	fveq2d	$⊢ m = n \to \log (R + 1) m = \log (R + 1) n$
25	24	oveq1d	$⊢ m = n \to \log (R + 1) m + π = \log (R + 1) n + π$
26	22 25	oveq12d	$⊢ m = n \to R \log (\frac{m + 1}{m}) + \log (R + 1) m + π = R \log (\frac{n + 1}{n}) + \log (R + 1) n + π$
27	14 17 26	ifbieq12d	$⊢ m = n \to if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
28		ovex	$⊢ R (\frac{2 (R + 1)}{n^{2}}) \in V$
29		ovex	$⊢ R \log (\frac{n + 1}{n}) + \log (R + 1) n + π \in V$
30	28 29	ifex	$⊢ if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π) \in V$
31	27 4 30	fvmpt	$⊢ n \in ℕ \to T (n) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
32	13 31	syl	$⊢ (φ \land n \in ℤ_{\geq 2 R}) \to T (n) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
33		eqid	$⊢ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) = (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))$
34	17 33 28	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) (n) = R (\frac{2 (R + 1)}{n^{2}})$
35	13 34	syl	$⊢ (φ \land n \in ℤ_{\geq 2 R}) \to (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) (n) = R (\frac{2 (R + 1)}{n^{2}})$
36	11 32 35	3eqtr4d	$⊢ (φ \land n \in ℤ_{\geq 2 R}) \to T (n) = (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) (n)$
37	8 36	seqfeq	$⊢ φ \to seq 2 R (+ T) = seq 2 R (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})))$
38		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
39		1zzd	$⊢ φ \to 1 \in ℤ$
40	1	nncnd	$⊢ φ \to R \in ℂ$
41		2cnd	$⊢ φ \to 2 \in ℂ$
42		1cnd	$⊢ φ \to 1 \in ℂ$
43	40 42	addcld	$⊢ φ \to R + 1 \in ℂ$
44	41 43	mulcld	$⊢ φ \to 2 (R + 1) \in ℂ$
45	40 44	mulcld	$⊢ φ \to R 2 (R + 1) \in ℂ$
46		1lt2	$⊢ 1 < 2$
47		2re	$⊢ 2 \in ℝ$
48		rere	$⊢ 2 \in ℝ \to ℜ (2) = 2$
49	47 48	ax-mp	$⊢ ℜ (2) = 2$
50	46 49	breqtrri	$⊢ 1 < ℜ (2)$
51	50	a1i	$⊢ φ \to 1 < ℜ (2)$
52		oveq1	$⊢ m = n \to m^{- 2} = n^{- 2}$
53		eqid	$⊢ (m \in ℕ ⟼ m^{- 2}) = (m \in ℕ ⟼ m^{- 2})$
54		ovex	$⊢ n^{- 2} \in V$
55	52 53 54	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ m^{- 2}) (n) = n^{- 2}$
56	55	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ m^{- 2}) (n) = n^{- 2}$
57	41 51 56	zetacvg	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ m^{- 2})) \in dom ⇝$
58		climdm	$⊢ seq 1 (+ (m \in ℕ ⟼ m^{- 2})) \in dom ⇝ \leftrightarrow seq 1 (+ (m \in ℕ ⟼ m^{- 2})) ⇝ ⇝ (seq 1 (+ (m \in ℕ ⟼ m^{- 2})))$
59	57 58	sylib	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ m^{- 2})) ⇝ ⇝ (seq 1 (+ (m \in ℕ ⟼ m^{- 2})))$
60		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
61	60	nncnd	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
62		2cnd	$⊢ (φ \land n \in ℕ) \to 2 \in ℂ$
63	62	negcld	$⊢ (φ \land n \in ℕ) \to - 2 \in ℂ$
64	61 63	cxpcld	$⊢ (φ \land n \in ℕ) \to n^{- 2} \in ℂ$
65	56 64	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ m^{- 2}) (n) \in ℂ$
66	40	adantr	$⊢ (φ \land n \in ℕ) \to R \in ℂ$
67		1cnd	$⊢ (φ \land n \in ℕ) \to 1 \in ℂ$
68	66 67	addcld	$⊢ (φ \land n \in ℕ) \to R + 1 \in ℂ$
69	62 68	mulcld	$⊢ (φ \land n \in ℕ) \to 2 (R + 1) \in ℂ$
70	66 69	mulcld	$⊢ (φ \land n \in ℕ) \to R 2 (R + 1) \in ℂ$
71	61	sqcld	$⊢ (φ \land n \in ℕ) \to n^{2} \in ℂ$
72	60	nnne0d	$⊢ (φ \land n \in ℕ) \to n \neq 0$
73		2z	$⊢ 2 \in ℤ$
74	73	a1i	$⊢ (φ \land n \in ℕ) \to 2 \in ℤ$
75	61 72 74	expne0d	$⊢ (φ \land n \in ℕ) \to n^{2} \neq 0$
76	70 71 75	divrecd	$⊢ (φ \land n \in ℕ) \to \frac{R 2 (R + 1)}{n^{2}} = R 2 (R + 1) (\frac{1}{n^{2}})$
77	66 69 71 75	divassd	$⊢ (φ \land n \in ℕ) \to \frac{R 2 (R + 1)}{n^{2}} = R (\frac{2 (R + 1)}{n^{2}})$
78	61 72 62	cxpnegd	$⊢ (φ \land n \in ℕ) \to n^{- 2} = \frac{1}{n^{2}}$
79	61 72 74	cxpexpzd	$⊢ (φ \land n \in ℕ) \to n^{2} = n^{2}$
80	79	oveq2d	$⊢ (φ \land n \in ℕ) \to \frac{1}{n^{2}} = \frac{1}{n^{2}}$
81	78 80	eqtr2d	$⊢ (φ \land n \in ℕ) \to \frac{1}{n^{2}} = n^{- 2}$
82	81	oveq2d	$⊢ (φ \land n \in ℕ) \to R 2 (R + 1) (\frac{1}{n^{2}}) = R 2 (R + 1) n^{- 2}$
83	76 77 82	3eqtr3d	$⊢ (φ \land n \in ℕ) \to R (\frac{2 (R + 1)}{n^{2}}) = R 2 (R + 1) n^{- 2}$
84	34	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) (n) = R (\frac{2 (R + 1)}{n^{2}})$
85	56	oveq2d	$⊢ (φ \land n \in ℕ) \to R 2 (R + 1) (m \in ℕ ⟼ m^{- 2}) (n) = R 2 (R + 1) n^{- 2}$
86	83 84 85	3eqtr4d	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) (n) = R 2 (R + 1) (m \in ℕ ⟼ m^{- 2}) (n)$
87	38 39 45 59 65 86	isermulc2	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) ⇝ R 2 (R + 1) ⇝ (seq 1 (+ (m \in ℕ ⟼ m^{- 2})))$
88		climrel	$⊢ Rel ⇝$
89	88	releldmi	$⊢ seq 1 (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) ⇝ R 2 (R + 1) ⇝ (seq 1 (+ (m \in ℕ ⟼ m^{- 2}))) \to seq 1 (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) \in dom ⇝$
90	87 89	syl	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) \in dom ⇝$
91	69 71 75	divcld	$⊢ (φ \land n \in ℕ) \to \frac{2 (R + 1)}{n^{2}} \in ℂ$
92	66 91	mulcld	$⊢ (φ \land n \in ℕ) \to R (\frac{2 (R + 1)}{n^{2}}) \in ℂ$
93	84 92	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}})) (n) \in ℂ$
94	38 7 93	iserex	$⊢ φ \to (seq 1 (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) \in dom ⇝ \leftrightarrow seq 2 R (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) \in dom ⇝)$
95	90 94	mpbid	$⊢ φ \to seq 2 R (+ (m \in ℕ ⟼ R (\frac{2 (R + 1)}{m^{2}}))) \in dom ⇝$
96	37 95	eqeltrd	$⊢ φ \to seq 2 R (+ T) \in dom ⇝$
97	31	adantl	$⊢ (φ \land n \in ℕ) \to T (n) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
98	1	adantr	$⊢ (φ \land n \in ℕ) \to R \in ℕ$
99	98	nnred	$⊢ (φ \land n \in ℕ) \to R \in ℝ$
100	47	a1i	$⊢ (φ \land n \in ℕ) \to 2 \in ℝ$
101		1red	$⊢ (φ \land n \in ℕ) \to 1 \in ℝ$
102	99 101	readdcld	$⊢ (φ \land n \in ℕ) \to R + 1 \in ℝ$
103	100 102	remulcld	$⊢ (φ \land n \in ℕ) \to 2 (R + 1) \in ℝ$
104	60	nnsqcld	$⊢ (φ \land n \in ℕ) \to n^{2} \in ℕ$
105	103 104	nndivred	$⊢ (φ \land n \in ℕ) \to \frac{2 (R + 1)}{n^{2}} \in ℝ$
106	99 105	remulcld	$⊢ (φ \land n \in ℕ) \to R (\frac{2 (R + 1)}{n^{2}}) \in ℝ$
107	60	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
108	107	nnrpd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℝ^{+}$
109	60	nnrpd	$⊢ (φ \land n \in ℕ) \to n \in ℝ^{+}$
110	108 109	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{n + 1}{n} \in ℝ^{+}$
111	110	relogcld	$⊢ (φ \land n \in ℕ) \to \log (\frac{n + 1}{n}) \in ℝ$
112	99 111	remulcld	$⊢ (φ \land n \in ℕ) \to R \log (\frac{n + 1}{n}) \in ℝ$
113	98	peano2nnd	$⊢ (φ \land n \in ℕ) \to R + 1 \in ℕ$
114	113	nnrpd	$⊢ (φ \land n \in ℕ) \to R + 1 \in ℝ^{+}$
115	114 109	rpmulcld	$⊢ (φ \land n \in ℕ) \to (R + 1) n \in ℝ^{+}$
116	115	relogcld	$⊢ (φ \land n \in ℕ) \to \log (R + 1) n \in ℝ$
117		pire	$⊢ π \in ℝ$
118	117	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
119	116 118	readdcld	$⊢ (φ \land n \in ℕ) \to \log (R + 1) n + π \in ℝ$
120	112 119	readdcld	$⊢ (φ \land n \in ℕ) \to R \log (\frac{n + 1}{n}) + \log (R + 1) n + π \in ℝ$
121	106 120	ifcld	$⊢ (φ \land n \in ℕ) \to if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π) \in ℝ$
122	97 121	eqeltrd	$⊢ (φ \land n \in ℕ) \to T (n) \in ℝ$
123	122	recnd	$⊢ (φ \land n \in ℕ) \to T (n) \in ℂ$
124	38 7 123	iserex	$⊢ φ \to (seq 1 (+ T) \in dom ⇝ \leftrightarrow seq 2 R (+ T) \in dom ⇝)$
125	96 124	mpbird	$⊢ φ \to seq 1 (+ T) \in dom ⇝$

Metamath Proof Explorer

Theorem lgamgulmlem4

Proof