zetacvg

Description: The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014)

	Ref	Expression
Hypotheses	zetacvg.1	$⊢ φ \to S \in ℂ$
	zetacvg.2	$⊢ φ \to 1 < ℜ (S)$
	zetacvg.3	$⊢ (φ \land k \in ℕ) \to F (k) = k^{- S}$
Assertion	zetacvg	$⊢ φ \to seq 1 (+ F) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		zetacvg.1	$⊢ φ \to S \in ℂ$
2		zetacvg.2	$⊢ φ \to 1 < ℜ (S)$
3		zetacvg.3	$⊢ (φ \land k \in ℕ) \to F (k) = k^{- S}$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ φ \to 1 \in ℤ$
6		oveq1	$⊢ n = k \to n^{- ℜ (S)} = k^{- ℜ (S)}$
7		eqid	$⊢ (n \in ℕ ⟼ n^{- ℜ (S)}) = (n \in ℕ ⟼ n^{- ℜ (S)})$
8		ovex	$⊢ k^{- ℜ (S)} \in V$
9	6 7 8	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k) = k^{- ℜ (S)}$
10	9	adantl	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k) = k^{- ℜ (S)}$
11		nncn	$⊢ k \in ℕ \to k \in ℂ$
12	11	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℂ$
13		nnne0	$⊢ k \in ℕ \to k \neq 0$
14	13	adantl	$⊢ (φ \land k \in ℕ) \to k \neq 0$
15	1	negcld	$⊢ φ \to - S \in ℂ$
16	15	adantr	$⊢ (φ \land k \in ℕ) \to - S \in ℂ$
17	12 14 16	cxpefd	$⊢ (φ \land k \in ℕ) \to k^{- S} = e^{(- S) \log k}$
18	3 17	eqtrd	$⊢ (φ \land k \in ℕ) \to F (k) = e^{(- S) \log k}$
19	18	fveq2d	$⊢ (φ \land k \in ℕ) \to \|F (k)\| = \|e^{(- S) \log k}\|$
20		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
21	20	relogcld	$⊢ k \in ℕ \to \log k \in ℝ$
22	21	recnd	$⊢ k \in ℕ \to \log k \in ℂ$
23		mulcl	$⊢ (- S \in ℂ \land \log k \in ℂ) \to (- S) \log k \in ℂ$
24	15 22 23	syl2an	$⊢ (φ \land k \in ℕ) \to (- S) \log k \in ℂ$
25		absef	$⊢ (- S) \log k \in ℂ \to \|e^{(- S) \log k}\| = e^{ℜ ((- S) \log k)}$
26	24 25	syl	$⊢ (φ \land k \in ℕ) \to \|e^{(- S) \log k}\| = e^{ℜ ((- S) \log k)}$
27		remul	$⊢ (- S \in ℂ \land \log k \in ℂ) \to ℜ ((- S) \log k) = ℜ (- S) ℜ (\log k) - ℑ (- S) ℑ (\log k)$
28	15 22 27	syl2an	$⊢ (φ \land k \in ℕ) \to ℜ ((- S) \log k) = ℜ (- S) ℜ (\log k) - ℑ (- S) ℑ (\log k)$
29	1	renegd	$⊢ φ \to ℜ (- S) = - ℜ (S)$
30	21	rered	$⊢ k \in ℕ \to ℜ (\log k) = \log k$
31	29 30	oveqan12d	$⊢ (φ \land k \in ℕ) \to ℜ (- S) ℜ (\log k) = (- ℜ (S)) \log k$
32	21	reim0d	$⊢ k \in ℕ \to ℑ (\log k) = 0$
33	32	oveq2d	$⊢ k \in ℕ \to ℑ (- S) ℑ (\log k) = ℑ (- S) \cdot 0$
34		imcl	$⊢ - S \in ℂ \to ℑ (- S) \in ℝ$
35	34	recnd	$⊢ - S \in ℂ \to ℑ (- S) \in ℂ$
36	15 35	syl	$⊢ φ \to ℑ (- S) \in ℂ$
37	36	mul01d	$⊢ φ \to ℑ (- S) \cdot 0 = 0$
38	33 37	sylan9eqr	$⊢ (φ \land k \in ℕ) \to ℑ (- S) ℑ (\log k) = 0$
39	31 38	oveq12d	$⊢ (φ \land k \in ℕ) \to ℜ (- S) ℜ (\log k) - ℑ (- S) ℑ (\log k) = (- ℜ (S)) \log k - 0$
40	1	recld	$⊢ φ \to ℜ (S) \in ℝ$
41	40	renegcld	$⊢ φ \to - ℜ (S) \in ℝ$
42	41	recnd	$⊢ φ \to - ℜ (S) \in ℂ$
43		mulcl	$⊢ (- ℜ (S) \in ℂ \land \log k \in ℂ) \to (- ℜ (S)) \log k \in ℂ$
44	42 22 43	syl2an	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log k \in ℂ$
45	44	subid1d	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log k - 0 = (- ℜ (S)) \log k$
46	28 39 45	3eqtrd	$⊢ (φ \land k \in ℕ) \to ℜ ((- S) \log k) = (- ℜ (S)) \log k$
47	46	fveq2d	$⊢ (φ \land k \in ℕ) \to e^{ℜ ((- S) \log k)} = e^{(- ℜ (S)) \log k}$
48	42	adantr	$⊢ (φ \land k \in ℕ) \to - ℜ (S) \in ℂ$
49	12 14 48	cxpefd	$⊢ (φ \land k \in ℕ) \to k^{- ℜ (S)} = e^{(- ℜ (S)) \log k}$
50	47 49	eqtr4d	$⊢ (φ \land k \in ℕ) \to e^{ℜ ((- S) \log k)} = k^{- ℜ (S)}$
51	19 26 50	3eqtrd	$⊢ (φ \land k \in ℕ) \to \|F (k)\| = k^{- ℜ (S)}$
52	10 51	eqtr4d	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k) = \|F (k)\|$
53	12 16	cxpcld	$⊢ (φ \land k \in ℕ) \to k^{- S} \in ℂ$
54	3 53	eqeltrd	$⊢ (φ \land k \in ℕ) \to F (k) \in ℂ$
55		2rp	$⊢ 2 \in ℝ^{+}$
56		1re	$⊢ 1 \in ℝ$
57		resubcl	$⊢ (1 \in ℝ \land ℜ (S) \in ℝ) \to 1 - ℜ (S) \in ℝ$
58	56 40 57	sylancr	$⊢ φ \to 1 - ℜ (S) \in ℝ$
59		rpcxpcl	$⊢ (2 \in ℝ^{+} \land 1 - ℜ (S) \in ℝ) \to 2^{1 - ℜ (S)} \in ℝ^{+}$
60	55 58 59	sylancr	$⊢ φ \to 2^{1 - ℜ (S)} \in ℝ^{+}$
61	60	rpcnd	$⊢ φ \to 2^{1 - ℜ (S)} \in ℂ$
62		recl	$⊢ S \in ℂ \to ℜ (S) \in ℝ$
63	62	recnd	$⊢ S \in ℂ \to ℜ (S) \in ℂ$
64	1 63	syl	$⊢ φ \to ℜ (S) \in ℂ$
65	64	addid2d	$⊢ φ \to 0 + ℜ (S) = ℜ (S)$
66	2 65	breqtrrd	$⊢ φ \to 1 < 0 + ℜ (S)$
67		0re	$⊢ 0 \in ℝ$
68		ltsubadd	$⊢ (1 \in ℝ \land ℜ (S) \in ℝ \land 0 \in ℝ) \to (1 - ℜ (S) < 0 \leftrightarrow 1 < 0 + ℜ (S))$
69	56 67 68	mp3an13	$⊢ ℜ (S) \in ℝ \to (1 - ℜ (S) < 0 \leftrightarrow 1 < 0 + ℜ (S))$
70	40 69	syl	$⊢ φ \to (1 - ℜ (S) < 0 \leftrightarrow 1 < 0 + ℜ (S))$
71	66 70	mpbird	$⊢ φ \to 1 - ℜ (S) < 0$
72		2re	$⊢ 2 \in ℝ$
73		1lt2	$⊢ 1 < 2$
74		cxplt	$⊢ ((2 \in ℝ \land 1 < 2) \land (1 - ℜ (S) \in ℝ \land 0 \in ℝ)) \to (1 - ℜ (S) < 0 \leftrightarrow 2^{1 - ℜ (S)} < 2^{0})$
75	72 73 74	mpanl12	$⊢ (1 - ℜ (S) \in ℝ \land 0 \in ℝ) \to (1 - ℜ (S) < 0 \leftrightarrow 2^{1 - ℜ (S)} < 2^{0})$
76	58 67 75	sylancl	$⊢ φ \to (1 - ℜ (S) < 0 \leftrightarrow 2^{1 - ℜ (S)} < 2^{0})$
77	71 76	mpbid	$⊢ φ \to 2^{1 - ℜ (S)} < 2^{0}$
78	60	rprege0d	$⊢ φ \to (2^{1 - ℜ (S)} \in ℝ \land 0 \leq 2^{1 - ℜ (S)})$
79		absid	$⊢ (2^{1 - ℜ (S)} \in ℝ \land 0 \leq 2^{1 - ℜ (S)}) \to \|2^{1 - ℜ (S)}\| = 2^{1 - ℜ (S)}$
80	78 79	syl	$⊢ φ \to \|2^{1 - ℜ (S)}\| = 2^{1 - ℜ (S)}$
81		2cn	$⊢ 2 \in ℂ$
82		cxp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
83	81 82	ax-mp	$⊢ 2^{0} = 1$
84	83	eqcomi	$⊢ 1 = 2^{0}$
85	84	a1i	$⊢ φ \to 1 = 2^{0}$
86	77 80 85	3brtr4d	$⊢ φ \to \|2^{1 - ℜ (S)}\| < 1$
87		oveq2	$⊢ n = m \to {(2^{1 - ℜ (S)})}^{n} = {(2^{1 - ℜ (S)})}^{m}$
88		eqid	$⊢ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n}) = (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})$
89		ovex	$⊢ {(2^{1 - ℜ (S)})}^{m} \in V$
90	87 88 89	fvmpt	$⊢ m \in ℕ_{0} \to (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n}) (m) = {(2^{1 - ℜ (S)})}^{m}$
91	90	adantl	$⊢ (φ \land m \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n}) (m) = {(2^{1 - ℜ (S)})}^{m}$
92	61 86 91	geolim	$⊢ φ \to seq 0 (+ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})) ⇝ (\frac{1}{1 - 2^{1 - ℜ (S)}})$
93		seqex	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})) \in V$
94		ovex	$⊢ \frac{1}{1 - 2^{1 - ℜ (S)}} \in V$
95	93 94	breldm	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})) ⇝ (\frac{1}{1 - 2^{1 - ℜ (S)}}) \to seq 0 (+ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})) \in dom ⇝$
96	92 95	syl	$⊢ φ \to seq 0 (+ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})) \in dom ⇝$
97		rpcxpcl	$⊢ (k \in ℝ^{+} \land - ℜ (S) \in ℝ) \to k^{- ℜ (S)} \in ℝ^{+}$
98	20 41 97	syl2anr	$⊢ (φ \land k \in ℕ) \to k^{- ℜ (S)} \in ℝ^{+}$
99	98	rpred	$⊢ (φ \land k \in ℕ) \to k^{- ℜ (S)} \in ℝ$
100	10 99	eqeltrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k) \in ℝ$
101	98	rpge0d	$⊢ (φ \land k \in ℕ) \to 0 \leq k^{- ℜ (S)}$
102	101 10	breqtrrd	$⊢ (φ \land k \in ℕ) \to 0 \leq (n \in ℕ ⟼ n^{- ℜ (S)}) (k)$
103		nnre	$⊢ k \in ℕ \to k \in ℝ$
104	103	lep1d	$⊢ k \in ℕ \to k \leq k + 1$
105	20	reeflogd	$⊢ k \in ℕ \to e^{\log k} = k$
106		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
107	106	nnrpd	$⊢ k \in ℕ \to k + 1 \in ℝ^{+}$
108	107	reeflogd	$⊢ k \in ℕ \to e^{\log (k + 1)} = k + 1$
109	104 105 108	3brtr4d	$⊢ k \in ℕ \to e^{\log k} \leq e^{\log (k + 1)}$
110	107	relogcld	$⊢ k \in ℕ \to \log (k + 1) \in ℝ$
111		efle	$⊢ (\log k \in ℝ \land \log (k + 1) \in ℝ) \to (\log k \leq \log (k + 1) \leftrightarrow e^{\log k} \leq e^{\log (k + 1)})$
112	21 110 111	syl2anc	$⊢ k \in ℕ \to (\log k \leq \log (k + 1) \leftrightarrow e^{\log k} \leq e^{\log (k + 1)})$
113	109 112	mpbird	$⊢ k \in ℕ \to \log k \leq \log (k + 1)$
114	113	adantl	$⊢ (φ \land k \in ℕ) \to \log k \leq \log (k + 1)$
115	21	adantl	$⊢ (φ \land k \in ℕ) \to \log k \in ℝ$
116	106	adantl	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ$
117	116	nnrpd	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℝ^{+}$
118	117	relogcld	$⊢ (φ \land k \in ℕ) \to \log (k + 1) \in ℝ$
119	40	adantr	$⊢ (φ \land k \in ℕ) \to ℜ (S) \in ℝ$
120	67	a1i	$⊢ φ \to 0 \in ℝ$
121	56	a1i	$⊢ φ \to 1 \in ℝ$
122		0lt1	$⊢ 0 < 1$
123	122	a1i	$⊢ φ \to 0 < 1$
124	120 121 40 123 2	lttrd	$⊢ φ \to 0 < ℜ (S)$
125	124	adantr	$⊢ (φ \land k \in ℕ) \to 0 < ℜ (S)$
126		lemul2	$⊢ (\log k \in ℝ \land \log (k + 1) \in ℝ \land (ℜ (S) \in ℝ \land 0 < ℜ (S))) \to (\log k \leq \log (k + 1) \leftrightarrow ℜ (S) \log k \leq ℜ (S) \log (k + 1))$
127	115 118 119 125 126	syl112anc	$⊢ (φ \land k \in ℕ) \to (\log k \leq \log (k + 1) \leftrightarrow ℜ (S) \log k \leq ℜ (S) \log (k + 1))$
128	114 127	mpbid	$⊢ (φ \land k \in ℕ) \to ℜ (S) \log k \leq ℜ (S) \log (k + 1)$
129		remulcl	$⊢ (ℜ (S) \in ℝ \land \log k \in ℝ) \to ℜ (S) \log k \in ℝ$
130	40 21 129	syl2an	$⊢ (φ \land k \in ℕ) \to ℜ (S) \log k \in ℝ$
131		remulcl	$⊢ (ℜ (S) \in ℝ \land \log (k + 1) \in ℝ) \to ℜ (S) \log (k + 1) \in ℝ$
132	40 110 131	syl2an	$⊢ (φ \land k \in ℕ) \to ℜ (S) \log (k + 1) \in ℝ$
133	130 132	lenegd	$⊢ (φ \land k \in ℕ) \to (ℜ (S) \log k \leq ℜ (S) \log (k + 1) \leftrightarrow - ℜ (S) \log (k + 1) \leq - ℜ (S) \log k)$
134	128 133	mpbid	$⊢ (φ \land k \in ℕ) \to - ℜ (S) \log (k + 1) \leq - ℜ (S) \log k$
135	110	recnd	$⊢ k \in ℕ \to \log (k + 1) \in ℂ$
136		mulneg1	$⊢ (ℜ (S) \in ℂ \land \log (k + 1) \in ℂ) \to (- ℜ (S)) \log (k + 1) = - ℜ (S) \log (k + 1)$
137	64 135 136	syl2an	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log (k + 1) = - ℜ (S) \log (k + 1)$
138		mulneg1	$⊢ (ℜ (S) \in ℂ \land \log k \in ℂ) \to (- ℜ (S)) \log k = - ℜ (S) \log k$
139	64 22 138	syl2an	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log k = - ℜ (S) \log k$
140	134 137 139	3brtr4d	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log (k + 1) \leq (- ℜ (S)) \log k$
141		remulcl	$⊢ (- ℜ (S) \in ℝ \land \log (k + 1) \in ℝ) \to (- ℜ (S)) \log (k + 1) \in ℝ$
142	41 110 141	syl2an	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log (k + 1) \in ℝ$
143		remulcl	$⊢ (- ℜ (S) \in ℝ \land \log k \in ℝ) \to (- ℜ (S)) \log k \in ℝ$
144	41 21 143	syl2an	$⊢ (φ \land k \in ℕ) \to (- ℜ (S)) \log k \in ℝ$
145		efle	$⊢ ((- ℜ (S)) \log (k + 1) \in ℝ \land (- ℜ (S)) \log k \in ℝ) \to ((- ℜ (S)) \log (k + 1) \leq (- ℜ (S)) \log k \leftrightarrow e^{(- ℜ (S)) \log (k + 1)} \leq e^{(- ℜ (S)) \log k})$
146	142 144 145	syl2anc	$⊢ (φ \land k \in ℕ) \to ((- ℜ (S)) \log (k + 1) \leq (- ℜ (S)) \log k \leftrightarrow e^{(- ℜ (S)) \log (k + 1)} \leq e^{(- ℜ (S)) \log k})$
147	140 146	mpbid	$⊢ (φ \land k \in ℕ) \to e^{(- ℜ (S)) \log (k + 1)} \leq e^{(- ℜ (S)) \log k}$
148		oveq1	$⊢ n = k + 1 \to n^{- ℜ (S)} = {(k + 1)}^{- ℜ (S)}$
149		ovex	$⊢ {(k + 1)}^{- ℜ (S)} \in V$
150	148 7 149	fvmpt	$⊢ k + 1 \in ℕ \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k + 1) = {(k + 1)}^{- ℜ (S)}$
151	116 150	syl	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k + 1) = {(k + 1)}^{- ℜ (S)}$
152	116	nncnd	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℂ$
153	116	nnne0d	$⊢ (φ \land k \in ℕ) \to k + 1 \neq 0$
154	152 153 48	cxpefd	$⊢ (φ \land k \in ℕ) \to {(k + 1)}^{- ℜ (S)} = e^{(- ℜ (S)) \log (k + 1)}$
155	151 154	eqtrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k + 1) = e^{(- ℜ (S)) \log (k + 1)}$
156	10 49	eqtrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k) = e^{(- ℜ (S)) \log k}$
157	147 155 156	3brtr4d	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (k + 1) \leq (n \in ℕ ⟼ n^{- ℜ (S)}) (k)$
158	58	recnd	$⊢ φ \to 1 - ℜ (S) \in ℂ$
159	158	adantr	$⊢ (φ \land m \in ℕ_{0}) \to 1 - ℜ (S) \in ℂ$
160		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
161	160	adantl	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℝ$
162	161	recnd	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℂ$
163	159 162	mulcomd	$⊢ (φ \land m \in ℕ_{0}) \to (1 - ℜ (S)) m = m (1 - ℜ (S))$
164	163	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to 2^{(1 - ℜ (S)) m} = 2^{m (1 - ℜ (S))}$
165	55	a1i	$⊢ (φ \land m \in ℕ_{0}) \to 2 \in ℝ^{+}$
166	165 161 159	cxpmuld	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m (1 - ℜ (S))} = {(2^{m})}^{1 - ℜ (S)}$
167		simpr	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℕ_{0}$
168		cxpexp	$⊢ (2 \in ℂ \land m \in ℕ_{0}) \to 2^{m} = 2^{m}$
169	81 167 168	sylancr	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m} = 2^{m}$
170		ax-1cn	$⊢ 1 \in ℂ$
171	64	adantr	$⊢ (φ \land m \in ℕ_{0}) \to ℜ (S) \in ℂ$
172		negsub	$⊢ (1 \in ℂ \land ℜ (S) \in ℂ) \to 1 + (- ℜ (S)) = 1 - ℜ (S)$
173	170 171 172	sylancr	$⊢ (φ \land m \in ℕ_{0}) \to 1 + (- ℜ (S)) = 1 - ℜ (S)$
174	173	eqcomd	$⊢ (φ \land m \in ℕ_{0}) \to 1 - ℜ (S) = 1 + (- ℜ (S))$
175	169 174	oveq12d	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{m})}^{1 - ℜ (S)} = {(2^{m})}^{1 + (- ℜ (S))}$
176	164 166 175	3eqtrd	$⊢ (φ \land m \in ℕ_{0}) \to 2^{(1 - ℜ (S)) m} = {(2^{m})}^{1 + (- ℜ (S))}$
177	58	adantr	$⊢ (φ \land m \in ℕ_{0}) \to 1 - ℜ (S) \in ℝ$
178	165 177 162	cxpmuld	$⊢ (φ \land m \in ℕ_{0}) \to 2^{(1 - ℜ (S)) m} = {(2^{1 - ℜ (S)})}^{m}$
179		2nn	$⊢ 2 \in ℕ$
180		nnexpcl	$⊢ (2 \in ℕ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
181	179 180	mpan	$⊢ m \in ℕ_{0} \to 2^{m} \in ℕ$
182	181	adantl	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
183	182	nncnd	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m} \in ℂ$
184	182	nnne0d	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m} \neq 0$
185		1cnd	$⊢ (φ \land m \in ℕ_{0}) \to 1 \in ℂ$
186	42	adantr	$⊢ (φ \land m \in ℕ_{0}) \to - ℜ (S) \in ℂ$
187	183 184 185 186	cxpaddd	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{m})}^{1 + (- ℜ (S))} = {(2^{m})}^{1} {(2^{m})}^{- ℜ (S)}$
188	176 178 187	3eqtr3d	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{1 - ℜ (S)})}^{m} = {(2^{m})}^{1} {(2^{m})}^{- ℜ (S)}$
189		cxpexp	$⊢ (2^{1 - ℜ (S)} \in ℂ \land m \in ℕ_{0}) \to {(2^{1 - ℜ (S)})}^{m} = {(2^{1 - ℜ (S)})}^{m}$
190	61 189	sylan	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{1 - ℜ (S)})}^{m} = {(2^{1 - ℜ (S)})}^{m}$
191	183	cxp1d	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{m})}^{1} = 2^{m}$
192	191	oveq1d	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{m})}^{1} {(2^{m})}^{- ℜ (S)} = 2^{m} {(2^{m})}^{- ℜ (S)}$
193	188 190 192	3eqtr3d	$⊢ (φ \land m \in ℕ_{0}) \to {(2^{1 - ℜ (S)})}^{m} = 2^{m} {(2^{m})}^{- ℜ (S)}$
194	179 167 180	sylancr	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
195		oveq1	$⊢ n = 2^{m} \to n^{- ℜ (S)} = {(2^{m})}^{- ℜ (S)}$
196		ovex	$⊢ {(2^{m})}^{- ℜ (S)} \in V$
197	195 7 196	fvmpt	$⊢ 2^{m} \in ℕ \to (n \in ℕ ⟼ n^{- ℜ (S)}) (2^{m}) = {(2^{m})}^{- ℜ (S)}$
198	194 197	syl	$⊢ (φ \land m \in ℕ_{0}) \to (n \in ℕ ⟼ n^{- ℜ (S)}) (2^{m}) = {(2^{m})}^{- ℜ (S)}$
199	198	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to 2^{m} (n \in ℕ ⟼ n^{- ℜ (S)}) (2^{m}) = 2^{m} {(2^{m})}^{- ℜ (S)}$
200	193 91 199	3eqtr4d	$⊢ (φ \land m \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n}) (m) = 2^{m} (n \in ℕ ⟼ n^{- ℜ (S)}) (2^{m})$
201	100 102 157 200	climcnds	$⊢ φ \to (seq 1 (+ (n \in ℕ ⟼ n^{- ℜ (S)})) \in dom ⇝ \leftrightarrow seq 0 (+ (n \in ℕ_{0} ⟼ {(2^{1 - ℜ (S)})}^{n})) \in dom ⇝)$
202	96 201	mpbird	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ n^{- ℜ (S)})) \in dom ⇝$
203	4 5 52 54 202	abscvgcvg	$⊢ φ \to seq 1 (+ F) \in dom ⇝$

Metamath Proof Explorer

Theorem zetacvg

Proof