Theorem binomcxplemdvsum 37576

Description: Lemma for binomcxp 37578. The derivative of the generalized sum in binomcxplemnn0 37570. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)

Hypotheses

Ref	Expression
binomcxp.a	⊢ (𝜑 → 𝐴 ∈ ℝ+)
binomcxp.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
binomcxp.lt	⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))
binomcxp.c	⊢ (𝜑 → 𝐶 ∈ ℂ)
binomcxplem.f	⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))
binomcxplem.s	⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
binomcxplem.r	⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
binomcxplem.e	⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))
binomcxplem.d	⊢ 𝐷 = (◡abs “ (0[,)𝑅))
binomcxplem.p	⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘))

Assertion

Ref	Expression
binomcxplemdvsum	⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)))

Distinct variable groups:   𝑘,𝑏,𝐹   𝜑,𝑏,𝑘   𝑟,𝑏,𝑘,𝐹   𝑗,𝑘,𝜑   𝐶,𝑗

Allowed substitution hints:   𝜑(𝑟)   𝐴(𝑗,𝑘,𝑟,𝑏)   𝐵(𝑗,𝑘,𝑟,𝑏)   𝐶(𝑘,𝑟,𝑏)   𝐷(𝑗,𝑘,𝑟,𝑏)   𝑃(𝑗,𝑘,𝑟,𝑏)   𝑅(𝑗,𝑘,𝑟,𝑏)   𝑆(𝑗,𝑘,𝑟,𝑏)   𝐸(𝑗,𝑘,𝑟,𝑏)   𝐹(𝑗)

