binomcxplemnotnn0

Description: Lemma for binomcxp . When C is not a nonnegative integer, the generalized sum in binomcxplemnn0 —which we will call P —is a convergent power series: its base b is always of smaller absolute value than the radius of convergence.

pserdv2 gives the derivative of P , which by dvradcnv also converges in that radius. When A is fixed at one, ( A + b ) times that derivative equals ( C x. P ) and fraction ( P / ( ( A + b ) ^c C ) ) is always defined with derivative zero, so the fraction is a constant—specifically one, because ( ( 1 + 0 ) ^c C ) = 1 . Thus ( ( 1 + b ) ^c C ) = ( Pb ) .

Finally, let b be ( B / A ) , and multiply both the binomial ( ( 1 + ( B / A ) ) ^c C ) and the sum ( P( B / A ) ) by ( A ^c C ) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
	binomcxp.b	$⊢ φ \to B \in ℝ$
	binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
	binomcxp.c	$⊢ φ \to C \in ℂ$
	binomcxplem.f	$⊢ F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
	binomcxplem.s	$⊢ S = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
	binomcxplem.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
	binomcxplem.e	$⊢ E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
	binomcxplem.d	$⊢ D = {abs}^{-1} [[0, R)]$
	binomcxplem.p	$⊢ P = (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k))$
