Proof of Theorem plyeq0
Step | Hyp | Ref
| Expression |
1 | | plyeq0.3 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) |
2 | | plyeq0.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
3 | | 0cnd 10826 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
4 | 3 | snssd 4722 |
. . . . . . . 8
⊢ (𝜑 → {0} ⊆
ℂ) |
5 | 2, 4 | unssd 4100 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
6 | | cnex 10810 |
. . . . . . 7
⊢ ℂ
∈ V |
7 | | ssexg 5216 |
. . . . . . 7
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
8 | 5, 6, 7 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V) |
9 | | nn0ex 12096 |
. . . . . 6
⊢
ℕ0 ∈ V |
10 | | elmapg 8521 |
. . . . . 6
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
11 | 8, 9, 10 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
12 | 1, 11 | mpbid 235 |
. . . 4
⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
13 | 12 | ffnd 6546 |
. . 3
⊢ (𝜑 → 𝐴 Fn ℕ0) |
14 | | imadmrn 5939 |
. . . 4
⊢ (𝐴 “ dom 𝐴) = ran 𝐴 |
15 | | fdm 6554 |
. . . . . . . . 9
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 =
ℕ0) |
16 | | fimacnv 6567 |
. . . . . . . . 9
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → (◡𝐴 “ (𝑆 ∪ {0})) =
ℕ0) |
17 | 15, 16 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 = (◡𝐴 “ (𝑆 ∪ {0}))) |
18 | 12, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝐴 = (◡𝐴 “ (𝑆 ∪ {0}))) |
19 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) = ∅) → (◡𝐴 “ (𝑆 ∖ {0})) = ∅) |
20 | 2 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → 𝑆 ⊆
ℂ) |
21 | | plyeq0.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
22 | 21 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → 𝑁 ∈
ℕ0) |
23 | 1 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) |
24 | | plyeq0.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
25 | 24 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
26 | | plyeq0.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
27 | 26 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) →
0𝑝 = (𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
28 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, <
) |
29 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → (◡𝐴 “ (𝑆 ∖ {0})) ≠
∅) |
30 | 20, 22, 23, 25, 27, 28, 29 | plyeq0lem 25104 |
. . . . . . . . . . 11
⊢ ¬
(𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠
∅) |
31 | 30 | pm2.21i 119 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) → (◡𝐴 “ (𝑆 ∖ {0})) = ∅) |
32 | 19, 31 | pm2.61dane 3029 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) = ∅) |
33 | 32 | uneq1d 4076 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝐴 “ (𝑆 ∖ {0})) ∪ (◡𝐴 “ {0})) = (∅ ∪ (◡𝐴 “ {0}))) |
34 | | undif1 4390 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ {0}) ∪ {0}) =
(𝑆 ∪
{0}) |
35 | 34 | imaeq2i 5927 |
. . . . . . . . 9
⊢ (◡𝐴 “ ((𝑆 ∖ {0}) ∪ {0})) = (◡𝐴 “ (𝑆 ∪ {0})) |
36 | | imaundi 6013 |
. . . . . . . . 9
⊢ (◡𝐴 “ ((𝑆 ∖ {0}) ∪ {0})) = ((◡𝐴 “ (𝑆 ∖ {0})) ∪ (◡𝐴 “ {0})) |
37 | 35, 36 | eqtr3i 2767 |
. . . . . . . 8
⊢ (◡𝐴 “ (𝑆 ∪ {0})) = ((◡𝐴 “ (𝑆 ∖ {0})) ∪ (◡𝐴 “ {0})) |
38 | | un0 4305 |
. . . . . . . . 9
⊢ ((◡𝐴 “ {0}) ∪ ∅) = (◡𝐴 “ {0}) |
39 | | uncom 4067 |
. . . . . . . . 9
⊢ ((◡𝐴 “ {0}) ∪ ∅) = (∅
∪ (◡𝐴 “ {0})) |
40 | 38, 39 | eqtr3i 2767 |
. . . . . . . 8
⊢ (◡𝐴 “ {0}) = (∅ ∪ (◡𝐴 “ {0})) |
41 | 33, 37, 40 | 3eqtr4g 2803 |
. . . . . . 7
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∪ {0})) = (◡𝐴 “ {0})) |
42 | 18, 41 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → dom 𝐴 = (◡𝐴 “ {0})) |
43 | | eqimss 3957 |
. . . . . 6
⊢ (dom
𝐴 = (◡𝐴 “ {0}) → dom 𝐴 ⊆ (◡𝐴 “ {0})) |
44 | 42, 43 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝐴 ⊆ (◡𝐴 “ {0})) |
45 | 12 | ffund 6549 |
. . . . . 6
⊢ (𝜑 → Fun 𝐴) |
46 | | ssid 3923 |
. . . . . 6
⊢ dom 𝐴 ⊆ dom 𝐴 |
47 | | funimass3 6874 |
. . . . . 6
⊢ ((Fun
𝐴 ∧ dom 𝐴 ⊆ dom 𝐴) → ((𝐴 “ dom 𝐴) ⊆ {0} ↔ dom 𝐴 ⊆ (◡𝐴 “ {0}))) |
48 | 45, 46, 47 | sylancl 589 |
. . . . 5
⊢ (𝜑 → ((𝐴 “ dom 𝐴) ⊆ {0} ↔ dom 𝐴 ⊆ (◡𝐴 “ {0}))) |
49 | 44, 48 | mpbird 260 |
. . . 4
⊢ (𝜑 → (𝐴 “ dom 𝐴) ⊆ {0}) |
50 | 14, 49 | eqsstrrid 3950 |
. . 3
⊢ (𝜑 → ran 𝐴 ⊆ {0}) |
51 | | df-f 6384 |
. . 3
⊢ (𝐴:ℕ0⟶{0}
↔ (𝐴 Fn
ℕ0 ∧ ran 𝐴 ⊆ {0})) |
52 | 13, 50, 51 | sylanbrc 586 |
. 2
⊢ (𝜑 → 𝐴:ℕ0⟶{0}) |
53 | | c0ex 10827 |
. . 3
⊢ 0 ∈
V |
54 | 53 | fconst2 7020 |
. 2
⊢ (𝐴:ℕ0⟶{0}
↔ 𝐴 =
(ℕ0 × {0})) |
55 | 52, 54 | sylib 221 |
1
⊢ (𝜑 → 𝐴 = (ℕ0 ×
{0})) |