Proof of Theorem plyeq0
Step | Hyp | Ref
| Expression |
1 | | plyeq0.3 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)) |
2 | | plyeq0.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
3 | | 0cnd 10033 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
4 | 3 | snssd 4340 |
. . . . . . . 8
⊢ (𝜑 → {0} ⊆
ℂ) |
5 | 2, 4 | unssd 3789 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
6 | | cnex 10017 |
. . . . . . 7
⊢ ℂ
∈ V |
7 | | ssexg 4804 |
. . . . . . 7
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
8 | 5, 6, 7 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V) |
9 | | nn0ex 11298 |
. . . . . 6
⊢
ℕ0 ∈ V |
10 | | elmapg 7870 |
. . . . . 6
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
11 | 8, 9, 10 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
12 | 1, 11 | mpbid 222 |
. . . 4
⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
13 | | ffn 6045 |
. . . 4
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → 𝐴 Fn
ℕ0) |
14 | 12, 13 | syl 17 |
. . 3
⊢ (𝜑 → 𝐴 Fn ℕ0) |
15 | | imadmrn 5476 |
. . . 4
⊢ (𝐴 “ dom 𝐴) = ran 𝐴 |
16 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 =
ℕ0) |
17 | | fimacnv 6347 |
. . . . . . . . 9
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → (◡𝐴 “ (𝑆 ∪ {0})) =
ℕ0) |
18 | 16, 17 | eqtr4d 2659 |
. . . . . . . 8
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 = (◡𝐴 “ (𝑆 ∪ {0}))) |
19 | 12, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝐴 = (◡𝐴 “ (𝑆 ∪ {0}))) |
20 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) = ∅) → (◡𝐴 “ (𝑆 ∖ {0})) = ∅) |
21 | 2 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → 𝑆 ⊆
ℂ) |
22 | | plyeq0.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → 𝑁 ∈
ℕ0) |
24 | 1 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → 𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)) |
25 | | plyeq0.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
26 | 25 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
27 | | plyeq0.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
28 | 27 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) →
0𝑝 = (𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
29 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, <
) |
30 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → (◡𝐴 “ (𝑆 ∖ {0})) ≠
∅) |
31 | 21, 23, 24, 26, 28, 29, 30 | plyeq0lem 23966 |
. . . . . . . . . . 11
⊢ ¬
(𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠
∅) |
32 | 31 | pm2.21i 116 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → (◡𝐴 “ (𝑆 ∖ {0})) = ∅) |
33 | 20, 32 | pm2.61dane 2881 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) = ∅) |
34 | 33 | uneq1d 3766 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝐴 “ (𝑆 ∖ {0})) ∪ (◡𝐴 “ {0})) = (∅ ∪ (◡𝐴 “ {0}))) |
35 | | undif1 4043 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ {0}) ∪ {0}) =
(𝑆 ∪
{0}) |
36 | 35 | imaeq2i 5464 |
. . . . . . . . 9
⊢ (◡𝐴 “ ((𝑆 ∖ {0}) ∪ {0})) = (◡𝐴 “ (𝑆 ∪ {0})) |
37 | | imaundi 5545 |
. . . . . . . . 9
⊢ (◡𝐴 “ ((𝑆 ∖ {0}) ∪ {0})) = ((◡𝐴 “ (𝑆 ∖ {0})) ∪ (◡𝐴 “ {0})) |
38 | 36, 37 | eqtr3i 2646 |
. . . . . . . 8
⊢ (◡𝐴 “ (𝑆 ∪ {0})) = ((◡𝐴 “ (𝑆 ∖ {0})) ∪ (◡𝐴 “ {0})) |
39 | | un0 3967 |
. . . . . . . . 9
⊢ ((◡𝐴 “ {0}) ∪ ∅) = (◡𝐴 “ {0}) |
40 | | uncom 3757 |
. . . . . . . . 9
⊢ ((◡𝐴 “ {0}) ∪ ∅) = (∅
∪ (◡𝐴 “ {0})) |
41 | 39, 40 | eqtr3i 2646 |
. . . . . . . 8
⊢ (◡𝐴 “ {0}) = (∅ ∪ (◡𝐴 “ {0})) |
42 | 34, 38, 41 | 3eqtr4g 2681 |
. . . . . . 7
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∪ {0})) = (◡𝐴 “ {0})) |
43 | 19, 42 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → dom 𝐴 = (◡𝐴 “ {0})) |
44 | | eqimss 3657 |
. . . . . 6
⊢ (dom
𝐴 = (◡𝐴 “ {0}) → dom 𝐴 ⊆ (◡𝐴 “ {0})) |
45 | 43, 44 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝐴 ⊆ (◡𝐴 “ {0})) |
46 | | ffun 6048 |
. . . . . . 7
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → Fun 𝐴) |
47 | 12, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun 𝐴) |
48 | | ssid 3624 |
. . . . . 6
⊢ dom 𝐴 ⊆ dom 𝐴 |
49 | | funimass3 6333 |
. . . . . 6
⊢ ((Fun
𝐴 ∧ dom 𝐴 ⊆ dom 𝐴) → ((𝐴 “ dom 𝐴) ⊆ {0} ↔ dom 𝐴 ⊆ (◡𝐴 “ {0}))) |
50 | 47, 48, 49 | sylancl 694 |
. . . . 5
⊢ (𝜑 → ((𝐴 “ dom 𝐴) ⊆ {0} ↔ dom 𝐴 ⊆ (◡𝐴 “ {0}))) |
51 | 45, 50 | mpbird 247 |
. . . 4
⊢ (𝜑 → (𝐴 “ dom 𝐴) ⊆ {0}) |
52 | 15, 51 | syl5eqssr 3650 |
. . 3
⊢ (𝜑 → ran 𝐴 ⊆ {0}) |
53 | | df-f 5892 |
. . 3
⊢ (𝐴:ℕ0⟶{0}
↔ (𝐴 Fn
ℕ0 ∧ ran 𝐴 ⊆ {0})) |
54 | 14, 52, 53 | sylanbrc 698 |
. 2
⊢ (𝜑 → 𝐴:ℕ0⟶{0}) |
55 | | c0ex 10034 |
. . 3
⊢ 0 ∈
V |
56 | 55 | fconst2 6470 |
. 2
⊢ (𝐴:ℕ0⟶{0}
↔ 𝐴 =
(ℕ0 × {0})) |
57 | 54, 56 | sylib 208 |
1
⊢ (𝜑 → 𝐴 = (ℕ0 ×
{0})) |