Step | Hyp | Ref
| Expression |
1 | | binomcxplem.d |
. . . . 5
⊢ 𝐷 = (◡abs “ (0[,)𝑅)) |
2 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑏◡abs |
3 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑏0 |
4 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑏[,) |
5 | | binomcxplem.r |
. . . . . . . 8
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
6 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏
+ |
7 | | binomcxplem.s |
. . . . . . . . . . . . . 14
⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) |
8 | | nfmpt1 4675 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) |
9 | 7, 8 | nfcxfr 2749 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏𝑆 |
10 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏𝑟 |
11 | 9, 10 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏(𝑆‘𝑟) |
12 | 3, 6, 11 | nfseq 12673 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏seq0(
+ , (𝑆‘𝑟)) |
13 | 12 | nfel1 2765 |
. . . . . . . . . 10
⊢
Ⅎ𝑏seq0( + ,
(𝑆‘𝑟)) ∈ dom ⇝ |
14 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑏ℝ |
15 | 13, 14 | nfrab 3100 |
. . . . . . . . 9
⊢
Ⅎ𝑏{𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ } |
16 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑏ℝ* |
17 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑏
< |
18 | 15, 16, 17 | nfsup 8240 |
. . . . . . . 8
⊢
Ⅎ𝑏sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
19 | 5, 18 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑏𝑅 |
20 | 3, 4, 19 | nfov 6575 |
. . . . . 6
⊢
Ⅎ𝑏(0[,)𝑅) |
21 | 2, 20 | nfima 5393 |
. . . . 5
⊢
Ⅎ𝑏(◡abs
“ (0[,)𝑅)) |
22 | 1, 21 | nfcxfr 2749 |
. . . 4
⊢
Ⅎ𝑏𝐷 |
23 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑦𝐷 |
24 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑦((1 +
𝑏)↑𝑐-𝐶) |
25 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑏((1 +
𝑦)↑𝑐-𝐶) |
26 | | oveq2 6557 |
. . . . 5
⊢ (𝑏 = 𝑦 → (1 + 𝑏) = (1 + 𝑦)) |
27 | 26 | oveq1d 6564 |
. . . 4
⊢ (𝑏 = 𝑦 → ((1 + 𝑏)↑𝑐-𝐶) = ((1 + 𝑦)↑𝑐-𝐶)) |
28 | 22, 23, 24, 25, 27 | cbvmptf 4676 |
. . 3
⊢ (𝑏 ∈ 𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶)) = (𝑦 ∈ 𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶)) |
29 | 28 | oveq2i 6560 |
. 2
⊢ (ℂ
D (𝑏 ∈ 𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (ℂ D (𝑦 ∈ 𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶))) |
30 | | cnelprrecn 9908 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
31 | 30 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ℂ
∈ {ℝ, ℂ}) |
32 | | 1cnd 9935 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → 1 ∈ ℂ) |
33 | | cnvimass 5404 |
. . . . . . . . . 10
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
34 | 1, 33 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝐷 ⊆ dom
abs |
35 | | absf 13925 |
. . . . . . . . . 10
⊢
abs:ℂ⟶ℝ |
36 | 35 | fdmi 5965 |
. . . . . . . . 9
⊢ dom abs =
ℂ |
37 | 34, 36 | sseqtri 3600 |
. . . . . . . 8
⊢ 𝐷 ⊆
ℂ |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝐷 ⊆
ℂ) |
39 | 38 | sselda 3568 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ ℂ) |
40 | 32, 39 | addcld 9938 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → (1 + 𝑦) ∈ ℂ) |
41 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → (1 + 𝑦) ∈
ℝ) |
42 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 1 ∈
ℂ) |
43 | 39 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 𝑦 ∈ ℂ) |
44 | 42, 43 | pncan2d 10273 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → ((1 + 𝑦) − 1) = 𝑦) |
45 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 1 ∈
ℝ) |
46 | 41, 45 | resubcld 10337 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → ((1 + 𝑦) − 1) ∈
ℝ) |
47 | 44, 46 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 𝑦 ∈ ℝ) |
48 | | 1pneg1e0 11006 |
. . . . . . . . 9
⊢ (1 + -1)
= 0 |
49 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → 1 ∈
ℝ) |
50 | 49 | renegcld 10336 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → -1 ∈
ℝ) |
51 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
52 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
53 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (abs Fn
ℂ → (𝑦 ∈
(◡abs “ (0[,)𝑅)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)𝑅)))) |
54 | 35, 52, 53 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡abs “ (0[,)𝑅)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)𝑅))) |
55 | 54 | simprbi 479 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (◡abs “ (0[,)𝑅)) → (abs‘𝑦) ∈ (0[,)𝑅)) |
56 | 55, 1 | eleq2s 2706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝐷 → (abs‘𝑦) ∈ (0[,)𝑅)) |
57 | | 0re 9919 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
58 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝑆‘𝑟)) ∈ dom ⇝ } ⊆
ℝ |
59 | | ressxr 9962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℝ
⊆ ℝ* |
60 | 58, 59 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝑆‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* |
61 | | supxrcl 12017 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑟 ∈ ℝ ∣ seq0( +
, (𝑆‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ* |
63 | 5, 62 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑅 ∈
ℝ* |
64 | | elico2 12108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 𝑅
∈ ℝ*) → ((abs‘𝑦) ∈ (0[,)𝑅) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) < 𝑅))) |
65 | 57, 63, 64 | mp2an 704 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘𝑦)
∈ (0[,)𝑅) ↔
((abs‘𝑦) ∈
ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) < 𝑅)) |
66 | 56, 65 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐷 → ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) < 𝑅)) |
67 | 66 | simp3d 1068 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐷 → (abs‘𝑦) < 𝑅) |
68 | 67 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → (abs‘𝑦) < 𝑅) |
69 | | binomcxp.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
70 | | binomcxp.b |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℝ) |
71 | | binomcxp.lt |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) |
72 | | binomcxp.c |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℂ) |
73 | | binomcxplem.f |
. . . . . . . . . . . . . . . 16
⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) |
74 | 69, 70, 71, 72, 73, 7, 5 | binomcxplemradcnv 37573 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝑅 = 1) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → 𝑅 = 1) |
76 | 68, 75 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → (abs‘𝑦) < 1) |
77 | 76 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → (abs‘𝑦) < 1) |
78 | 51, 49 | absltd 14016 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (-1 < 𝑦 ∧ 𝑦 < 1))) |
79 | 77, 78 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → (-1 < 𝑦 ∧ 𝑦 < 1)) |
80 | 79 | simpld 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → -1 < 𝑦) |
81 | 50, 51, 49, 80 | ltadd2dd 10075 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → (1 + -1) < (1 +
𝑦)) |
82 | 48, 81 | syl5eqbrr 4619 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ ℝ) → 0 < (1 + 𝑦)) |
83 | 47, 82 | syldan 486 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 0 < (1 + 𝑦)) |
84 | 41, 83 | elrpd 11745 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) ∧ (1 + 𝑦) ∈ ℝ) → (1 + 𝑦) ∈
ℝ+) |
85 | 84 | ex 449 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → ((1 + 𝑦) ∈ ℝ → (1 + 𝑦) ∈
ℝ+)) |
86 | | eqid 2610 |
. . . . . 6
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
87 | 86 | ellogdm 24185 |
. . . . 5
⊢ ((1 +
𝑦) ∈ (ℂ ∖
(-∞(,]0)) ↔ ((1 + 𝑦) ∈ ℂ ∧ ((1 + 𝑦) ∈ ℝ → (1 +
𝑦) ∈
ℝ+))) |
88 | 40, 85, 87 | sylanbrc 695 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → (1 + 𝑦) ∈ (ℂ ∖
(-∞(,]0))) |
89 | | eldifi 3694 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
(-∞(,]0)) → 𝑥
∈ ℂ) |
90 | 89 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖
(-∞(,]0))) → 𝑥
∈ ℂ) |
91 | 72 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝐶 ∈
ℂ) |
92 | 91 | negcld 10258 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → -𝐶 ∈
ℂ) |
93 | 92 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖
(-∞(,]0))) → -𝐶
∈ ℂ) |
94 | 90, 93 | cxpcld 24254 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖
(-∞(,]0))) → (𝑥↑𝑐-𝐶) ∈ ℂ) |
95 | | ovex 6577 |
. . . . 5
⊢ (-𝐶 · (𝑥↑𝑐(-𝐶 − 1))) ∈ V |
96 | 95 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖
(-∞(,]0))) → (-𝐶
· (𝑥↑𝑐(-𝐶 − 1))) ∈ V) |
97 | | 1cnd 9935 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → 1 ∈
ℂ) |
98 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
99 | 97, 98 | addcld 9938 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → (1 +
𝑥) ∈
ℂ) |
100 | | c0ex 9913 |
. . . . . . . . 9
⊢ 0 ∈
V |
101 | 100 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → 0 ∈
V) |
102 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 1 ∈
ℂ) |
103 | 31, 102 | dvmptc 23527 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑥 ∈ ℂ ↦
1)) = (𝑥 ∈ ℂ
↦ 0)) |
104 | 31 | dvmptid 23526 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑥 ∈ ℂ ↦
𝑥)) = (𝑥 ∈ ℂ ↦ 1)) |
105 | 31, 97, 101, 103, 98, 97, 104 | dvmptadd 23529 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑥 ∈ ℂ ↦
(1 + 𝑥))) = (𝑥 ∈ ℂ ↦ (0 +
1))) |
106 | | 0p1e1 11009 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
107 | 106 | mpteq2i 4669 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ ↦ (0 + 1))
= (𝑥 ∈ ℂ ↦
1) |
108 | 105, 107 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑥 ∈ ℂ ↦
(1 + 𝑥))) = (𝑥 ∈ ℂ ↦
1)) |
109 | | fvex 6113 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ V |
110 | | cnfldtps 22391 |
. . . . . . . . . 10
⊢
ℂfld ∈ TopSp |
111 | | cnfldbas 19571 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
112 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
113 | 111, 112 | tpsuni 20553 |
. . . . . . . . . 10
⊢
(ℂfld ∈ TopSp → ℂ = ∪ (TopOpen‘ℂfld)) |
114 | 110, 113 | ax-mp 5 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
115 | 114 | restid 15917 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ∈ V →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
116 | 109, 115 | ax-mp 5 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
117 | 116 | eqcomi 2619 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
118 | 112 | cnfldtop 22397 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
119 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) = (abs ∘ − ) |
120 | 119 | cnbl0 22387 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ*
→ (◡abs “ (0[,)𝑅)) = (0(ball‘(abs ∘
− ))𝑅)) |
121 | 63, 120 | ax-mp 5 |
. . . . . . . . . 10
⊢ (◡abs “ (0[,)𝑅)) = (0(ball‘(abs ∘ −
))𝑅) |
122 | 1, 121 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝐷 = (0(ball‘(abs ∘
− ))𝑅) |
123 | | cnxmet 22386 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
124 | | 0cn 9911 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
125 | 112 | cnfldtopn 22395 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
126 | 125 | blopn 22115 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑅) ∈
(TopOpen‘ℂfld)) |
127 | 123, 124,
63, 126 | mp3an 1416 |
. . . . . . . . 9
⊢
(0(ball‘(abs ∘ − ))𝑅) ∈
(TopOpen‘ℂfld) |
128 | 122, 127 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
129 | | isopn3i 20696 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐷 ∈
(TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘𝐷) = 𝐷) |
130 | 118, 128,
129 | mp2an 704 |
. . . . . . 7
⊢
((int‘(TopOpen‘ℂfld))‘𝐷) = 𝐷 |
131 | 130 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) →
((int‘(TopOpen‘ℂfld))‘𝐷) = 𝐷) |
132 | 31, 99, 97, 108, 38, 117, 112, 131 | dvmptres2 23531 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑥 ∈ 𝐷 ↦ (1 + 𝑥))) = (𝑥 ∈ 𝐷 ↦ 1)) |
133 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (1 + 𝑥) = (1 + 𝑦)) |
134 | 133 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (1 + 𝑥)) = (𝑦 ∈ 𝐷 ↦ (1 + 𝑦)) |
135 | 134 | oveq2i 6560 |
. . . . 5
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ (1 + 𝑥))) = (ℂ D (𝑦 ∈ 𝐷 ↦ (1 + 𝑦))) |
136 | | eqidd 2611 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 1 = 1) |
137 | 136 | cbvmptv 4678 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ 1) = (𝑦 ∈ 𝐷 ↦ 1) |
138 | 132, 135,
137 | 3eqtr3g 2667 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑦 ∈ 𝐷 ↦ (1 + 𝑦))) = (𝑦 ∈ 𝐷 ↦ 1)) |
139 | 86 | dvcncxp1 24284 |
. . . . 5
⊢ (-𝐶 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ (-∞(,]0)) ↦ (𝑥↑𝑐-𝐶))) = (𝑥 ∈ (ℂ ∖ (-∞(,]0))
↦ (-𝐶 · (𝑥↑𝑐(-𝐶 − 1))))) |
140 | 92, 139 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑥 ∈ (ℂ
∖ (-∞(,]0)) ↦ (𝑥↑𝑐-𝐶))) = (𝑥 ∈ (ℂ ∖ (-∞(,]0))
↦ (-𝐶 · (𝑥↑𝑐(-𝐶 − 1))))) |
141 | | oveq1 6556 |
. . . 4
⊢ (𝑥 = (1 + 𝑦) → (𝑥↑𝑐-𝐶) = ((1 + 𝑦)↑𝑐-𝐶)) |
142 | | oveq1 6556 |
. . . . 5
⊢ (𝑥 = (1 + 𝑦) → (𝑥↑𝑐(-𝐶 − 1)) = ((1 + 𝑦)↑𝑐(-𝐶 − 1))) |
143 | 142 | oveq2d 6565 |
. . . 4
⊢ (𝑥 = (1 + 𝑦) → (-𝐶 · (𝑥↑𝑐(-𝐶 − 1))) = (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))) |
144 | 31, 31, 88, 32, 94, 96, 138, 140, 141, 143 | dvmptco 23541 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑦 ∈ 𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶))) = (𝑦 ∈ 𝐷 ↦ ((-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) ·
1))) |
145 | 91 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → 𝐶 ∈ ℂ) |
146 | 145 | negcld 10258 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → -𝐶 ∈ ℂ) |
147 | 146, 32 | subcld 10271 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → (-𝐶 − 1) ∈ ℂ) |
148 | 40, 147 | cxpcld 24254 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → ((1 + 𝑦)↑𝑐(-𝐶 − 1)) ∈
ℂ) |
149 | 146, 148 | mulcld 9939 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) ∈
ℂ) |
150 | 149 | mulid1d 9936 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦 ∈ 𝐷) → ((-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) · 1) =
(-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))) |
151 | 150 | mpteq2dva 4672 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑦 ∈ 𝐷 ↦ ((-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) · 1)) =
(𝑦 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))))) |
152 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑏(-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) |
153 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦(-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))) |
154 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (1 + 𝑦) = (1 + 𝑏)) |
155 | 154 | oveq1d 6564 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((1 + 𝑦)↑𝑐(-𝐶 − 1)) = ((1 + 𝑏)↑𝑐(-𝐶 − 1))) |
156 | 155 | oveq2d 6565 |
. . . . 5
⊢ (𝑦 = 𝑏 → (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) = (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))) |
157 | 23, 22, 152, 153, 156 | cbvmptf 4676 |
. . . 4
⊢ (𝑦 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))) |
158 | 157 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑦 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))) |
159 | 144, 151,
158 | 3eqtrd 2648 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑦 ∈ 𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))) |
160 | 29, 159 | syl5eq 2656 |
1
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ
D (𝑏 ∈ 𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))) |