Proof of Theorem binomcxplemdvsum

Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		binomcxplem.s	. . . 4 ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
2		binomcxplem.p	. . . . 5 ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘))
3		binomcxplem.d	. . . . . . 7 ⊢ 𝐷 = (◡abs “ (0[,)𝑅))
4		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑏◡abs
5		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑏0
6		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑏[,)
7		binomcxplem.r	. . . . . . . . . 10 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
8		nfcv 2751	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏 +
9		nfmpt1 4675	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
10	1, 9	nfcxfr 2749	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏𝑆
11		nfcv 2751	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏𝑟
12	10, 11	nffv 6110	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑆‘𝑟)
13	5, 8, 12	nfseq 12673	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏seq0( + , (𝑆‘𝑟))
14	13	nfel1 2765	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏seq0( + , (𝑆‘𝑟)) ∈ dom ⇝
15		nfcv 2751	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏ℝ
16	14, 15	nfrab 3100	. . . . . . . . . . 11 ⊢ Ⅎ𝑏{𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }
17		nfcv 2751	. . . . . . . . . . 11 ⊢ Ⅎ𝑏ℝ*
18		nfcv 2751	. . . . . . . . . . 11 ⊢ Ⅎ𝑏 <
19	16, 17, 18	nfsup 8240	. . . . . . . . . 10 ⊢ Ⅎ𝑏sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
20	7, 19	nfcxfr 2749	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑅
21	5, 6, 20	nfov 6575	. . . . . . . 8 ⊢ Ⅎ𝑏(0[,)𝑅)
22	4, 21	nfima 5393	. . . . . . 7 ⊢ Ⅎ𝑏(◡abs “ (0[,)𝑅))
23	3, 22	nfcxfr 2749	. . . . . 6 ⊢ Ⅎ𝑏𝐷
24		nfcv 2751	. . . . . 6 ⊢ Ⅎ𝑦𝐷
25		nfcv 2751	. . . . . 6 ⊢ Ⅎ𝑦Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)
26		nfcv 2751	. . . . . . 7 ⊢ Ⅎ𝑏ℕ0
27		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑦
28	10, 27	nffv 6110	. . . . . . . 8 ⊢ Ⅎ𝑏(𝑆‘𝑦)
29		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑏𝑚
30	28, 29	nffv 6110	. . . . . . 7 ⊢ Ⅎ𝑏((𝑆‘𝑦)‘𝑚)
31	26, 30	nfsum 14269	. . . . . 6 ⊢ Ⅎ𝑏Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚)
32		simpl 472	. . . . . . . . . 10 ⊢ ((𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0) → 𝑏 = 𝑦)
33	32	fveq2d 6107	. . . . . . . . 9 ⊢ ((𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑏) = (𝑆‘𝑦))
34	33	fveq1d 6105	. . . . . . . 8 ⊢ ((𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑏)‘𝑘) = ((𝑆‘𝑦)‘𝑘))
35	34	sumeq2dv 14281	. . . . . . 7 ⊢ (𝑏 = 𝑦 → Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘) = Σ𝑘 ∈ ℕ0 ((𝑆‘𝑦)‘𝑘))
36		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑚((𝑆‘𝑦)‘𝑘)
37		nfcv 2751	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘ℂ
38		nfmpt1 4675	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))
39	37, 38	nfmpt 4674	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
40	1, 39	nfcxfr 2749	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑆
41		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑦
42	40, 41	nffv 6110	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝑆‘𝑦)
43		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑘𝑚
44	42, 43	nffv 6110	. . . . . . . 8 ⊢ Ⅎ𝑘((𝑆‘𝑦)‘𝑚)
45		fveq2 6103	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ((𝑆‘𝑦)‘𝑘) = ((𝑆‘𝑦)‘𝑚))
46	36, 44, 45	cbvsumi 14275	. . . . . . 7 ⊢ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑦)‘𝑘) = Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚)
47	35, 46	syl6eq 2660	. . . . . 6 ⊢ (𝑏 = 𝑦 → Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘) = Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚))
48	23, 24, 25, 31, 47	cbvmptf 4676	. . . . 5 ⊢ (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) = (𝑦 ∈ 𝐷 ↦ Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚))
49	2, 48	eqtri 2632	. . . 4 ⊢ 𝑃 = (𝑦 ∈ 𝐷 ↦ Σ𝑚 ∈ ℕ0 ((𝑆‘𝑦)‘𝑚))
50		ovex 6577	. . . . . 6 ⊢ (𝐶C𝑐𝑗) ∈ V
51	50	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐶C𝑐𝑗) ∈ V)
52		binomcxplem.f	. . . . . 6 ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))
53	52	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)))
54	52	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)))
55		simpr 476	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
56	55	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝐶C𝑐𝑗) = (𝐶C𝑐𝑘))
57		simpr 476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
58		binomcxp.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
59	58	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)
60	59, 57	bcccl 37560	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶C𝑐𝑘) ∈ ℂ)
61	54, 56, 57, 60	fvmptd 6197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐶C𝑐𝑘))
62	61, 60	eqeltrd 2688	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ)
63	51, 53, 62	fmpt2d 6300	. . . 4 ⊢ (𝜑 → 𝐹:ℕ0⟶ℂ)
64		nfcv 2751	. . . . . . 7 ⊢ Ⅎ𝑟ℝ
65		nfcv 2751	. . . . . . 7 ⊢ Ⅎ𝑧ℝ
66		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑧seq0( + , (𝑆‘𝑟)) ∈ dom ⇝
67		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑟0
68		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑟 +
69		nfcv 2751	. . . . . . . . . . 11 ⊢ Ⅎ𝑟(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
70	1, 69	nfcxfr 2749	. . . . . . . . . 10 ⊢ Ⅎ𝑟𝑆
71		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑟𝑧
72	70, 71	nffv 6110	. . . . . . . . 9 ⊢ Ⅎ𝑟(𝑆‘𝑧)
73	67, 68, 72	nfseq 12673	. . . . . . . 8 ⊢ Ⅎ𝑟seq0( + , (𝑆‘𝑧))
74	73	nfel1 2765	. . . . . . 7 ⊢ Ⅎ𝑟seq0( + , (𝑆‘𝑧)) ∈ dom ⇝
75		fveq2 6103	. . . . . . . . 9 ⊢ (𝑟 = 𝑧 → (𝑆‘𝑟) = (𝑆‘𝑧))
76	75	seqeq3d 12671	. . . . . . . 8 ⊢ (𝑟 = 𝑧 → seq0( + , (𝑆‘𝑟)) = seq0( + , (𝑆‘𝑧)))
77	76	eleq1d 2672	. . . . . . 7 ⊢ (𝑟 = 𝑧 → (seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ ))
78	64, 65, 66, 74, 77	cbvrab 3171	. . . . . 6 ⊢ {𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }
79	78	supeq1i 8236	. . . . 5 ⊢ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }, ℝ*, < )
80	7, 79	eqtri 2632	. . . 4 ⊢ 𝑅 = sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }, ℝ*, < )
81	1	fveq1i 6104	. . . . . . . . . . . 12 ⊢ (𝑆‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)
82		seqeq3 12668	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧) → seq0( + , (𝑆‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)))
83	81, 82	ax-mp 5	. . . . . . . . . . 11 ⊢ seq0( + , (𝑆‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧))
84	83	eleq1i 2679	. . . . . . . . . 10 ⊢ (seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ ↔ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ )
85	84	a1i 11	. . . . . . . . 9 ⊢ (𝑧 ∈ ℝ → (seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ ↔ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ ))
86	85	rabbiia 3161	. . . . . . . 8 ⊢ {𝑧 ∈ ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }
87	86	supeq1i 8236	. . . . . . 7 ⊢ sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )
88	7, 79, 87	3eqtrri 2637	. . . . . 6 ⊢ sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) = 𝑅
89	88	eleq1i 2679	. . . . 5 ⊢ (sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ ↔ 𝑅 ∈ ℝ)
90	88	oveq2i 6560	. . . . . 6 ⊢ ((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) = ((abs‘𝑥) + 𝑅)
91	90	oveq1i 6559	. . . . 5 ⊢ (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2) = (((abs‘𝑥) + 𝑅) / 2)
92		eqid 2610	. . . . 5 ⊢ ((abs‘𝑥) + 1) = ((abs‘𝑥) + 1)
93	89, 91, 92	ifbieq12i 4062	. . . 4 ⊢ if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1)) = if(𝑅 ∈ ℝ, (((abs‘𝑥) + 𝑅) / 2), ((abs‘𝑥) + 1))
94		oveq1 6556	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑏 → (𝑤↑𝑘) = (𝑏↑𝑘))
95	94	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑏 → ((𝐹‘𝑘) · (𝑤↑𝑘)) = ((𝐹‘𝑘) · (𝑏↑𝑘)))
96	95	mpteq2dv 4673	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
97	96	cbvmptv 4678	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘)))) = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))
98	97	fveq1i 6104	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)
99		seqeq3 12668	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧) → seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)))
100	98, 99	ax-mp 5	. . . . . . . . . . . . 13 ⊢ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧))
101	100	eleq1i 2679	. . . . . . . . . . . 12 ⊢ (seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ ↔ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ )
102	101	a1i 11	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℝ → (seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ ↔ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ ))
103	102	rabbiia 3161	. . . . . . . . . 10 ⊢ {𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }
104	103	supeq1i 8236	. . . . . . . . 9 ⊢ sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )
105	104	eleq1i 2679	. . . . . . . 8 ⊢ (sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ ↔ sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ)
106	104	oveq2i 6560	. . . . . . . . 9 ⊢ ((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) = ((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ))
107	106	oveq1i 6559	. . . . . . . 8 ⊢ (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2) = (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2)
108	105, 107, 92	ifbieq12i 4062	. . . . . . 7 ⊢ if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1)) = if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))
109	108	oveq2i 6560	. . . . . 6 ⊢ ((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) = ((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1)))
110	109	oveq1i 6559	. . . . 5 ⊢ (((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2) = (((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2)
111	110	oveq2i 6560	. . . 4 ⊢ (0(ball‘(abs ∘ − ))(((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑤↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2)) = (0(ball‘(abs ∘ − ))(((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2))
112	1, 49, 63, 80, 3, 93, 111	pserdv2 23988	. . 3 ⊢ (𝜑 → (ℂ D 𝑃) = (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1)))))
113		cnvimass 5404	. . . . . . . 8 ⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs
114	3, 113	eqsstri 3598	. . . . . . 7 ⊢ 𝐷 ⊆ dom abs
115		absf 13925	. . . . . . . 8 ⊢ abs:ℂ⟶ℝ
116	115	fdmi 5965	. . . . . . 7 ⊢ dom abs = ℂ
117	114, 116	sseqtri 3600	. . . . . 6 ⊢ 𝐷 ⊆ ℂ
118	117	sseli 3564	. . . . 5 ⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ ℂ)
119		binomcxplem.e	. . . . . . . . . 10 ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))
120	119	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))))
121		simplr 788	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → 𝑏 = 𝑦)
122	121	oveq1d 6564	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → (𝑏↑(𝑘 − 1)) = (𝑦↑(𝑘 − 1)))
123	122	oveq2d 6565	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))) = ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1))))
124	123	mpteq2dva 4672	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))))
125		simpr 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
126		nnex 10903	. . . . . . . . . . 11 ⊢ ℕ ∈ V
127	126	mptex 6390	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))) ∈ V
128	127	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))) ∈ V)
129	120, 124, 125, 128	fvmptd 6197	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐸‘𝑦) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))))
130	129	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑦) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1)))))
131		simpr 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
132	131	fveq2d 6107	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝐹‘𝑘) = (𝐹‘𝑛))
133	131, 132	oveq12d 6567	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑘 · (𝐹‘𝑘)) = (𝑛 · (𝐹‘𝑛)))
134	131	oveq1d 6564	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑘 − 1) = (𝑛 − 1))
135	134	oveq2d 6565	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑦↑(𝑘 − 1)) = (𝑦↑(𝑛 − 1)))
136	133, 135	oveq12d 6567	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → ((𝑘 · (𝐹‘𝑘)) · (𝑦↑(𝑘 − 1))) = ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))))
137		simpr 476	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
138		ovex 6577	. . . . . . . 8 ⊢ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V
139	138	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V)
140	130, 136, 137, 139	fvmptd 6197	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑦)‘𝑛) = ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))))
141	140	sumeq2dv 14281	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))))
142	118, 141	sylan2 490	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1))))
143	142	mpteq2dva 4672	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛)) = (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝑛 · (𝐹‘𝑛)) · (𝑦↑(𝑛 − 1)))))
144	112, 143	eqtr4d 2647	. 2 ⊢ (𝜑 → (ℂ D 𝑃) = (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛)))
145		nfcv 2751	. . . 4 ⊢ Ⅎ𝑏ℕ
146		nfmpt1 4675	. . . . . . 7 ⊢ Ⅎ𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))
147	119, 146	nfcxfr 2749	. . . . . 6 ⊢ Ⅎ𝑏𝐸
148	147, 27	nffv 6110	. . . . 5 ⊢ Ⅎ𝑏(𝐸‘𝑦)
149		nfcv 2751	. . . . 5 ⊢ Ⅎ𝑏𝑛
150	148, 149	nffv 6110	. . . 4 ⊢ Ⅎ𝑏((𝐸‘𝑦)‘𝑛)
151	145, 150	nfsum 14269	. . 3 ⊢ Ⅎ𝑏Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛)
152		nfcv 2751	. . 3 ⊢ Ⅎ𝑦Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)
153		simpl 472	. . . . . . 7 ⊢ ((𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ) → 𝑦 = 𝑏)
154	153	fveq2d 6107	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑦) = (𝐸‘𝑏))
155	154	fveq1d 6105	. . . . 5 ⊢ ((𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑦)‘𝑛) = ((𝐸‘𝑏)‘𝑛))
156	155	sumeq2dv 14281	. . . 4 ⊢ (𝑦 = 𝑏 → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝐸‘𝑏)‘𝑛))
157		nfmpt1 4675	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))
158	37, 157	nfmpt 4674	. . . . . . . 8 ⊢ Ⅎ𝑘(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))
159	119, 158	nfcxfr 2749	. . . . . . 7 ⊢ Ⅎ𝑘𝐸
160		nfcv 2751	. . . . . . 7 ⊢ Ⅎ𝑘𝑏
161	159, 160	nffv 6110	. . . . . 6 ⊢ Ⅎ𝑘(𝐸‘𝑏)
162		nfcv 2751	. . . . . 6 ⊢ Ⅎ𝑘𝑛
163	161, 162	nffv 6110	. . . . 5 ⊢ Ⅎ𝑘((𝐸‘𝑏)‘𝑛)
164		nfcv 2751	. . . . 5 ⊢ Ⅎ𝑛((𝐸‘𝑏)‘𝑘)
165		fveq2 6103	. . . . 5 ⊢ (𝑛 = 𝑘 → ((𝐸‘𝑏)‘𝑛) = ((𝐸‘𝑏)‘𝑘))
166	163, 164, 165	cbvsumi 14275	. . . 4 ⊢ Σ𝑛 ∈ ℕ ((𝐸‘𝑏)‘𝑛) = Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)
167	156, 166	syl6eq 2660	. . 3 ⊢ (𝑦 = 𝑏 → Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘))
168	24, 23, 151, 152, 167	cbvmptf 4676	. 2 ⊢ (𝑦 ∈ 𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸‘𝑦)‘𝑛)) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘))
169	144, 168	syl6eq 2660	1 ⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ^◡ccnv 5037  dom cdm 5038   “ cima 5041   ∘ ccom 5042  ‘cfv 5804  (class class class)co 6549  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ^*cxr 9952   < clt 9953   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ℝ⁺crp 11708  [,)cico 12048  seqcseq 12663  ↑cexp 12722  abscabs 13822   ⇝ cli 14063  Σcsu 14264  ballcbl 19554   D cdv 23433  C_𝑐cbcc 37557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-fac 12923  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-prod 14475  df-fallfac 14577  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-ulm 23935  df-bcc 37558

This theorem is referenced by:  binomcxplemnotnn0  37577