Assertion	binomcxplemnotnn0	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k}$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
2		binomcxp.b	$⊢ φ \to B \in ℝ$
3		binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
4		binomcxp.c	$⊢ φ \to C \in ℂ$
5		binomcxplem.f	$⊢ F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
6		binomcxplem.s	$⊢ S = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
7		binomcxplem.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
8		binomcxplem.e	$⊢ E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
9		binomcxplem.d	$⊢ D = {abs}^{-1} [[0, R)]$
10		binomcxplem.p	$⊢ P = (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k))$
11		nfcv	$⊢ \underline{Ⅎ} b {abs}^{-1}$
12		nfcv	$⊢ \underline{Ⅎ} b 0$
13		nfcv	$⊢ \underline{Ⅎ} b [.)$
14		nfcv	$⊢ \underline{Ⅎ} b +$
15		nfmpt1	$⊢ \underline{Ⅎ} b (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
16	6 15	nfcxfr	$⊢ \underline{Ⅎ} b S$
17		nfcv	$⊢ \underline{Ⅎ} b r$
18	16 17	nffv	$⊢ \underline{Ⅎ} b S (r)$
19	12 14 18	nfseq	$⊢ \underline{Ⅎ} b seq 0 (+ S (r))$
20	19	nfel1	$⊢ Ⅎ b seq 0 (+ S (r)) \in dom ⇝$
21		nfcv	$⊢ \underline{Ⅎ} b ℝ$
22	20 21	nfrabw	$⊢ \underline{Ⅎ} b \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\}$
23		nfcv	$⊢ \underline{Ⅎ} b ℝ^{*}$
24		nfcv	$⊢ \underline{Ⅎ} b <$
25	22 23 24	nfsup	$⊢ \underline{Ⅎ} b sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
26	7 25	nfcxfr	$⊢ \underline{Ⅎ} b R$
27	12 13 26	nfov	$⊢ \underline{Ⅎ} b [0, R)$
28	11 27	nfima	$⊢ \underline{Ⅎ} b {abs}^{-1} [[0, R)]$
29	9 28	nfcxfr	$⊢ \underline{Ⅎ} b D$
30		nfcv	$⊢ \underline{Ⅎ} x D$
31		nfcv	$⊢ \underline{Ⅎ} x \sum_{k \in ℕ_{0}} S (b) (k)$
32		nfcv	$⊢ \underline{Ⅎ} b ℕ_{0}$
33		nfcv	$⊢ \underline{Ⅎ} b x$
34	16 33	nffv	$⊢ \underline{Ⅎ} b S (x)$
35		nfcv	$⊢ \underline{Ⅎ} b k$
36	34 35	nffv	$⊢ \underline{Ⅎ} b S (x) (k)$
37	32 36	nfsum	$⊢ \underline{Ⅎ} b \sum_{k \in ℕ_{0}} S (x) (k)$
38		simpl	$⊢ (b = x \land k \in ℕ_{0}) \to b = x$
39	38	fveq2d	$⊢ (b = x \land k \in ℕ_{0}) \to S (b) = S (x)$
40	39	fveq1d	$⊢ (b = x \land k \in ℕ_{0}) \to S (b) (k) = S (x) (k)$
41	40	sumeq2dv	$⊢ b = x \to \sum_{k \in ℕ_{0}} S (b) (k) = \sum_{k \in ℕ_{0}} S (x) (k)$
42	29 30 31 37 41	cbvmptf	$⊢ (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k)) = (x \in D ⟼ \sum_{k \in ℕ_{0}} S (x) (k))$
43	10 42	eqtri	$⊢ P = (x \in D ⟼ \sum_{k \in ℕ_{0}} S (x) (k))$
44	43	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to P = (x \in D ⟼ \sum_{k \in ℕ_{0}} S (x) (k))$
45		simplr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \land k \in ℕ_{0}) \to x = \frac{B}{A}$
46	45	fveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \land k \in ℕ_{0}) \to S (x) = S (\frac{B}{A})$
47	46	fveq1d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \land k \in ℕ_{0}) \to S (x) (k) = S (\frac{B}{A}) (k)$
48	47	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \to \sum_{k \in ℕ_{0}} S (x) (k) = \sum_{k \in ℕ_{0}} S (\frac{B}{A}) (k)$
49	2	recnd	$⊢ φ \to B \in ℂ$
50	49	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to B \in ℂ$
51	1	rpcnd	$⊢ φ \to A \in ℂ$
52	51	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to A \in ℂ$
53		0red	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \in ℝ$
54	50	abscld	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|B\| \in ℝ$
55	52	abscld	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|A\| \in ℝ$
56	50	absge0d	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \leq \|B\|$
57	3	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|B\| < \|A\|$
58	53 54 55 56 57	lelttrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 < \|A\|$
59	58	gt0ne0d	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|A\| \neq 0$
60	52	abs00ad	$⊢ (φ \land \neg C \in ℕ_{0}) \to (\|A\| = 0 \leftrightarrow A = 0)$
61	60	necon3bid	$⊢ (φ \land \neg C \in ℕ_{0}) \to (\|A\| \neq 0 \leftrightarrow A \neq 0)$
62	59 61	mpbid	$⊢ (φ \land \neg C \in ℕ_{0}) \to A \neq 0$
63	50 52 62	divcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{B}{A} \in ℂ$
64	63	abscld	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|\frac{B}{A}\| \in ℝ$
65	63	absge0d	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \leq \|\frac{B}{A}\|$
66	55	recnd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|A\| \in ℂ$
67	66	mulid1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|A\| \cdot 1 = \|A\|$
68	57 67	breqtrrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|B\| < \|A\| \cdot 1$
69		1red	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 \in ℝ$
70	55 58	elrpd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|A\| \in ℝ^{+}$
71	54 69 70	ltdivmuld	$⊢ (φ \land \neg C \in ℕ_{0}) \to (\frac{\|B\|}{\|A\|} < 1 \leftrightarrow \|B\| < \|A\| \cdot 1)$
72	68 71	mpbird	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{\|B\|}{\|A\|} < 1$
73	50 52 62	absdivd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|\frac{B}{A}\| = \frac{\|B\|}{\|A\|}$
74	1 2 3 4 5 6 7	binomcxplemradcnv	$⊢ (φ \land \neg C \in ℕ_{0}) \to R = 1$
75	72 73 74	3brtr4d	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|\frac{B}{A}\| < R$
76		0re	$⊢ 0 \in ℝ$
77		ssrab2	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ$
78		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
79	77 78	sstri	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ^{*}$
80		supxrcl	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ^{} \to sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{*}$
81	79 80	ax-mp	$⊢ sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{}$
82	7 81	eqeltri	$⊢ R \in ℝ^{*}$
83		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|\frac{B}{A}\| \in [0, R) \leftrightarrow (\|\frac{B}{A}\| \in ℝ \land 0 \leq \|\frac{B}{A}\| \land \|\frac{B}{A}\| < R))$
84	76 82 83	mp2an	$⊢ \|\frac{B}{A}\| \in [0, R) \leftrightarrow (\|\frac{B}{A}\| \in ℝ \land 0 \leq \|\frac{B}{A}\| \land \|\frac{B}{A}\| < R)$
85	64 65 75 84	syl3anbrc	$⊢ (φ \land \neg C \in ℕ_{0}) \to \|\frac{B}{A}\| \in [0, R)$
86	9	eleq2i	$⊢ \frac{B}{A} \in D \leftrightarrow \frac{B}{A} \in {abs}^{-1} [[0, R)]$
87		absf	$⊢ abs : ℂ ⟶ ℝ$
88		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
89		elpreima	$⊢ abs Fn ℂ \to (\frac{B}{A} \in {abs}^{-1} [[0, R)] \leftrightarrow (\frac{B}{A} \in ℂ \land \|\frac{B}{A}\| \in [0, R)))$
90	87 88 89	mp2b	$⊢ \frac{B}{A} \in {abs}^{-1} [[0, R)] \leftrightarrow (\frac{B}{A} \in ℂ \land \|\frac{B}{A}\| \in [0, R))$
91	86 90	bitri	$⊢ \frac{B}{A} \in D \leftrightarrow (\frac{B}{A} \in ℂ \land \|\frac{B}{A}\| \in [0, R))$
92	63 85 91	sylanbrc	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{B}{A} \in D$
93		sumex	$⊢ \sum_{k \in ℕ_{0}} S (\frac{B}{A}) (k) \in V$
94	93	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} S (\frac{B}{A}) (k) \in V$
95	44 48 92 94	fvmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to P (\frac{B}{A}) = \sum_{k \in ℕ_{0}} S (\frac{B}{A}) (k)$
96		eqid	$⊢ abs \circ - = abs \circ -$
97	96	cnbl0	$⊢ R \in ℝ^{*} \to {abs}^{-1} [[0, R)] = 0 ball (abs \circ -) R$
98	82 97	ax-mp	$⊢ {abs}^{-1} [[0, R)] = 0 ball (abs \circ -) R$
99	9 98	eqtri	$⊢ D = 0 ball (abs \circ -) R$
100		0cnd	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \in ℂ$
101	82	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to R \in ℝ^{*}$
102		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
103	102	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
104		nfv	$⊢ Ⅎ b (φ \land \neg C \in ℕ_{0})$
105	29	nfcri	$⊢ Ⅎ b x \in D$
106	104 105	nfan	$⊢ Ⅎ b ((φ \land \neg C \in ℕ_{0}) \land x \in D)$
107	37	nfel1	$⊢ Ⅎ b \sum_{k \in ℕ_{0}} S (x) (k) \in ℂ$
108	106 107	nfim	$⊢ Ⅎ b (((φ \land \neg C \in ℕ_{0}) \land x \in D) \to \sum_{k \in ℕ_{0}} S (x) (k) \in ℂ)$
109		eleq1	$⊢ b = x \to (b \in D \leftrightarrow x \in D)$
110	109	anbi2d	$⊢ b = x \to (((φ \land \neg C \in ℕ_{0}) \land b \in D) \leftrightarrow ((φ \land \neg C \in ℕ_{0}) \land x \in D))$
111	41	eleq1d	$⊢ b = x \to (\sum_{k \in ℕ_{0}} S (b) (k) \in ℂ \leftrightarrow \sum_{k \in ℕ_{0}} S (x) (k) \in ℂ)$
112	110 111	imbi12d	$⊢ b = x \to ((((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} S (b) (k) \in ℂ) \leftrightarrow (((φ \land \neg C \in ℕ_{0}) \land x \in D) \to \sum_{k \in ℕ_{0}} S (x) (k) \in ℂ))$
113		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
114		0zd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 0 \in ℤ$
115		eqidd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to S (b) (k) = S (b) (k)$
116		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
117	9 116	eqsstri	$⊢ D \subseteq dom abs$
118	87	fdmi	$⊢ dom abs = ℂ$
119	117 118	sseqtri	$⊢ D \subseteq ℂ$
120	119	sseli	$⊢ b \in D \to b \in ℂ$
121	6	a1i	$⊢ φ \to S = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
122		nn0ex	$⊢ ℕ_{0} \in V$
123	122	mptex	$⊢ (k \in ℕ_{0} ⟼ F (k) b^{k}) \in V$
124	123	a1i	$⊢ (φ \land b \in ℂ) \to (k \in ℕ_{0} ⟼ F (k) b^{k}) \in V$
125	121 124	fvmpt2d	$⊢ (φ \land b \in ℂ) \to S (b) = (k \in ℕ_{0} ⟼ F (k) b^{k})$
126		ovexd	$⊢ ((φ \land b \in ℂ) \land k \in ℕ_{0}) \to F (k) b^{k} \in V$
127	125 126	fvmpt2d	$⊢ ((φ \land b \in ℂ) \land k \in ℕ_{0}) \to S (b) (k) = F (k) b^{k}$
128	5	a1i	$⊢ (φ \land k \in ℕ_{0}) \to F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
129		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to j = k$
130	129	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to C C_{𝑐} j = C C_{𝑐} k$
131		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
132		ovexd	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} k \in V$
133	128 130 131 132	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
134	133	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to F (k) b^{k} = (C C_{𝑐} k) b^{k}$
135	134	adantlr	$⊢ ((φ \land b \in ℂ) \land k \in ℕ_{0}) \to F (k) b^{k} = (C C_{𝑐} k) b^{k}$
136	127 135	eqtrd	$⊢ ((φ \land b \in ℂ) \land k \in ℕ_{0}) \to S (b) (k) = (C C_{𝑐} k) b^{k}$
137	120 136	sylanl2	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to S (b) (k) = (C C_{𝑐} k) b^{k}$
138	4	ad2antrr	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to C \in ℂ$
139		simpr	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
140	138 139	bcccl	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
141	120	ad2antlr	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to b \in ℂ$
142	141 139	expcld	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to b^{k} \in ℂ$
143	140 142	mulcld	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to (C C_{𝑐} k) b^{k} \in ℂ$
144	137 143	eqeltrd	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to S (b) (k) \in ℂ$
145	144	adantllr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to S (b) (k) \in ℂ$
146		eleq1	$⊢ x = b \to (x \in D \leftrightarrow b \in D)$
147	146	anbi2d	$⊢ x = b \to ((φ \land x \in D) \leftrightarrow (φ \land b \in D))$
148		fveq2	$⊢ x = b \to S (x) = S (b)$
149	148	seqeq3d	$⊢ x = b \to seq 0 (+ S (x)) = seq 0 (+ S (b))$
150	149	eleq1d	$⊢ x = b \to (seq 0 (+ S (x)) \in dom ⇝ \leftrightarrow seq 0 (+ S (b)) \in dom ⇝)$
151		fveq2	$⊢ x = b \to E (x) = E (b)$
152	151	seqeq3d	$⊢ x = b \to seq 1 (+ E (x)) = seq 1 (+ E (b))$
153	152	eleq1d	$⊢ x = b \to (seq 1 (+ E (x)) \in dom ⇝ \leftrightarrow seq 1 (+ E (b)) \in dom ⇝)$
154	150 153	anbi12d	$⊢ x = b \to ((seq 0 (+ S (x)) \in dom ⇝ \land seq 1 (+ E (x)) \in dom ⇝) \leftrightarrow (seq 0 (+ S (b)) \in dom ⇝ \land seq 1 (+ E (b)) \in dom ⇝))$
155	147 154	imbi12d	$⊢ x = b \to (((φ \land x \in D) \to (seq 0 (+ S (x)) \in dom ⇝ \land seq 1 (+ E (x)) \in dom ⇝)) \leftrightarrow ((φ \land b \in D) \to (seq 0 (+ S (b)) \in dom ⇝ \land seq 1 (+ E (b)) \in dom ⇝)))$
156	1 2 3 4 5 6 7 8 9	binomcxplemcvg	$⊢ (φ \land x \in D) \to (seq 0 (+ S (x)) \in dom ⇝ \land seq 1 (+ E (x)) \in dom ⇝)$
157	155 156	chvarvv	$⊢ (φ \land b \in D) \to (seq 0 (+ S (b)) \in dom ⇝ \land seq 1 (+ E (b)) \in dom ⇝)$
158	157	simpld	$⊢ (φ \land b \in D) \to seq 0 (+ S (b)) \in dom ⇝$
159	158	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 0 (+ S (b)) \in dom ⇝$
160	113 114 115 145 159	isumcl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} S (b) (k) \in ℂ$
161	108 112 160	chvarfv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to \sum_{k \in ℕ_{0}} S (x) (k) \in ℂ$
162	161 43	fmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to P : D ⟶ ℂ$
163		1cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to 1 \in ℂ$
164	119	sseli	$⊢ x \in D \to x \in ℂ$
165	164	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to x \in ℂ$
166	163 165	addcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to 1 + x \in ℂ$
167	4	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to C \in ℂ$
168	167	negcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to - C \in ℂ$
169	166 168	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to {(1 + x)}^{- C} \in ℂ$
170		nfcv	$⊢ \underline{Ⅎ} x {(1 + b)}^{- C}$
171		nfcv	$⊢ \underline{Ⅎ} b {(1 + x)}^{- C}$
172		oveq2	$⊢ b = x \to 1 + b = 1 + x$
173	172	oveq1d	$⊢ b = x \to {(1 + b)}^{- C} = {(1 + x)}^{- C}$
174	29 30 170 171 173	cbvmptf	$⊢ (b \in D ⟼ {(1 + b)}^{- C}) = (x \in D ⟼ {(1 + x)}^{- C})$
175	169 174	fmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ {(1 + b)}^{- C}) : D ⟶ ℂ$
176		cnex	$⊢ ℂ \in V$
177		fex	$⊢ (abs : ℂ ⟶ ℝ \land ℂ \in V) \to abs \in V$
178	87 176 177	mp2an	$⊢ abs \in V$
179	178	cnvex	$⊢ {abs}^{-1} \in V$
180		imaexg	$⊢ {abs}^{-1} \in V \to {abs}^{-1} [[0, R)] \in V$
181	179 180	ax-mp	$⊢ {abs}^{-1} [[0, R)] \in V$
182	9 181	eqeltri	$⊢ D \in V$
183	182	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to D \in V$
184		inidm	$⊢ D \cap D = D$
185	103 162 175 183 183 184	off	$⊢ (φ \land \neg C \in ℕ_{0}) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) : D ⟶ ℂ$
186		1ex	$⊢ 1 \in V$
187	186	fconst	$⊢ (D \times \{1\}) : D ⟶ \{1\}$
188		fconstmpt	$⊢ D \times \{1\} = (x \in D ⟼ 1)$
189		nfcv	$⊢ \underline{Ⅎ} b 1$
190		nfcv	$⊢ \underline{Ⅎ} x 1$
191		eqidd	$⊢ x = b \to 1 = 1$
192	30 29 189 190 191	cbvmptf	$⊢ (x \in D ⟼ 1) = (b \in D ⟼ 1)$
193	188 192	eqtri	$⊢ D \times \{1\} = (b \in D ⟼ 1)$
194	193	feq1i	$⊢ (D \times \{1\}) : D ⟶ \{1\} \leftrightarrow (b \in D ⟼ 1) : D ⟶ \{1\}$
195	187 194	mpbi	$⊢ (b \in D ⟼ 1) : D ⟶ \{1\}$
196		ax-1cn	$⊢ 1 \in ℂ$
197		snssi	$⊢ 1 \in ℂ \to \{1\} \subseteq ℂ$
198	196 197	ax-mp	$⊢ \{1\} \subseteq ℂ$
199		fss	$⊢ ((b \in D ⟼ 1) : D ⟶ \{1\} \land \{1\} \subseteq ℂ) \to (b \in D ⟼ 1) : D ⟶ ℂ$
200	195 198 199	mp2an	$⊢ (b \in D ⟼ 1) : D ⟶ ℂ$
201	200	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ 1) : D ⟶ ℂ$
202		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
203	202	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ \in \{ℝ, ℂ\}$
204	1 2 3 4 5 6 7 8 9 10	binomcxplemdvsum	$⊢ φ \to ℂ D P = (b \in D ⟼ \sum_{k \in ℕ} E (b) (k))$
205	204	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D P = (b \in D ⟼ \sum_{k \in ℕ} E (b) (k))$
206		nfcv	$⊢ \underline{Ⅎ} x \sum_{k \in ℕ} E (b) (k)$
207		nfcv	$⊢ \underline{Ⅎ} b ℕ$
208		nfmpt1	$⊢ \underline{Ⅎ} b (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
209	8 208	nfcxfr	$⊢ \underline{Ⅎ} b E$
210	209 33	nffv	$⊢ \underline{Ⅎ} b E (x)$
211	210 35	nffv	$⊢ \underline{Ⅎ} b E (x) (k)$
212	207 211	nfsum	$⊢ \underline{Ⅎ} b \sum_{k \in ℕ} E (x) (k)$
213		simpl	$⊢ (b = x \land k \in ℕ) \to b = x$
214	213	fveq2d	$⊢ (b = x \land k \in ℕ) \to E (b) = E (x)$
215	214	fveq1d	$⊢ (b = x \land k \in ℕ) \to E (b) (k) = E (x) (k)$
216	215	sumeq2dv	$⊢ b = x \to \sum_{k \in ℕ} E (b) (k) = \sum_{k \in ℕ} E (x) (k)$
217	29 30 206 212 216	cbvmptf	$⊢ (b \in D ⟼ \sum_{k \in ℕ} E (b) (k)) = (x \in D ⟼ \sum_{k \in ℕ} E (x) (k))$
218	205 217	eqtrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D P = (x \in D ⟼ \sum_{k \in ℕ} E (x) (k))$
219		sumex	$⊢ \sum_{k \in ℕ} E (x) (k) \in V$
220	219	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to \sum_{k \in ℕ} E (x) (k) \in V$
221	218 220	fmpt3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to P_{ℂ}^{'} : D ⟶ V$
222	221	fdmd	$⊢ (φ \land \neg C \in ℕ_{0}) \to dom P_{ℂ}^{'} = D$
223	1 2 3 4 5 6 7 8 9	binomcxplemdvbinom	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$
224		nfcv	$⊢ \underline{Ⅎ} x (- C) {(1 + b)}^{- C - 1}$
225		nfcv	$⊢ \underline{Ⅎ} b (- C) {(1 + x)}^{- C - 1}$
226	172	oveq1d	$⊢ b = x \to {(1 + b)}^{- C - 1} = {(1 + x)}^{- C - 1}$
227	226	oveq2d	$⊢ b = x \to (- C) {(1 + b)}^{- C - 1} = (- C) {(1 + x)}^{- C - 1}$
228	29 30 224 225 227	cbvmptf	$⊢ (b \in D ⟼ (- C) {(1 + b)}^{- C - 1}) = (x \in D ⟼ (- C) {(1 + x)}^{- C - 1})$
229	223 228	eqtrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} = (x \in D ⟼ (- C) {(1 + x)}^{- C - 1})$
230	168 163	subcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to - C - 1 \in ℂ$
231	166 230	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to {(1 + x)}^{- C - 1} \in ℂ$
232	168 231	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to (- C) {(1 + x)}^{- C - 1} \in ℂ$
233	229 232	fmpt3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} : D ⟶ ℂ$
234	233	fdmd	$⊢ (φ \land \neg C \in ℕ_{0}) \to dom \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} = D$
235	203 162 175 222 234	dvmulf	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) = (P_{ℂ}^{'} \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) +_{f} (\frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} \times_{f} P)$
236	4	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C \in ℂ$
237	236	mulid1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C \cdot 1 = C$
238	237	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C \cdot 1 + C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k} = C + C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
239		1cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 \in ℂ$
240		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
241		1zzd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 \in ℤ$
242		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
243	242 137	sylan2	$⊢ ((φ \land b \in D) \land k \in ℕ) \to S (b) (k) = (C C_{𝑐} k) b^{k}$
244	243	adantllr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to S (b) (k) = (C C_{𝑐} k) b^{k}$
245	4	ad3antrrr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C \in ℂ$
246		simpr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
247	245 246	bcccl	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
248	242 247	sylan2	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to C C_{𝑐} k \in ℂ$
249	120	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to b \in ℂ$
250	249	adantr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to b \in ℂ$
251	250 246	expcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to b^{k} \in ℂ$
252	242 251	sylan2	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b^{k} \in ℂ$
253	248 252	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C C_{𝑐} k) b^{k} \in ℂ$
254		1nn0	$⊢ 1 \in ℕ_{0}$
255	254	a1i	$⊢ (φ \land b \in D) \to 1 \in ℕ_{0}$
256	113 255 144	iserex	$⊢ (φ \land b \in D) \to (seq 0 (+ S (b)) \in dom ⇝ \leftrightarrow seq 1 (+ S (b)) \in dom ⇝)$
257	158 256	mpbid	$⊢ (φ \land b \in D) \to seq 1 (+ S (b)) \in dom ⇝$
258	257	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 1 (+ S (b)) \in dom ⇝$
259	240 241 244 253 258	isumcl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C C_{𝑐} k) b^{k} \in ℂ$
260	236 239 259	adddid	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C (1 + \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}) = C \cdot 1 + C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
261	8	a1i	$⊢ φ \to E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
262		nnex	$⊢ ℕ \in V$
263	262	mptex	$⊢ (k \in ℕ ⟼ k F (k) b^{k - 1}) \in V$
264	263	a1i	$⊢ (φ \land b \in ℂ) \to (k \in ℕ ⟼ k F (k) b^{k - 1}) \in V$
265	261 264	fvmpt2d	$⊢ (φ \land b \in ℂ) \to E (b) = (k \in ℕ ⟼ k F (k) b^{k - 1})$
266	120 265	sylan2	$⊢ (φ \land b \in D) \to E (b) = (k \in ℕ ⟼ k F (k) b^{k - 1})$
267	266	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) = (k \in ℕ ⟼ k F (k) b^{k - 1})$
268		ovexd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to k F (k) b^{k - 1} \in V$
269	267 268	fmpt3d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) : ℕ ⟶ V$
270	269	feqmptd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) = (k \in ℕ ⟼ E (b) (k))$
271		ovexd	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to k F (k) b^{k - 1} \in V$
272	265 271	fvmpt2d	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to E (b) (k) = k F (k) b^{k - 1}$
273	242 133	sylan2	$⊢ (φ \land k \in ℕ) \to F (k) = C C_{𝑐} k$
274	273	oveq2d	$⊢ (φ \land k \in ℕ) \to k F (k) = k (C C_{𝑐} k)$
275	274	oveq1d	$⊢ (φ \land k \in ℕ) \to k F (k) b^{k - 1} = k (C C_{𝑐} k) b^{k - 1}$
276	275	adantlr	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to k F (k) b^{k - 1} = k (C C_{𝑐} k) b^{k - 1}$
277	272 276	eqtrd	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to E (b) (k) = k (C C_{𝑐} k) b^{k - 1}$
278	4	adantr	$⊢ (φ \land k \in ℕ) \to C \in ℂ$
279		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
280	279	adantl	$⊢ (φ \land k \in ℕ) \to k - 1 \in ℕ_{0}$
281	278 280	bccp1k	$⊢ (φ \land k \in ℕ) \to C C_{𝑐} (k - 1 + 1) = (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k - 1 + 1})$
282	242	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℕ_{0}$
283	282	nn0cnd	$⊢ (φ \land k \in ℕ) \to k \in ℂ$
284		1cnd	$⊢ (φ \land k \in ℕ) \to 1 \in ℂ$
285	283 284	npcand	$⊢ (φ \land k \in ℕ) \to k - 1 + 1 = k$
286	285	oveq2d	$⊢ (φ \land k \in ℕ) \to C C_{𝑐} (k - 1 + 1) = C C_{𝑐} k$
287	285	oveq2d	$⊢ (φ \land k \in ℕ) \to \frac{C - (k - 1)}{k - 1 + 1} = \frac{C - (k - 1)}{k}$
288	287	oveq2d	$⊢ (φ \land k \in ℕ) \to (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k - 1 + 1}) = (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k})$
289	281 286 288	3eqtr3d	$⊢ (φ \land k \in ℕ) \to C C_{𝑐} k = (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k})$
290	289	oveq2d	$⊢ (φ \land k \in ℕ) \to k (C C_{𝑐} k) = k (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k})$
291	278 280	bcccl	$⊢ (φ \land k \in ℕ) \to C C_{𝑐} (k - 1) \in ℂ$
292	283 284	subcld	$⊢ (φ \land k \in ℕ) \to k - 1 \in ℂ$
293	278 292	subcld	$⊢ (φ \land k \in ℕ) \to C - (k - 1) \in ℂ$
294		nnne0	$⊢ k \in ℕ \to k \neq 0$
295	294	adantl	$⊢ (φ \land k \in ℕ) \to k \neq 0$
296	291 293 283 295	divassd	$⊢ (φ \land k \in ℕ) \to \frac{(C C_{𝑐} (k - 1)) (C - (k - 1))}{k} = (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k})$
297	296	oveq2d	$⊢ (φ \land k \in ℕ) \to k (\frac{(C C_{𝑐} (k - 1)) (C - (k - 1))}{k}) = k (C C_{𝑐} (k - 1)) (\frac{C - (k - 1)}{k})$
298	291 293	mulcld	$⊢ (φ \land k \in ℕ) \to (C C_{𝑐} (k - 1)) (C - (k - 1)) \in ℂ$
299	298 283 295	divcan2d	$⊢ (φ \land k \in ℕ) \to k (\frac{(C C_{𝑐} (k - 1)) (C - (k - 1))}{k}) = (C C_{𝑐} (k - 1)) (C - (k - 1))$
300	290 297 299	3eqtr2d	$⊢ (φ \land k \in ℕ) \to k (C C_{𝑐} k) = (C C_{𝑐} (k - 1)) (C - (k - 1))$
301	300	oveq1d	$⊢ (φ \land k \in ℕ) \to k (C C_{𝑐} k) b^{k - 1} = (C C_{𝑐} (k - 1)) (C - (k - 1)) b^{k - 1}$
302	301	adantlr	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to k (C C_{𝑐} k) b^{k - 1} = (C C_{𝑐} (k - 1)) (C - (k - 1)) b^{k - 1}$
303	291	adantlr	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to C C_{𝑐} (k - 1) \in ℂ$
304	293	adantlr	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to C - (k - 1) \in ℂ$
305	303 304	mulcomd	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to (C C_{𝑐} (k - 1)) (C - (k - 1)) = (C - (k - 1)) (C C_{𝑐} (k - 1))$
306	305	oveq1d	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to (C C_{𝑐} (k - 1)) (C - (k - 1)) b^{k - 1} = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
307	277 302 306	3eqtrd	$⊢ ((φ \land b \in ℂ) \land k \in ℕ) \to E (b) (k) = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
308	120 307	sylanl2	$⊢ ((φ \land b \in D) \land k \in ℕ) \to E (b) (k) = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
309	308	adantllr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to E (b) (k) = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
310	309	mpteq2dva	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (k \in ℕ ⟼ E (b) (k)) = (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1})$
311	270 310	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) = (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1})$
312	311	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) shift -1 = (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}) shift -1$
313		eqid	$⊢ (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}) = (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1})$
314		ovex	$⊢ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} \in V$
315		oveq1	$⊢ k = j - -1 \to k - 1 = j - -1 - 1$
316	315	oveq2d	$⊢ k = j - -1 \to C - (k - 1) = C - (j - -1 - 1)$
317	315	oveq2d	$⊢ k = j - -1 \to C C_{𝑐} (k - 1) = C C_{𝑐} (j - -1 - 1)$
318	316 317	oveq12d	$⊢ k = j - -1 \to (C - (k - 1)) (C C_{𝑐} (k - 1)) = (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1))$
319	315	oveq2d	$⊢ k = j - -1 \to b^{k - 1} = b^{j - -1 - 1}$
320	318 319	oveq12d	$⊢ k = j - -1 \to (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1)) b^{j - -1 - 1}$
321		1pneg1e0	$⊢ 1 + -1 = 0$
322	321	fveq2i	$⊢ ℤ_{\geq (1 + -1)} = ℤ_{\geq 0}$
323	113 322	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 + -1)}$
324	241	znegcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to - 1 \in ℤ$
325	313 314 320 240 323 241 324	uzmptshftfval	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}) shift -1 = (j \in ℕ_{0} ⟼ (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1)) b^{j - -1 - 1})$
326		oveq1	$⊢ j = k \to j - -1 = k - -1$
327	326	oveq1d	$⊢ j = k \to j - -1 - 1 = k - -1 - 1$
328	327	oveq2d	$⊢ j = k \to C - (j - -1 - 1) = C - (k - -1 - 1)$
329	327	oveq2d	$⊢ j = k \to C C_{𝑐} (j - -1 - 1) = C C_{𝑐} (k - -1 - 1)$
330	328 329	oveq12d	$⊢ j = k \to (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1)) = (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1))$
331	327	oveq2d	$⊢ j = k \to b^{j - -1 - 1} = b^{k - -1 - 1}$
332	330 331	oveq12d	$⊢ j = k \to (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1)) b^{j - -1 - 1} = (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) b^{k - -1 - 1}$
333	332	cbvmptv	$⊢ (j \in ℕ_{0} ⟼ (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1)) b^{j - -1 - 1}) = (k \in ℕ_{0} ⟼ (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) b^{k - -1 - 1})$
334	333	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (j \in ℕ_{0} ⟼ (C - (j - -1 - 1)) (C C_{𝑐} (j - -1 - 1)) b^{j - -1 - 1}) = (k \in ℕ_{0} ⟼ (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) b^{k - -1 - 1})$
335	312 325 334	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) shift -1 = (k \in ℕ_{0} ⟼ (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) b^{k - -1 - 1})$
336		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
337		1cnd	$⊢ k \in ℕ_{0} \to 1 \in ℂ$
338	336 337	subnegd	$⊢ k \in ℕ_{0} \to k - -1 = k + 1$
339	338	oveq1d	$⊢ k \in ℕ_{0} \to k - -1 - 1 = k + 1 - 1$
340	336 337	pncand	$⊢ k \in ℕ_{0} \to k + 1 - 1 = k$
341	339 340	eqtrd	$⊢ k \in ℕ_{0} \to k - -1 - 1 = k$
342	341	adantl	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to k - -1 - 1 = k$
343	342	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C - (k - -1 - 1) = C - k$
344	342	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C C_{𝑐} (k - -1 - 1) = C C_{𝑐} k$
345	343 344	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) = (C - k) (C C_{𝑐} k)$
346	342	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to b^{k - -1 - 1} = b^{k}$
347	345 346	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) b^{k - -1 - 1} = (C - k) (C C_{𝑐} k) b^{k}$
348	347	mpteq2dva	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (k \in ℕ_{0} ⟼ (C - (k - -1 - 1)) (C C_{𝑐} (k - -1 - 1)) b^{k - -1 - 1}) = (k \in ℕ_{0} ⟼ (C - k) (C C_{𝑐} k) b^{k})$
349	335 348	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to E (b) shift -1 = (k \in ℕ_{0} ⟼ (C - k) (C C_{𝑐} k) b^{k})$
350		ovexd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - k) (C C_{𝑐} k) b^{k} \in V$
351	349 350	fvmpt2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (E (b) shift -1) (k) = (C - k) (C C_{𝑐} k) b^{k}$
352	242 351	sylan2	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (E (b) shift -1) (k) = (C - k) (C C_{𝑐} k) b^{k}$
353	336	adantl	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to k \in ℂ$
354	245 353	subcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C - k \in ℂ$
355	354 247	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - k) (C C_{𝑐} k) \in ℂ$
356	355 251	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - k) (C C_{𝑐} k) b^{k} \in ℂ$
357	242 356	sylan2	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - k) (C C_{𝑐} k) b^{k} \in ℂ$
358		fveq2	$⊢ k = j \to E (b) (k) = E (b) (j)$
359	358	oveq2d	$⊢ k = j \to b E (b) (k) = b E (b) (j)$
360	359	cbvmptv	$⊢ (k \in ℕ ⟼ b E (b) (k)) = (j \in ℕ ⟼ b E (b) (j))$
361	309	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b E (b) (k) = b (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
362	249	adantr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b \in ℂ$
363	4	ad3antrrr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to C \in ℂ$
364		nncn	$⊢ k \in ℕ \to k \in ℂ$
365	364	adantl	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to k \in ℂ$
366		1cnd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to 1 \in ℂ$
367	365 366	subcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to k - 1 \in ℂ$
368	363 367	subcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to C - (k - 1) \in ℂ$
369	279	adantl	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to k - 1 \in ℕ_{0}$
370	363 369	bcccl	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to C C_{𝑐} (k - 1) \in ℂ$
371	368 370	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - (k - 1)) (C C_{𝑐} (k - 1)) \in ℂ$
372	362 369	expcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b^{k - 1} \in ℂ$
373	362 371 372	mul12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = (C - (k - 1)) (C C_{𝑐} (k - 1)) b b^{k - 1}$
374	362 372	mulcomd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b b^{k - 1} = b^{k - 1} b$
375	362 369	expp1d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b^{k - 1 + 1} = b^{k - 1} b$
376	285	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to k - 1 + 1 = k$
377	376	adantlr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to k - 1 + 1 = k$
378	377	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b^{k - 1 + 1} = b^{k}$
379	374 375 378	3eqtr2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b b^{k - 1} = b^{k}$
380	379	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - (k - 1)) (C C_{𝑐} (k - 1)) b b^{k - 1} = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
381	373 380	eqtrd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
382	361 381	eqtrd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to b E (b) (k) = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
383	382	mpteq2dva	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (k \in ℕ ⟼ b E (b) (k)) = (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k})$
384	360 383	eqtr3id	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (j \in ℕ ⟼ b E (b) (j)) = (k \in ℕ ⟼ (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k})$
385		ovexd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k} \in V$
386	384 385	fvmpt2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (j \in ℕ ⟼ b E (b) (j)) (k) = (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
387	371 252	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k} \in ℂ$
388		climrel	$⊢ Rel ⇝$
389	157	simprd	$⊢ (φ \land b \in D) \to seq 1 (+ E (b)) \in dom ⇝$
390	389	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 1 (+ E (b)) \in dom ⇝$
391		climdm	$⊢ seq 1 (+ E (b)) \in dom ⇝ \leftrightarrow seq 1 (+ E (b)) ⇝ ⇝ (seq 1 (+ E (b)))$
392	390 391	sylib	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 1 (+ E (b)) ⇝ ⇝ (seq 1 (+ E (b)))$
393		0z	$⊢ 0 \in ℤ$
394		neg1z	$⊢ - 1 \in ℤ$
395		fvex	$⊢ E (b) \in V$
396	395	seqshft	$⊢ (0 \in ℤ \land - 1 \in ℤ) \to seq 0 (+ (E (b) shift -1)) = seq (0 - -1) (+ E (b)) shift -1$
397	393 394 396	mp2an	$⊢ seq 0 (+ (E (b) shift -1)) = seq (0 - -1) (+ E (b)) shift -1$
398		0cn	$⊢ 0 \in ℂ$
399	398 196	subnegi	$⊢ 0 - -1 = 0 + 1$
400		0p1e1	$⊢ 0 + 1 = 1$
401	399 400	eqtri	$⊢ 0 - -1 = 1$
402		seqeq1	$⊢ 0 - -1 = 1 \to seq (0 - -1) (+ E (b)) = seq 1 (+ E (b))$
403	401 402	ax-mp	$⊢ seq (0 - -1) (+ E (b)) = seq 1 (+ E (b))$
404	403	oveq1i	$⊢ seq (0 - -1) (+ E (b)) shift -1 = seq 1 (+ E (b)) shift -1$
405	397 404	eqtri	$⊢ seq 0 (+ (E (b) shift -1)) = seq 1 (+ E (b)) shift -1$
406	405	breq1i	$⊢ seq 0 (+ (E (b) shift -1)) ⇝ ⇝ (seq 1 (+ E (b))) \leftrightarrow (seq 1 (+ E (b)) shift -1) ⇝ ⇝ (seq 1 (+ E (b)))$
407		seqex	$⊢ seq 1 (+ E (b)) \in V$
408		climshft	$⊢ (- 1 \in ℤ \land seq 1 (+ E (b)) \in V) \to ((seq 1 (+ E (b)) shift -1) ⇝ ⇝ (seq 1 (+ E (b))) \leftrightarrow seq 1 (+ E (b)) ⇝ ⇝ (seq 1 (+ E (b))))$
409	394 407 408	mp2an	$⊢ (seq 1 (+ E (b)) shift -1) ⇝ ⇝ (seq 1 (+ E (b))) \leftrightarrow seq 1 (+ E (b)) ⇝ ⇝ (seq 1 (+ E (b)))$
410	406 409	bitri	$⊢ seq 0 (+ (E (b) shift -1)) ⇝ ⇝ (seq 1 (+ E (b))) \leftrightarrow seq 1 (+ E (b)) ⇝ ⇝ (seq 1 (+ E (b)))$
411	392 410	sylibr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 0 (+ (E (b) shift -1)) ⇝ ⇝ (seq 1 (+ E (b)))$
412		releldm	$⊢ (Rel ⇝ \land seq 0 (+ (E (b) shift -1)) ⇝ ⇝ (seq 1 (+ E (b)))) \to seq 0 (+ (E (b) shift -1)) \in dom ⇝$
413	388 411 412	sylancr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 0 (+ (E (b) shift -1)) \in dom ⇝$
414	254	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 \in ℕ_{0}$
415	351 356	eqeltrd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (E (b) shift -1) (k) \in ℂ$
416	113 414 415	iserex	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (seq 0 (+ (E (b) shift -1)) \in dom ⇝ \leftrightarrow seq 1 (+ (E (b) shift -1)) \in dom ⇝)$
417	413 416	mpbid	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 1 (+ (E (b) shift -1)) \in dom ⇝$
418	371 372	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} \in ℂ$
419	309 418	eqeltrd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to E (b) (k) \in ℂ$
420	386 382	eqtr4d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (j \in ℕ ⟼ b E (b) (j)) (k) = b E (b) (k)$
421	240 241 249 392 419 420	isermulc2	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 1 (+ (j \in ℕ ⟼ b E (b) (j))) ⇝ b ⇝ (seq 1 (+ E (b)))$
422		releldm	$⊢ (Rel ⇝ \land seq 1 (+ (j \in ℕ ⟼ b E (b) (j))) ⇝ b ⇝ (seq 1 (+ E (b)))) \to seq 1 (+ (j \in ℕ ⟼ b E (b) (j))) \in dom ⇝$
423	388 421 422	sylancr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to seq 1 (+ (j \in ℕ ⟼ b E (b) (j))) \in dom ⇝$
424	240 241 352 357 386 387 417 423	isumadd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) b^{k} + (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}) = \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
425	424	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C + \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) b^{k} + (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}) = C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
426	363 365	subcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to C - k \in ℂ$
427	426 248	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to (C - k) (C C_{𝑐} k) \in ℂ$
428	427 371 252	adddird	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = (C - k) (C C_{𝑐} k) b^{k} + (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
429	428	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) b^{k} + (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k})$
430	429	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C + \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = C + \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) b^{k} + (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k})$
431	307	sumeq2dv	$⊢ (φ \land b \in ℂ) \to \sum_{k \in ℕ} E (b) (k) = \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
432	431	oveq2d	$⊢ (φ \land b \in ℂ) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = (1 + b) \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
433	120 432	sylan2	$⊢ (φ \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = (1 + b) \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
434	433	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = (1 + b) \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
435	240 241 309 418 390	isumcl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} \in ℂ$
436	239 249 435	adddird	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = 1 \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} + b \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
437	435	mulid2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
438	240 241 309 418 390 249	isummulc2	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to b \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{k \in ℕ} b (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1}$
439	381	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} b (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
440	438 439	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to b \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
441	437 440	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} + b \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
442	434 436 441	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
443	400	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
444	240 443	eqtr4i	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
445		oveq1	$⊢ k = 1 + j \to k - 1 = 1 + j - 1$
446	445	oveq2d	$⊢ k = 1 + j \to C - (k - 1) = C - (1 + j - 1)$
447	445	oveq2d	$⊢ k = 1 + j \to C C_{𝑐} (k - 1) = C C_{𝑐} (1 + j - 1)$
448	446 447	oveq12d	$⊢ k = 1 + j \to (C - (k - 1)) (C C_{𝑐} (k - 1)) = (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1))$
449	445	oveq2d	$⊢ k = 1 + j \to b^{k - 1} = b^{1 + j - 1}$
450	448 449	oveq12d	$⊢ k = 1 + j \to (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1)) b^{1 + j - 1}$
451	113 444 450 241 114 418	isumshft	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{j \in ℕ_{0}} (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1)) b^{1 + j - 1}$
452		oveq2	$⊢ j = k \to 1 + j = 1 + k$
453	452	oveq1d	$⊢ j = k \to 1 + j - 1 = 1 + k - 1$
454	453	oveq2d	$⊢ j = k \to C - (1 + j - 1) = C - (1 + k - 1)$
455	453	oveq2d	$⊢ j = k \to C C_{𝑐} (1 + j - 1) = C C_{𝑐} (1 + k - 1)$
456	454 455	oveq12d	$⊢ j = k \to (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1)) = (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1))$
457	453	oveq2d	$⊢ j = k \to b^{1 + j - 1} = b^{1 + k - 1}$
458	456 457	oveq12d	$⊢ j = k \to (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1)) b^{1 + j - 1} = (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1)) b^{1 + k - 1}$
459	458	cbvsumv	$⊢ \sum_{j \in ℕ_{0}} (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1)) b^{1 + j - 1} = \sum_{k \in ℕ_{0}} (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1)) b^{1 + k - 1}$
460	459	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{j \in ℕ_{0}} (C - (1 + j - 1)) (C C_{𝑐} (1 + j - 1)) b^{1 + j - 1} = \sum_{k \in ℕ_{0}} (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1)) b^{1 + k - 1}$
461		1cnd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to 1 \in ℂ$
462	461 353	pncan2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to 1 + k - 1 = k$
463	462	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C - (1 + k - 1) = C - k$
464	462	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to C C_{𝑐} (1 + k - 1) = C C_{𝑐} k$
465	463 464	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1)) = (C - k) (C C_{𝑐} k)$
466	462	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to b^{1 + k - 1} = b^{k}$
467	465 466	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1)) b^{1 + k - 1} = (C - k) (C C_{𝑐} k) b^{k}$
468	467	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} (C - (1 + k - 1)) (C C_{𝑐} (1 + k - 1)) b^{1 + k - 1} = \sum_{k \in ℕ_{0}} (C - k) (C C_{𝑐} k) b^{k}$
469	451 460 468	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = \sum_{k \in ℕ_{0}} (C - k) (C C_{𝑐} k) b^{k}$
470	113 114 351 356 413	isum1p	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} (C - k) (C C_{𝑐} k) b^{k} = (E (b) shift -1) (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} (C - k) (C C_{𝑐} k) b^{k}$
471		simpr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to k = 0$
472	471	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to C - k = C - 0$
473	471	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to C C_{𝑐} k = C C_{𝑐} 0$
474	472 473	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to (C - k) (C C_{𝑐} k) = (C - 0) (C C_{𝑐} 0)$
475	471	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to b^{k} = b^{0}$
476	474 475	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to (C - k) (C C_{𝑐} k) b^{k} = (C - 0) (C C_{𝑐} 0) b^{0}$
477		0nn0	$⊢ 0 \in ℕ_{0}$
478	477	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 0 \in ℕ_{0}$
479		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (C - 0) (C C_{𝑐} 0) b^{0} \in V$
480	349 476 478 479	fvmptd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (E (b) shift -1) (0) = (C - 0) (C C_{𝑐} 0) b^{0}$
481	236	subid1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C - 0 = C$
482	236	bccn0	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C C_{𝑐} 0 = 1$
483	481 482	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (C - 0) (C C_{𝑐} 0) = C \cdot 1$
484	483 237	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (C - 0) (C C_{𝑐} 0) = C$
485	249	exp0d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to b^{0} = 1$
486	484 485	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (C - 0) (C C_{𝑐} 0) b^{0} = C \cdot 1$
487	480 486 237	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (E (b) shift -1) (0) = C$
488	444	eqcomi	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
489	488	sumeq1i	$⊢ \sum_{k \in ℤ_{\geq (0 + 1)}} (C - k) (C C_{𝑐} k) b^{k} = \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k}$
490	489	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℤ_{\geq (0 + 1)}} (C - k) (C C_{𝑐} k) b^{k} = \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k}$
491	487 490	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (E (b) shift -1) (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} (C - k) (C C_{𝑐} k) b^{k} = C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k}$
492	469 470 491	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} = C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k}$
493	492	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k} = C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
494	240 241 352 357 417	isumcl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} \in ℂ$
495	249 435	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to b \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k - 1} \in ℂ$
496	440 495	eqeltrrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k} \in ℂ$
497	236 494 496	addassd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k} = C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
498	442 493 497	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = C + \sum_{k \in ℕ} (C - k) (C C_{𝑐} k) b^{k} + \sum_{k \in ℕ} (C - (k - 1)) (C C_{𝑐} (k - 1)) b^{k}$
499	425 430 498	3eqtr4rd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = C + \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k}$
500		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
501	278 500	binomcxplemwb	$⊢ (φ \land k \in ℕ) \to (C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1)) = C (C C_{𝑐} k)$
502	501	oveq1d	$⊢ (φ \land k \in ℕ) \to ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = C (C C_{𝑐} k) b^{k}$
503	502	sumeq2dv	$⊢ φ \to \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k}$
504	503	oveq2d	$⊢ φ \to C + \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = C + \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k}$
505	504	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C + \sum_{k \in ℕ} ((C - k) (C C_{𝑐} k) + (C - (k - 1)) (C C_{𝑐} (k - 1))) b^{k} = C + \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k}$
506	363 248 252	mulassd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to C (C C_{𝑐} k) b^{k} = C (C C_{𝑐} k) b^{k}$
507	506	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k} = \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k}$
508	240 241 244 253 258 236	isummulc2	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k} = \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k}$
509	507 508	eqtr4d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k} = C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
510	509	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C + \sum_{k \in ℕ} C (C C_{𝑐} k) b^{k} = C + C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
511	499 505 510	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = C + C \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
512	238 260 511	3eqtr4rd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = C (1 + \sum_{k \in ℕ} (C C_{𝑐} k) b^{k})$
513	6	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to S = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
514	123	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in ℂ) \to (k \in ℕ_{0} ⟼ F (k) b^{k}) \in V$
515	513 514	fvmpt2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in ℂ) \to S (b) = (k \in ℕ_{0} ⟼ F (k) b^{k})$
516	120 515	sylan2	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to S (b) = (k \in ℕ_{0} ⟼ F (k) b^{k})$
517		ovexd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to F (k) b^{k} \in V$
518	516 517	fvmpt2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to S (b) (k) = F (k) b^{k}$
519	518	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} S (b) (k) = \sum_{k \in ℕ_{0}} F (k) b^{k}$
520	4	adantr	$⊢ (φ \land k \in ℕ_{0}) \to C \in ℂ$
521	520 131	bcccl	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
522	133 521	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℂ$
523	522	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) \in ℂ$
524	523	adantlr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to F (k) \in ℂ$
525	524 251	mulcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ_{0}) \to F (k) b^{k} \in ℂ$
526	113 114 518 525 159	isum1p	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} F (k) b^{k} = S (b) (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} F (k) b^{k}$
527	471	fveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to F (k) = F (0)$
528	527 475	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k = 0) \to F (k) b^{k} = F (0) b^{0}$
529		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to F (0) b^{0} \in V$
530	516 528 478 529	fvmptd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to S (b) (0) = F (0) b^{0}$
531	5	a1i	$⊢ φ \to F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
532		simpr	$⊢ (φ \land j = 0) \to j = 0$
533	532	oveq2d	$⊢ (φ \land j = 0) \to C C_{𝑐} j = C C_{𝑐} 0$
534	477	a1i	$⊢ φ \to 0 \in ℕ_{0}$
535		ovexd	$⊢ φ \to C C_{𝑐} 0 \in V$
536	531 533 534 535	fvmptd	$⊢ φ \to F (0) = C C_{𝑐} 0$
537	536	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to F (0) = C C_{𝑐} 0$
538	537 482	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to F (0) = 1$
539	538 485	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to F (0) b^{0} = 1 \cdot 1$
540	239	mulid1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 \cdot 1 = 1$
541	530 539 540	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to S (b) (0) = 1$
542	488	sumeq1i	$⊢ \sum_{k \in ℤ_{\geq (0 + 1)}} F (k) b^{k} = \sum_{k \in ℕ} F (k) b^{k}$
543	134	adantlr	$⊢ ((φ \land b \in D) \land k \in ℕ_{0}) \to F (k) b^{k} = (C C_{𝑐} k) b^{k}$
544	242 543	sylan2	$⊢ ((φ \land b \in D) \land k \in ℕ) \to F (k) b^{k} = (C C_{𝑐} k) b^{k}$
545	544	adantllr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to F (k) b^{k} = (C C_{𝑐} k) b^{k}$
546	545	sumeq2dv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} F (k) b^{k} = \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
547	542 546	syl5eq	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℤ_{\geq (0 + 1)}} F (k) b^{k} = \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
548	541 547	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to S (b) (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} F (k) b^{k} = 1 + \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}$
549	519 526 548	3eqtrrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 + \sum_{k \in ℕ} (C C_{𝑐} k) b^{k} = \sum_{k \in ℕ_{0}} S (b) (k)$
550	549	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C (1 + \sum_{k \in ℕ} (C C_{𝑐} k) b^{k}) = C \sum_{k \in ℕ_{0}} S (b) (k)$
551	512 550	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (1 + b) \sum_{k \in ℕ} E (b) (k) = C \sum_{k \in ℕ_{0}} S (b) (k)$
552	236 160	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C \sum_{k \in ℕ_{0}} S (b) (k) \in ℂ$
553	239 249	addcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 + b \in ℂ$
554		eqidd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b \in D) \land k \in ℕ) \to E (b) (k) = E (b) (k)$
555	240 241 554 419 390	isumcl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} E (b) (k) \in ℂ$
556	239 249	subnegd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 - (- b) = 1 + b$
557	249	negcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to - b \in ℂ$
558		elpreima	$⊢ abs Fn ℂ \to (b \in {abs}^{-1} [[0, R)] \leftrightarrow (b \in ℂ \land \|b\| \in [0, R)))$
559	87 88 558	mp2b	$⊢ b \in {abs}^{-1} [[0, R)] \leftrightarrow (b \in ℂ \land \|b\| \in [0, R))$
560	559	simprbi	$⊢ b \in {abs}^{-1} [[0, R)] \to \|b\| \in [0, R)$
561	560 9	eleq2s	$⊢ b \in D \to \|b\| \in [0, R)$
562		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|b\| \in [0, R) \leftrightarrow (\|b\| \in ℝ \land 0 \leq \|b\| \land \|b\| < R))$
563	76 82 562	mp2an	$⊢ \|b\| \in [0, R) \leftrightarrow (\|b\| \in ℝ \land 0 \leq \|b\| \land \|b\| < R)$
564	563	simp3bi	$⊢ \|b\| \in [0, R) \to \|b\| < R$
565	561 564	syl	$⊢ b \in D \to \|b\| < R$
566	565	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \|b\| < R$
567	249	absnegd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \|- b\| = \|b\|$
568	567	eqcomd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \|b\| = \|- b\|$
569	74	adantr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to R = 1$
570	566 568 569	3brtr3d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \|- b\| < 1$
571		1re	$⊢ 1 \in ℝ$
572		abssubne0	$⊢ (- b \in ℂ \land 1 \in ℝ \land \|- b\| < 1) \to 1 - (- b) \neq 0$
573	571 572	mp3an2	$⊢ (- b \in ℂ \land \|- b\| < 1) \to 1 - (- b) \neq 0$
574	557 570 573	syl2anc	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 - (- b) \neq 0$
575	556 574	eqnetrrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 + b \neq 0$
576	552 553 555 575	divmuld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C \sum_{k \in ℕ_{0}} S (b) (k)}{1 + b} = \sum_{k \in ℕ} E (b) (k) \leftrightarrow (1 + b) \sum_{k \in ℕ} E (b) (k) = C \sum_{k \in ℕ_{0}} S (b) (k))$
577	551 576	mpbird	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{C \sum_{k \in ℕ_{0}} S (b) (k)}{1 + b} = \sum_{k \in ℕ} E (b) (k)$
578	236 160 553 575	div23d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{C \sum_{k \in ℕ_{0}} S (b) (k)}{1 + b} = (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k)$
579	577 578	eqtr3d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ} E (b) (k) = (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k)$
580	579	mpteq2dva	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ \sum_{k \in ℕ} E (b) (k)) = (b \in D ⟼ (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k))$
581		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{C}{1 + b} \in V$
582		sumex	$⊢ \sum_{k \in ℕ_{0}} S (b) (k) \in V$
583	582	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \sum_{k \in ℕ_{0}} S (b) (k) \in V$
584		eqidd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ \frac{C}{1 + b}) = (b \in D ⟼ \frac{C}{1 + b})$
585	10	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to P = (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k))$
586	104 29 183 581 583 584 585	offval2f	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ \frac{C}{1 + b}) \times_{f} P = (b \in D ⟼ (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k))$
587	580 205 586	3eqtr4d	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D P = (b \in D ⟼ \frac{C}{1 + b}) \times_{f} P$
588	587	oveq1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to P_{ℂ}^{'} \times_{f} (b \in D ⟼ {(1 + b)}^{- C}) = ((b \in D ⟼ \frac{C}{1 + b}) \times_{f} P) \times_{f} (b \in D ⟼ {(1 + b)}^{- C})$
589	223	oveq1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} \times_{f} P = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1}) \times_{f} P$
590	588 589	oveq12d	$⊢ (φ \land \neg C \in ℕ_{0}) \to (P_{ℂ}^{'} \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) +_{f} (\frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} \times_{f} P) = (((b \in D ⟼ \frac{C}{1 + b}) \times_{f} P) \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) +_{f} ((b \in D ⟼ (- C) {(1 + b)}^{- C - 1}) \times_{f} P)$
591		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} \in V$
592		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) \in V$
593		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) \in V$
594		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{- C} \in V$
595		eqidd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ {(1 + b)}^{- C}) = (b \in D ⟼ {(1 + b)}^{- C})$
596	104 29 183 593 594 586 595	offval2f	$⊢ (φ \land \neg C \in ℕ_{0}) \to ((b \in D ⟼ \frac{C}{1 + b}) \times_{f} P) \times_{f} (b \in D ⟼ {(1 + b)}^{- C}) = (b \in D ⟼ (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C})$
597		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (- C) {(1 + b)}^{- C - 1} \in V$
598		eqidd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ (- C) {(1 + b)}^{- C - 1}) = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$
599	104 29 183 597 583 598 585	offval2f	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ (- C) {(1 + b)}^{- C - 1}) \times_{f} P = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k))$
600	104 29 183 591 592 596 599	offval2f	$⊢ (φ \land \neg C \in ℕ_{0}) \to (((b \in D ⟼ \frac{C}{1 + b}) \times_{f} P) \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) +_{f} ((b \in D ⟼ (- C) {(1 + b)}^{- C - 1}) \times_{f} P) = (b \in D ⟼ (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} + (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k))$
601	235 590 600	3eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) = (b \in D ⟼ (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} + (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k))$
602	236 553 575	divcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{C}{1 + b} \in ℂ$
603	236	negcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to - C \in ℂ$
604	553 603	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{- C} \in ℂ$
605	602 160 604	mul32d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} = (\frac{C}{1 + b}) {(1 + b)}^{- C} \sum_{k \in ℕ_{0}} S (b) (k)$
606	236 553 604 575	div32d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) {(1 + b)}^{- C} = C (\frac{{(1 + b)}^{- C}}{1 + b})$
607	553 575 603 239	cxpsubd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{- C - 1} = \frac{{(1 + b)}^{- C}}{{(1 + b)}^{1}}$
608	553	cxp1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{1} = 1 + b$
609	608	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{{(1 + b)}^{- C}}{{(1 + b)}^{1}} = \frac{{(1 + b)}^{- C}}{1 + b}$
610	607 609	eqtr2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{{(1 + b)}^{- C}}{1 + b} = {(1 + b)}^{- C - 1}$
611	610	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C (\frac{{(1 + b)}^{- C}}{1 + b}) = C {(1 + b)}^{- C - 1}$
612	606 611	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) {(1 + b)}^{- C} = C {(1 + b)}^{- C - 1}$
613	612	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) {(1 + b)}^{- C} \sum_{k \in ℕ_{0}} S (b) (k) = C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k)$
614	605 613	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} = C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k)$
615	603 239	subcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to - C - 1 \in ℂ$
616	553 615	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{- C - 1} \in ℂ$
617	236 616	mulneg1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (- C) {(1 + b)}^{- C - 1} = - C {(1 + b)}^{- C - 1}$
618	617	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) = (- C {(1 + b)}^{- C - 1}) \sum_{k \in ℕ_{0}} S (b) (k)$
619	236 616	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C {(1 + b)}^{- C - 1} \in ℂ$
620	619 160	mulneg1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (- C {(1 + b)}^{- C - 1}) \sum_{k \in ℕ_{0}} S (b) (k) = - C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k)$
621	618 620	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) = - C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k)$
622	614 621	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} + (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) = C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) + (- C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k))$
623	619 160	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) \in ℂ$
624	623	negidd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) + (- C {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k)) = 0$
625	622 624	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} + (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k) = 0$
626	625	mpteq2dva	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ (\frac{C}{1 + b}) \sum_{k \in ℕ_{0}} S (b) (k) {(1 + b)}^{- C} + (- C) {(1 + b)}^{- C - 1} \sum_{k \in ℕ_{0}} S (b) (k)) = (b \in D ⟼ 0)$
627	601 626	eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) = (b \in D ⟼ 0)$
628		nfcv	$⊢ \underline{Ⅎ} x 0$
629		eqidd	$⊢ x = b \to 0 = 0$
630	30 29 12 628 629	cbvmptf	$⊢ (x \in D ⟼ 0) = (b \in D ⟼ 0)$
631	627 630	eqtr4di	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) = (x \in D ⟼ 0)$
632		c0ex	$⊢ 0 \in V$
633	632	snid	$⊢ 0 \in \{0\}$
634	633	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to 0 \in \{0\}$
635	631 634	fmpt3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(P \times_{f} (b \in D ⟼ {(1 + b)}^{- C}))}_{ℂ}^{'} : D ⟶ \{0\}$
636	635	fdmd	$⊢ (φ \land \neg C \in ℕ_{0}) \to dom {(P \times_{f} (b \in D ⟼ {(1 + b)}^{- C}))}_{ℂ}^{'} = D$
637		1cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in ℂ) \to 1 \in ℂ$
638		0cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in ℂ) \to 0 \in ℂ$
639		dvconst	$⊢ 1 \in ℂ \to ℂ D (ℂ \times \{1\}) = ℂ \times \{0\}$
640	196 639	ax-mp	$⊢ ℂ D (ℂ \times \{1\}) = ℂ \times \{0\}$
641		fconstmpt	$⊢ ℂ \times \{1\} = (x \in ℂ ⟼ 1)$
642	641	oveq2i	$⊢ ℂ D (ℂ \times \{1\}) = \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x}$
643		fconstmpt	$⊢ ℂ \times \{0\} = (x \in ℂ ⟼ 0)$
644	640 642 643	3eqtr3i	$⊢ \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
645	644	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
646	119	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to D \subseteq ℂ$
647		fvex	$⊢ TopOpen (ℂ_{fld}) \in V$
648		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
649		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
650		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
651	649 650	tpsuni	$⊢ ℂ_{fld} \in TopSp \to ℂ = ⋃ TopOpen (ℂ_{fld})$
652	648 651	ax-mp	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
653	652	restid	$⊢ TopOpen (ℂ_{fld}) \in V \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
654	647 653	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
655	654	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
656	650	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
657		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
658	650	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
659	658	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land R \in ℝ^{*}) \to 0 ball (abs \circ -) R \in TopOpen (ℂ_{fld})$
660	657 398 82 659	mp3an	$⊢ 0 ball (abs \circ -) R \in TopOpen (ℂ_{fld})$
661	99 660	eqeltri	$⊢ D \in TopOpen (ℂ_{fld})$
662		isopn3i	$⊢ (TopOpen (ℂ_{fld}) \in Top \land D \in TopOpen (ℂ_{fld})) \to int (TopOpen (ℂ_{fld})) (D) = D$
663	656 661 662	mp2an	$⊢ int (TopOpen (ℂ_{fld})) (D) = D$
664	663	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to int (TopOpen (ℂ_{fld})) (D) = D$
665	203 637 638 645 646 655 650 664	dvmptres2	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in D⟼ 1)}{d_{ℂ} x} = (x \in D ⟼ 0)$
666	192	oveq2i	$⊢ \frac{d (x \in D⟼ 1)}{d_{ℂ} x} = \frac{d (b \in D⟼ 1)}{d_{ℂ} b}$
667	665 666 630	3eqtr3g	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ 1)}{d_{ℂ} b} = (b \in D ⟼ 0)$
668	626 601 667	3eqtr4d	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ D (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) = \frac{d (b \in D⟼ 1)}{d_{ℂ} b}$
669		1rp	$⊢ 1 \in ℝ^{+}$
670	74 669	eqeltrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to R \in ℝ^{+}$
671		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land R \in ℝ^{+}) \to 0 \in (0 ball (abs \circ -) R)$
672	657 398 671	mp3an12	$⊢ R \in ℝ^{+} \to 0 \in (0 ball (abs \circ -) R)$
673	670 672	syl	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \in (0 ball (abs \circ -) R)$
674	673 99	eleqtrrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \in D$
675		0zd	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \in ℤ$
676		eqidd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to S (0) (k) = S (0) (k)$
677		nfv	$⊢ Ⅎ b φ$
678	29	nfel2	$⊢ Ⅎ b 0 \in D$
679	677 678	nfan	$⊢ Ⅎ b (φ \land 0 \in D)$
680		nfv	$⊢ Ⅎ b k \in ℕ_{0}$
681	679 680	nfan	$⊢ Ⅎ b ((φ \land 0 \in D) \land k \in ℕ_{0})$
682	16 12	nffv	$⊢ \underline{Ⅎ} b S (0)$
683	682 35	nffv	$⊢ \underline{Ⅎ} b S (0) (k)$
684	683	nfel1	$⊢ Ⅎ b S (0) (k) \in ℂ$
685	681 684	nfim	$⊢ Ⅎ b (((φ \land 0 \in D) \land k \in ℕ_{0}) \to S (0) (k) \in ℂ)$
686		eleq1	$⊢ b = 0 \to (b \in D \leftrightarrow 0 \in D)$
687	686	anbi2d	$⊢ b = 0 \to ((φ \land b \in D) \leftrightarrow (φ \land 0 \in D))$
688	687	anbi1d	$⊢ b = 0 \to (((φ \land b \in D) \land k \in ℕ_{0}) \leftrightarrow ((φ \land 0 \in D) \land k \in ℕ_{0}))$
689		fveq2	$⊢ b = 0 \to S (b) = S (0)$
690	689	fveq1d	$⊢ b = 0 \to S (b) (k) = S (0) (k)$
691	690	eleq1d	$⊢ b = 0 \to (S (b) (k) \in ℂ \leftrightarrow S (0) (k) \in ℂ)$
692	688 691	imbi12d	$⊢ b = 0 \to ((((φ \land b \in D) \land k \in ℕ_{0}) \to S (b) (k) \in ℂ) \leftrightarrow (((φ \land 0 \in D) \land k \in ℕ_{0}) \to S (0) (k) \in ℂ))$
693	685 632 692 144	vtoclf	$⊢ ((φ \land 0 \in D) \land k \in ℕ_{0}) \to S (0) (k) \in ℂ$
694	674 693	syldanl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to S (0) (k) \in ℂ$
695	12 14 682	nfseq	$⊢ \underline{Ⅎ} b seq 0 (+ S (0))$
696	695	nfel1	$⊢ Ⅎ b seq 0 (+ S (0)) \in dom ⇝$
697	679 696	nfim	$⊢ Ⅎ b ((φ \land 0 \in D) \to seq 0 (+ S (0)) \in dom ⇝)$
698	689	seqeq3d	$⊢ b = 0 \to seq 0 (+ S (b)) = seq 0 (+ S (0))$
699	698	eleq1d	$⊢ b = 0 \to (seq 0 (+ S (b)) \in dom ⇝ \leftrightarrow seq 0 (+ S (0)) \in dom ⇝)$
700	687 699	imbi12d	$⊢ b = 0 \to (((φ \land b \in D) \to seq 0 (+ S (b)) \in dom ⇝) \leftrightarrow ((φ \land 0 \in D) \to seq 0 (+ S (0)) \in dom ⇝))$
701	697 632 700 158	vtoclf	$⊢ (φ \land 0 \in D) \to seq 0 (+ S (0)) \in dom ⇝$
702	674 701	syldan	$⊢ (φ \land \neg C \in ℕ_{0}) \to seq 0 (+ S (0)) \in dom ⇝$
703	113 675 676 694 702	isum1p	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} S (0) (k) = S (0) (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} S (0) (k)$
704	133	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
705	704	adantlr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = 0) \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
706		simplr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = 0) \land k \in ℕ_{0}) \to b = 0$
707	706	oveq1d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = 0) \land k \in ℕ_{0}) \to b^{k} = 0^{k}$
708	705 707	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = 0) \land k \in ℕ_{0}) \to F (k) b^{k} = (C C_{𝑐} k) 0^{k}$
709	708	mpteq2dva	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b = 0) \to (k \in ℕ_{0} ⟼ F (k) b^{k}) = (k \in ℕ_{0} ⟼ (C C_{𝑐} k) 0^{k})$
710	122	mptex	$⊢ (k \in ℕ_{0} ⟼ (C C_{𝑐} k) 0^{k}) \in V$
711	710	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (C C_{𝑐} k) 0^{k}) \in V$
712	513 709 100 711	fvmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to S (0) = (k \in ℕ_{0} ⟼ (C C_{𝑐} k) 0^{k})$
713		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k = 0) \to k = 0$
714	713	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k = 0) \to C C_{𝑐} k = C C_{𝑐} 0$
715	713	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k = 0) \to 0^{k} = 0^{0}$
716	714 715	oveq12d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k = 0) \to (C C_{𝑐} k) 0^{k} = (C C_{𝑐} 0) 0^{0}$
717	477	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \in ℕ_{0}$
718		ovexd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (C C_{𝑐} 0) 0^{0} \in V$
719	712 716 717 718	fvmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to S (0) (0) = (C C_{𝑐} 0) 0^{0}$
720	4	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to C \in ℂ$
721	720	bccn0	$⊢ (φ \land \neg C \in ℕ_{0}) \to C C_{𝑐} 0 = 1$
722	100	exp0d	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0^{0} = 1$
723	721 722	oveq12d	$⊢ (φ \land \neg C \in ℕ_{0}) \to (C C_{𝑐} 0) 0^{0} = 1 \cdot 1$
724		1t1e1	$⊢ 1 \cdot 1 = 1$
725	724	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 \cdot 1 = 1$
726	719 723 725	3eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to S (0) (0) = 1$
727		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) 0^{k} \in V$
728	712 727	fvmpt2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to S (0) (k) = (C C_{𝑐} k) 0^{k}$
729	242 728	sylan2	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to S (0) (k) = (C C_{𝑐} k) 0^{k}$
730		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to k \in ℕ$
731	730	0expd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to 0^{k} = 0$
732	731	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to (C C_{𝑐} k) 0^{k} = (C C_{𝑐} k) \cdot 0$
733	521	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
734	242 733	sylan2	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to C C_{𝑐} k \in ℂ$
735	734	mul01d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to (C C_{𝑐} k) \cdot 0 = 0$
736	729 732 735	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ) \to S (0) (k) = 0$
737	736	sumeq2dv	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ} S (0) (k) = \sum_{k \in ℕ} 0$
738	444	sumeq1i	$⊢ \sum_{k \in ℕ} S (0) (k) = \sum_{k \in ℤ_{\geq (0 + 1)}} S (0) (k)$
739	240	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
740	739	orci	$⊢ (ℕ \subseteq ℤ_{\geq 1} \lor ℕ \in Fin)$
741		sumz	$⊢ (ℕ \subseteq ℤ_{\geq 1} \lor ℕ \in Fin) \to \sum_{k \in ℕ} 0 = 0$
742	740 741	ax-mp	$⊢ \sum_{k \in ℕ} 0 = 0$
743	737 738 742	3eqtr3g	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq (0 + 1)}} S (0) (k) = 0$
744	726 743	oveq12d	$⊢ (φ \land \neg C \in ℕ_{0}) \to S (0) (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} S (0) (k) = 1 + 0$
745	703 744	eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} S (0) (k) = 1 + 0$
746		1p0e1	$⊢ 1 + 0 = 1$
747	746	oveq1i	$⊢ {(1 + 0)}^{- C} = 1^{- C}$
748	720	negcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to - C \in ℂ$
749	748	1cxpd	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1^{- C} = 1$
750	747 749	syl5eq	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + 0)}^{- C} = 1$
751	745 750	oveq12d	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} S (0) (k) {(1 + 0)}^{- C} = (1 + 0) \cdot 1$
752	746	oveq1i	$⊢ (1 + 0) \cdot 1 = 1 \cdot 1$
753	752 724	eqtri	$⊢ (1 + 0) \cdot 1 = 1$
754	751 753	eqtrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} S (0) (k) {(1 + 0)}^{- C} = 1$
755	162	ffnd	$⊢ (φ \land \neg C \in ℕ_{0}) \to P Fn D$
756	175	ffnd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ {(1 + b)}^{- C}) Fn D$
757	43	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to P = (x \in D ⟼ \sum_{k \in ℕ_{0}} S (x) (k))$
758		simplr	$⊢ ((((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \land k \in ℕ_{0}) \to x = 0$
759	758	fveq2d	$⊢ ((((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \land k \in ℕ_{0}) \to S (x) = S (0)$
760	759	fveq1d	$⊢ ((((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \land k \in ℕ_{0}) \to S (x) (k) = S (0) (k)$
761	760	sumeq2dv	$⊢ (((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \to \sum_{k \in ℕ_{0}} S (x) (k) = \sum_{k \in ℕ_{0}} S (0) (k)$
762		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to 0 \in D$
763		sumex	$⊢ \sum_{k \in ℕ_{0}} S (0) (k) \in V$
764	763	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to \sum_{k \in ℕ_{0}} S (0) (k) \in V$
765	757 761 762 764	fvmptd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to P (0) = \sum_{k \in ℕ_{0}} S (0) (k)$
766	174	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to (b \in D ⟼ {(1 + b)}^{- C}) = (x \in D ⟼ {(1 + x)}^{- C})$
767		simpr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \to x = 0$
768	767	oveq2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \to 1 + x = 1 + 0$
769	768	oveq1d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \land x = 0) \to {(1 + x)}^{- C} = {(1 + 0)}^{- C}$
770		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to {(1 + 0)}^{- C} \in V$
771	766 769 762 770	fvmptd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to (b \in D ⟼ {(1 + b)}^{- C}) (0) = {(1 + 0)}^{- C}$
772	755 756 183 183 184 765 771	ofval	$⊢ ((φ \land \neg C \in ℕ_{0}) \land 0 \in D) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) (0) = \sum_{k \in ℕ_{0}} S (0) (k) {(1 + 0)}^{- C}$
773	674 772	mpdan	$⊢ (φ \land \neg C \in ℕ_{0}) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) (0) = \sum_{k \in ℕ_{0}} S (0) (k) {(1 + 0)}^{- C}$
774	193	fveq1i	$⊢ (D \times \{1\}) (0) = (b \in D ⟼ 1) (0)$
775	186	fvconst2	$⊢ 0 \in D \to (D \times \{1\}) (0) = 1$
776	674 775	syl	$⊢ (φ \land \neg C \in ℕ_{0}) \to (D \times \{1\}) (0) = 1$
777	774 776	eqtr3id	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ 1) (0) = 1$
778	754 773 777	3eqtr4d	$⊢ (φ \land \neg C \in ℕ_{0}) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) (0) = (b \in D ⟼ 1) (0)$
779	99 100 101 185 201 636 668 674 778	dv11cn	$⊢ (φ \land \neg C \in ℕ_{0}) \to P \times_{f} (b \in D ⟼ {(1 + b)}^{- C}) = (b \in D ⟼ 1)$
780	779	oveq1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) \div_{f} (b \in D ⟼ {(1 + b)}^{- C}) = (b \in D ⟼ 1) \div_{f} (b \in D ⟼ {(1 + b)}^{- C})$
781		nfv	$⊢ Ⅎ b 1 + x \neq 0$
782	106 781	nfim	$⊢ Ⅎ b (((φ \land \neg C \in ℕ_{0}) \land x \in D) \to 1 + x \neq 0)$
783	172	neeq1d	$⊢ b = x \to (1 + b \neq 0 \leftrightarrow 1 + x \neq 0)$
784	110 783	imbi12d	$⊢ b = x \to ((((φ \land \neg C \in ℕ_{0}) \land b \in D) \to 1 + b \neq 0) \leftrightarrow (((φ \land \neg C \in ℕ_{0}) \land x \in D) \to 1 + x \neq 0))$
785	782 784 575	chvarfv	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to 1 + x \neq 0$
786	166 785 168	cxpne0d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to {(1 + x)}^{- C} \neq 0$
787		eldifsn	$⊢ {(1 + x)}^{- C} \in (ℂ ∖ \{0\}) \leftrightarrow ({(1 + x)}^{- C} \in ℂ \land {(1 + x)}^{- C} \neq 0)$
788	169 786 787	sylanbrc	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in D) \to {(1 + x)}^{- C} \in (ℂ ∖ \{0\})$
789	788 174	fmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ {(1 + b)}^{- C}) : D ⟶ ℂ ∖ \{0\}$
790		ofdivcan4	$⊢ (D \in V \land P : D ⟶ ℂ \land (b \in D ⟼ {(1 + b)}^{- C}) : D ⟶ ℂ ∖ \{0\}) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) \div_{f} (b \in D ⟼ {(1 + b)}^{- C}) = P$
791	183 162 789 790	syl3anc	$⊢ (φ \land \neg C \in ℕ_{0}) \to (P \times_{f} (b \in D ⟼ {(1 + b)}^{- C})) \div_{f} (b \in D ⟼ {(1 + b)}^{- C}) = P$
792		eqidd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ 1) = (b \in D ⟼ 1)$
793	104 29 183 239 604 792 595	offval2f	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ 1) \div_{f} (b \in D ⟼ {(1 + b)}^{- C}) = (b \in D ⟼ \frac{1}{{(1 + b)}^{- C}})$
794	780 791 793	3eqtr3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to P = (b \in D ⟼ \frac{1}{{(1 + b)}^{- C}})$
795	553 575 603	cxpnegd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{- (- C)} = \frac{1}{{(1 + b)}^{- C}}$
796	236	negnegd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to - (- C) = C$
797	796	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to {(1 + b)}^{- (- C)} = {(1 + b)}^{C}$
798	795 797	eqtr3d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b \in D) \to \frac{1}{{(1 + b)}^{- C}} = {(1 + b)}^{C}$
799	798	mpteq2dva	$⊢ (φ \land \neg C \in ℕ_{0}) \to (b \in D ⟼ \frac{1}{{(1 + b)}^{- C}}) = (b \in D ⟼ {(1 + b)}^{C})$
800	794 799	eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to P = (b \in D ⟼ {(1 + b)}^{C})$
801		nfcv	$⊢ \underline{Ⅎ} x {(1 + b)}^{C}$
802		nfcv	$⊢ \underline{Ⅎ} b {(1 + x)}^{C}$
803	172	oveq1d	$⊢ b = x \to {(1 + b)}^{C} = {(1 + x)}^{C}$
804	29 30 801 802 803	cbvmptf	$⊢ (b \in D ⟼ {(1 + b)}^{C}) = (x \in D ⟼ {(1 + x)}^{C})$
805	800 804	eqtrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to P = (x \in D ⟼ {(1 + x)}^{C})$
806		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \to x = \frac{B}{A}$
807	806	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \to 1 + x = 1 + (\frac{B}{A})$
808	807	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x = \frac{B}{A}) \to {(1 + x)}^{C} = {(1 + (\frac{B}{A}))}^{C}$
809		1cnd	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 \in ℂ$
810	809 63	addcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 + (\frac{B}{A}) \in ℂ$
811	810 720	cxpcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + (\frac{B}{A}))}^{C} \in ℂ$
812	805 808 92 811	fvmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to P (\frac{B}{A}) = {(1 + (\frac{B}{A}))}^{C}$
813	704	adantlr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = \frac{B}{A}) \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
814		simplr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = \frac{B}{A}) \land k \in ℕ_{0}) \to b = \frac{B}{A}$
815	814	oveq1d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = \frac{B}{A}) \land k \in ℕ_{0}) \to b^{k} = {(\frac{B}{A})}^{k}$
816	813 815	oveq12d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land b = \frac{B}{A}) \land k \in ℕ_{0}) \to F (k) b^{k} = (C C_{𝑐} k) {(\frac{B}{A})}^{k}$
817	816	mpteq2dva	$⊢ ((φ \land \neg C \in ℕ_{0}) \land b = \frac{B}{A}) \to (k \in ℕ_{0} ⟼ F (k) b^{k}) = (k \in ℕ_{0} ⟼ (C C_{𝑐} k) {(\frac{B}{A})}^{k})$
818	122	mptex	$⊢ (k \in ℕ_{0} ⟼ (C C_{𝑐} k) {(\frac{B}{A})}^{k}) \in V$
819	818	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (C C_{𝑐} k) {(\frac{B}{A})}^{k}) \in V$
820	513 817 63 819	fvmptd	$⊢ (φ \land \neg C \in ℕ_{0}) \to S (\frac{B}{A}) = (k \in ℕ_{0} ⟼ (C C_{𝑐} k) {(\frac{B}{A})}^{k})$
821		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} \in V$
822	820 821	fvmpt2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to S (\frac{B}{A}) (k) = (C C_{𝑐} k) {(\frac{B}{A})}^{k}$
823	822	sumeq2dv	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} S (\frac{B}{A}) (k) = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k}$
824	95 812 823	3eqtr3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + (\frac{B}{A}))}^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k}$
825	824	oveq1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + (\frac{B}{A}))}^{C} A^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C}$
826	2 1	rerpdivcld	$⊢ φ \to \frac{B}{A} \in ℝ$
827	826	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{B}{A} \in ℝ$
828	69 827	readdcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 + (\frac{B}{A}) \in ℝ$
829		df-neg	$⊢ - \frac{B}{A} = 0 - (\frac{B}{A})$
830	826	recnd	$⊢ φ \to \frac{B}{A} \in ℂ$
831	830	negcld	$⊢ φ \to - \frac{B}{A} \in ℂ$
832	831	abscld	$⊢ φ \to \|- \frac{B}{A}\| \in ℝ$
833		1red	$⊢ φ \to 1 \in ℝ$
834	830	absnegd	$⊢ φ \to \|- \frac{B}{A}\| = \|\frac{B}{A}\|$
835	1	rpne0d	$⊢ φ \to A \neq 0$
836	49 51 835	absdivd	$⊢ φ \to \|\frac{B}{A}\| = \frac{\|B\|}{\|A\|}$
837	834 836	eqtrd	$⊢ φ \to \|- \frac{B}{A}\| = \frac{\|B\|}{\|A\|}$
838	49	abscld	$⊢ φ \to \|B\| \in ℝ$
839	669	a1i	$⊢ φ \to 1 \in ℝ^{+}$
840	51 835	absrpcld	$⊢ φ \to \|A\| \in ℝ^{+}$
841	838	recnd	$⊢ φ \to \|B\| \in ℂ$
842	841	div1d	$⊢ φ \to \frac{\|B\|}{1} = \|B\|$
843	842 3	eqbrtrd	$⊢ φ \to \frac{\|B\|}{1} < \|A\|$
844	838 839 840 843	ltdiv23d	$⊢ φ \to \frac{\|B\|}{\|A\|} < 1$
845	837 844	eqbrtrd	$⊢ φ \to \|- \frac{B}{A}\| < 1$
846	832 833 845	ltled	$⊢ φ \to \|- \frac{B}{A}\| \leq 1$
847	826	renegcld	$⊢ φ \to - \frac{B}{A} \in ℝ$
848	847 833	absled	$⊢ φ \to (\|- \frac{B}{A}\| \leq 1 \leftrightarrow (- 1 \leq - \frac{B}{A} \land - \frac{B}{A} \leq 1))$
849	846 848	mpbid	$⊢ φ \to (- 1 \leq - \frac{B}{A} \land - \frac{B}{A} \leq 1)$
850	849	simprd	$⊢ φ \to - \frac{B}{A} \leq 1$
851	829 850	eqbrtrrid	$⊢ φ \to 0 - (\frac{B}{A}) \leq 1$
852		0red	$⊢ φ \to 0 \in ℝ$
853	852 826 833	lesubaddd	$⊢ φ \to (0 - (\frac{B}{A}) \leq 1 \leftrightarrow 0 \leq 1 + (\frac{B}{A}))$
854	851 853	mpbid	$⊢ φ \to 0 \leq 1 + (\frac{B}{A})$
855	854	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \leq 1 + (\frac{B}{A})$
856	1	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to A \in ℝ^{+}$
857	856	rpred	$⊢ (φ \land \neg C \in ℕ_{0}) \to A \in ℝ$
858	856	rpge0d	$⊢ (φ \land \neg C \in ℕ_{0}) \to 0 \leq A$
859	828 855 857 858 720	mulcxpd	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + (\frac{B}{A})) A}^{C} = {(1 + (\frac{B}{A}))}^{C} A^{C}$
860	809 63 52	adddird	$⊢ (φ \land \neg C \in ℕ_{0}) \to (1 + (\frac{B}{A})) A = 1 A + (\frac{B}{A}) A$
861	52	mulid2d	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 A = A$
862	50 52 62	divcan1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to (\frac{B}{A}) A = B$
863	861 862	oveq12d	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 A + (\frac{B}{A}) A = A + B$
864	860 863	eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (1 + (\frac{B}{A})) A = A + B$
865	864	oveq1d	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + (\frac{B}{A})) A}^{C} = {(A + B)}^{C}$
866	859 865	eqtr3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(1 + (\frac{B}{A}))}^{C} A^{C} = {(A + B)}^{C}$
867	63	adantr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{B}{A} \in ℂ$
868		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
869	867 868	expcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {(\frac{B}{A})}^{k} \in ℂ$
870	733 869	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} \in ℂ$
871	1 2 3 4 5 6 7 8 9	binomcxplemcvg	$⊢ (φ \land \frac{B}{A} \in D) \to (seq 0 (+ S (\frac{B}{A})) \in dom ⇝ \land seq 1 (+ E (\frac{B}{A})) \in dom ⇝)$
872	871	simpld	$⊢ (φ \land \frac{B}{A} \in D) \to seq 0 (+ S (\frac{B}{A})) \in dom ⇝$
873	92 872	syldan	$⊢ (φ \land \neg C \in ℕ_{0}) \to seq 0 (+ S (\frac{B}{A})) \in dom ⇝$
874	52 720	cxpcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to A^{C} \in ℂ$
875	113 675 822 870 873 874	isummulc1	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C}$
876	49	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to B \in ℂ$
877	51	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A \in ℂ$
878	835	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A \neq 0$
879	876 877 878	divrecd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{B}{A} = B (\frac{1}{A})$
880	879	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {(\frac{B}{A})}^{k} = {B (\frac{1}{A})}^{k}$
881	877 878	reccld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{1}{A} \in ℂ$
882	876 881 868	mulexpd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {B (\frac{1}{A})}^{k} = B^{k} {(\frac{1}{A})}^{k}$
883	880 882	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {(\frac{B}{A})}^{k} = B^{k} {(\frac{1}{A})}^{k}$
884	883	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} = (C C_{𝑐} k) B^{k} {(\frac{1}{A})}^{k}$
885	876 868	expcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to B^{k} \in ℂ$
886	881 868	expcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {(\frac{1}{A})}^{k} \in ℂ$
887	733 885 886	mulassd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) B^{k} {(\frac{1}{A})}^{k} = (C C_{𝑐} k) B^{k} {(\frac{1}{A})}^{k}$
888	884 887	eqtr4d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} = (C C_{𝑐} k) B^{k} {(\frac{1}{A})}^{k}$
889	888	oveq1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = (C C_{𝑐} k) B^{k} {(\frac{1}{A})}^{k} A^{C}$
890	733 885	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) B^{k} \in ℂ$
891	874	adantr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C} \in ℂ$
892	890 886 891	mul32d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) B^{k} {(\frac{1}{A})}^{k} A^{C} = (C C_{𝑐} k) B^{k} A^{C} {(\frac{1}{A})}^{k}$
893	890 891 886	mulassd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) B^{k} A^{C} {(\frac{1}{A})}^{k} = (C C_{𝑐} k) B^{k} A^{C} {(\frac{1}{A})}^{k}$
894	889 892 893	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = (C C_{𝑐} k) B^{k} A^{C} {(\frac{1}{A})}^{k}$
895	868	nn0cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℂ$
896	877 895	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{k} \in ℂ$
897	877 878 895	cxpne0d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{k} \neq 0$
898	891 896 897	divrecd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{A^{C}}{A^{k}} = A^{C} (\frac{1}{A^{k}})$
899	4	ad2antrr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to C \in ℂ$
900	877 878 899 895	cxpsubd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C - k} = \frac{A^{C}}{A^{k}}$
901	868	nn0zd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℤ$
902	877 878 901	exprecd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {(\frac{1}{A})}^{k} = \frac{1}{A^{k}}$
903		cxpexp	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} = A^{k}$
904	877 868 903	syl2anc	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{k} = A^{k}$
905	904	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{1}{A^{k}} = \frac{1}{A^{k}}$
906	902 905	eqtr4d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to {(\frac{1}{A})}^{k} = \frac{1}{A^{k}}$
907	906	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C} {(\frac{1}{A})}^{k} = A^{C} (\frac{1}{A^{k}})$
908	898 900 907	3eqtr4rd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C} {(\frac{1}{A})}^{k} = A^{C - k}$
909	908	oveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) B^{k} A^{C} {(\frac{1}{A})}^{k} = (C C_{𝑐} k) B^{k} A^{C - k}$
910	899 895	subcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to C - k \in ℂ$
911	877 910	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C - k} \in ℂ$
912	733 885 911	mul32d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) B^{k} A^{C - k} = (C C_{𝑐} k) A^{C - k} B^{k}$
913	894 909 912	3eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = (C C_{𝑐} k) A^{C - k} B^{k}$
914	733 911 885	mulassd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) A^{C - k} B^{k} = (C C_{𝑐} k) A^{C - k} B^{k}$
915	913 914	eqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = (C C_{𝑐} k) A^{C - k} B^{k}$
916	915	sumeq2dv	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k}$
917	875 916	eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} (C C_{𝑐} k) {(\frac{B}{A})}^{k} A^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k}$
918	825 866 917	3eqtr3d	$⊢ (φ \land \neg C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k}$

Metamath Proof Explorer

Theorem binomcxplemnotnn0

Proof