Step | Hyp | Ref
| Expression |
1 | | nnuz 12012 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11743 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | fzfid 13074 |
. . . . . 6
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
4 | | 1zzd 11743 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ) |
5 | | plyeq0.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)) |
6 | | plyeq0.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
7 | | 0cn 10355 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ∈
ℂ) |
9 | 8 | snssd 4560 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {0} ⊆
ℂ) |
10 | 6, 9 | unssd 4018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
11 | | cnex 10340 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℂ
∈ V |
12 | | ssexg 5031 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
13 | 10, 11, 12 | sylancl 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V) |
14 | | nn0ex 11632 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 ∈ V |
15 | | elmapg 8140 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
16 | 13, 14, 15 | sylancl 580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
17 | 5, 16 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
18 | 17, 10 | fssd 6296 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
19 | | elfznn0 12734 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
20 | | ffvelrn 6611 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
21 | 18, 19, 20 | syl2an 589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
22 | 21 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴‘𝑘) ∈ ℂ) |
23 | 22 | abscld 14559 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℝ) |
24 | 23 | recnd 10392 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℂ) |
25 | | divcnv 14966 |
. . . . . . . . . . 11
⊢
((abs‘(𝐴‘𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0) |
27 | | nnex 11364 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
28 | 27 | mptex 6747 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V |
29 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V) |
30 | | oveq2 6918 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) / 𝑛) = ((abs‘(𝐴‘𝑘)) / 𝑚)) |
31 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
((abs‘(𝐴‘𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) |
32 | | ovex 6942 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝐴‘𝑘)) / 𝑚) ∈ V |
33 | 30, 31, 32 | fvmpt 6533 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚)) |
34 | 33 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚)) |
35 | | nndivre 11399 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐴‘𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ) |
36 | 23, 35 | sylan 575 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ) |
37 | 34, 36 | eqeltrd 2906 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) ∈ ℝ) |
38 | | oveq1 6917 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝑛↑(𝑘 − 𝑀)) = (𝑚↑(𝑘 − 𝑀))) |
39 | 38 | oveq2d 6926 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀)))) |
40 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) |
41 | | ovex 6942 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ V |
42 | 39, 40, 41 | fvmpt 6533 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀)))) |
43 | 42 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀)))) |
44 | 21 | ad2antrr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴‘𝑘) ∈ ℂ) |
45 | 44 | abscld 14559 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℝ) |
46 | | nnrp 12132 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
47 | 46 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+) |
48 | | elfzelz 12642 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
49 | | cnvimass 5730 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴 |
50 | 49, 17 | fssdm 6298 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆
ℕ0) |
51 | | plyeq0.6 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, <
) |
52 | | nn0ssz 11733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
ℕ0 ⊆ ℤ |
53 | 50, 52 | syl6ss 3839 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆
ℤ) |
54 | | plyeq0.7 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠
∅) |
55 | | plyeq0.2 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
56 | 55 | nn0red 11686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℝ) |
57 | 17 | ffnd 6283 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐴 Fn ℕ0) |
58 | | elpreima 6591 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 Fn ℕ0 →
(𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0})))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0})))) |
60 | 59 | simplbda 495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ∈ (𝑆 ∖ {0})) |
61 | | eldifsni 4542 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴‘𝑧) ∈ (𝑆 ∖ {0}) → (𝐴‘𝑧) ≠ 0) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ≠ 0) |
63 | | fveq2 6437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑧 → (𝐴‘𝑘) = (𝐴‘𝑧)) |
64 | 63 | neeq1d 3058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑧 → ((𝐴‘𝑘) ≠ 0 ↔ (𝐴‘𝑧) ≠ 0)) |
65 | | breq1 4878 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑧 → (𝑘 ≤ 𝑁 ↔ 𝑧 ≤ 𝑁)) |
66 | 64, 65 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑧 → (((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁))) |
67 | | plyeq0.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
68 | | plyco0 24354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
69 | 55, 18, 68 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
70 | 67, 69 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
71 | 70 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
72 | 50 | sselda 3827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0) |
73 | 66, 71, 72 | rspcdva 3532 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁)) |
74 | 62, 73 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ≤ 𝑁) |
75 | 74 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁) |
76 | | brralrspcev 4935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℝ ∧
∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) |
77 | 56, 75, 76 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) |
78 | | suprzcl 11792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈
(◡𝐴 “ (𝑆 ∖ {0}))) |
79 | 53, 54, 77, 78 | syl3anc 1494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈
(◡𝐴 “ (𝑆 ∖ {0}))) |
80 | 51, 79 | syl5eqel 2910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) |
81 | 50, 80 | sseldd 3828 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
82 | 81 | nn0zd 11815 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℤ) |
83 | | zsubcl 11754 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 − 𝑀) ∈ ℤ) |
84 | 48, 82, 83 | syl2anr 590 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ) |
85 | 84 | ad2antrr 717 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℤ) |
86 | 47, 85 | rpexpcld 13335 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈
ℝ+) |
87 | 86 | rpred 12163 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ) |
88 | 45, 87 | remulcld 10394 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ ℝ) |
89 | 43, 88 | eqeltrd 2906 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℝ) |
90 | | nnrecre 11400 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → (1 /
𝑚) ∈
ℝ) |
91 | 90 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈
ℝ) |
92 | 22 | absge0d 14567 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴‘𝑘))) |
93 | 92 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤
(abs‘(𝐴‘𝑘))) |
94 | | nnre 11365 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
95 | 94 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ) |
96 | | nnge1 11387 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 1 ≤
𝑚) |
97 | 96 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚) |
98 | | 1red 10364 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈
ℝ) |
99 | 85 | zred 11817 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℝ) |
100 | | simplr 785 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀) |
101 | 48 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ) |
102 | 101 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ) |
103 | 82 | ad3antrrr 721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ) |
104 | | zltp1le 11762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀)) |
105 | 102, 103,
104 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀)) |
106 | 100, 105 | mpbid 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀) |
107 | 19 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
108 | 107 | nn0red 11686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ) |
109 | 108 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ) |
110 | 81 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈
ℕ0) |
111 | 110 | nn0red 11686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ) |
112 | 111 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ) |
113 | 109, 98, 112 | leaddsub2d 10961 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀 − 𝑘))) |
114 | 106, 113 | mpbid 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀 − 𝑘)) |
115 | 108 | recnd 10392 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) |
116 | 115 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ) |
117 | 111 | recnd 10392 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ) |
118 | 117 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ) |
119 | 116, 118 | negsubdi2d 10736 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘 − 𝑀) = (𝑀 − 𝑘)) |
120 | 114, 119 | breqtrrd 4903 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘 − 𝑀)) |
121 | 98, 99, 120 | lenegcon2d 10942 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ≤ -1) |
122 | | neg1z 11748 |
. . . . . . . . . . . . . . . 16
⊢ -1 ∈
ℤ |
123 | | eluz 11989 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 − 𝑀) ∈ ℤ ∧ -1 ∈ ℤ)
→ (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1)) |
124 | 85, 122, 123 | sylancl 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈
(ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1)) |
125 | 121, 124 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈
(ℤ≥‘(𝑘 − 𝑀))) |
126 | 95, 97, 125 | leexp2ad 13344 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (𝑚↑-1)) |
127 | | nncn 11366 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
128 | 127 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
129 | | expn1 13171 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚)) |
131 | 126, 130 | breqtrd 4901 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (1 / 𝑚)) |
132 | 87, 91, 45, 93, 131 | lemul2ad 11301 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ≤ ((abs‘(𝐴‘𝑘)) · (1 / 𝑚))) |
133 | 24 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℂ) |
134 | | nnne0 11393 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0) |
135 | 134 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0) |
136 | 133, 128,
135 | divrecd 11137 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚))) |
137 | 34, 136 | eqtrd 2861 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚))) |
138 | 132, 43, 137 | 3brtr4d 4907 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚)) |
139 | 86 | rpge0d 12167 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘 − 𝑀))) |
140 | 45, 87, 93, 139 | mulge0d 10936 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤
((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀)))) |
141 | 140, 43 | breqtrrd 4903 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦
((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) |
142 | 1, 4, 26, 29, 37, 89, 138, 141 | climsqz2 14756 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0) |
143 | 27 | mptex 6747 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V |
144 | 143 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V) |
145 | 38 | oveq2d 6926 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) |
146 | | eqid 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) |
147 | | ovex 6942 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ V |
148 | 145, 146,
147 | fvmpt 6533 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) |
149 | 148 | ad2antlr 718 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) |
150 | 18 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ) |
151 | 150, 19, 20 | syl2an 589 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
152 | 127 | ad2antlr 718 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ) |
153 | 134 | ad2antlr 718 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0) |
154 | 82 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ) |
155 | 48, 154, 83 | syl2anr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ) |
156 | 152, 153,
155 | expclzd 13314 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ) |
157 | 151, 156 | mulcld 10384 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ ℂ) |
158 | 149, 157 | eqeltrd 2906 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ) |
159 | 158 | an32s 642 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ) |
160 | 159 | adantlr 706 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ) |
161 | 87 | recnd 10392 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ) |
162 | 44, 161 | absmuld 14577 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀))))) |
163 | 87, 139 | absidd 14545 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘 − 𝑀))) = (𝑚↑(𝑘 − 𝑀))) |
164 | 163 | oveq2d 6926 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀)))) |
165 | 162, 164 | eqtrd 2861 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀)))) |
166 | 148 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) |
167 | 166 | fveq2d 6441 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) = (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))) |
168 | 165, 167,
43 | 3eqtr4rd 2872 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))) |
169 | 1, 4, 144, 29, 160, 168 | climabs0 14700 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)) |
170 | 142, 169 | mpbird 249 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0) |
171 | 108 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ) |
172 | | simpr 479 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀) |
173 | 171, 172 | ltned 10499 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ≠ 𝑀) |
174 | | velsn 4415 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀) |
175 | 174 | necon3bbii 3046 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ {𝑀} ↔ 𝑘 ≠ 𝑀) |
176 | 173, 175 | sylibr 226 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀}) |
177 | 176 | iffalsed 4319 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0) |
178 | 170, 177 | breqtrrd 4903 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
179 | | nncn 11366 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
180 | 179 | ad2antlr 718 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ∈ ℂ) |
181 | | nnne0 11393 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
182 | 181 | ad2antlr 718 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ≠ 0) |
183 | 84 | ad3antrrr 721 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑘 − 𝑀) ∈ ℤ) |
184 | 180, 182,
183 | expclzd 13314 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑛↑(𝑘 − 𝑀)) ∈ ℂ) |
185 | 184 | mul02d 10560 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (0 · (𝑛↑(𝑘 − 𝑀))) = 0) |
186 | | simpr 479 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0) |
187 | 186 | oveq1d 6925 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = (0 · (𝑛↑(𝑘 − 𝑀)))) |
188 | 186 | ifeq1d 4326 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0)) |
189 | | ifid 4347 |
. . . . . . . . . . . . 13
⊢ if(𝑘 ∈ {𝑀}, 0, 0) = 0 |
190 | 188, 189 | syl6eq 2877 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0) |
191 | 185, 187,
190 | 3eqtr4d 2871 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
192 | 21 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝐴‘𝑘) ∈ ℂ) |
193 | 192 | ad2antrr 717 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ℂ) |
194 | 193 | mulid1d 10381 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · 1) = (𝐴‘𝑘)) |
195 | | nn0ssre 11629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
ℕ0 ⊆ ℝ |
196 | 50, 195 | syl6ss 3839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆
ℝ) |
197 | 196 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ⊆
ℝ) |
198 | 54 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ≠
∅) |
199 | 77 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) |
200 | 19 | ad2antlr 718 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℕ0) |
201 | | ffvelrn 6611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0)
→ (𝐴‘𝑘) ∈ (𝑆 ∪ {0})) |
202 | 17, 19, 201 | syl2an 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0})) |
203 | 202 | anim1i 608 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0)) |
204 | | eldifsn 4538 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0)) |
205 | 203, 204 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0})) |
206 | | difun2 4273 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∪ {0}) ∖ {0}) =
(𝑆 ∖
{0}) |
207 | 205, 206 | syl6eleq 2916 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ (𝑆 ∖ {0})) |
208 | | elpreima 6591 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 Fn ℕ0 →
(𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0})))) |
209 | 57, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0})))) |
210 | 209 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0})))) |
211 | 200, 207,
210 | mpbir2and 704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) |
212 | | suprub 11321 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) ∧ 𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑘 ≤ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, <
)) |
213 | 197, 198,
199, 211, 212 | syl31anc 1496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, <
)) |
214 | 213, 51 | syl6breqr 4917 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀) |
215 | 214 | adantlr 706 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀) |
216 | 215 | adantlr 706 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀) |
217 | | simpllr 793 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ≤ 𝑘) |
218 | 108 | ad3antrrr 721 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℝ) |
219 | 111 | ad3antrrr 721 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℝ) |
220 | 218, 219 | letri3d 10505 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘))) |
221 | 216, 217,
220 | mpbir2and 704 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 = 𝑀) |
222 | 221 | oveq1d 6925 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = (𝑀 − 𝑀)) |
223 | 117 | ad3antrrr 721 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℂ) |
224 | 223 | subidd 10708 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑀 − 𝑀) = 0) |
225 | 222, 224 | eqtrd 2861 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = 0) |
226 | 225 | oveq2d 6926 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = (𝑛↑0)) |
227 | 179 | ad2antlr 718 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑛 ∈ ℂ) |
228 | 227 | exp0d 13303 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑0) = 1) |
229 | 226, 228 | eqtrd 2861 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = 1) |
230 | 229 | oveq2d 6926 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · 1)) |
231 | 221, 174 | sylibr 226 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ {𝑀}) |
232 | 231 | iftrued 4316 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑘)) |
233 | 194, 230,
232 | 3eqtr4d 2871 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
234 | 191, 233 | pm2.61dane 3086 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
235 | 234 | mpteq2dva 4969 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))) |
236 | | fconstmpt 5402 |
. . . . . . . . 9
⊢ (ℕ
× {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
237 | 235, 236 | syl6eqr 2879 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)})) |
238 | | ifcl 4352 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑘) ∈ ℂ ∧ 0 ∈ ℂ)
→ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ) |
239 | 192, 7, 238 | sylancl 580 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ) |
240 | | 1z 11742 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
241 | 1 | eqimss2i 3885 |
. . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℕ |
242 | 241, 27 | climconst2 14663 |
. . . . . . . . 9
⊢
((if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ)
→ (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
243 | 239, 240,
242 | sylancl 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
244 | 237, 243 | eqbrtrd 4897 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
245 | 178, 244,
108, 111 | ltlecasei 10471 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
246 | | snex 5131 |
. . . . . . . 8
⊢ {0}
∈ V |
247 | 27, 246 | xpex 7228 |
. . . . . . 7
⊢ (ℕ
× {0}) ∈ V |
248 | 247 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (ℕ × {0})
∈ V) |
249 | 159 | anasss 460 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ) |
250 | | plyeq0.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
251 | 250 | fveq1d 6439 |
. . . . . . . . . . 11
⊢ (𝜑 →
(0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚)) |
252 | 251 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚)) |
253 | 127 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
254 | | 0pval 23844 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℂ →
(0𝑝‘𝑚) = 0) |
255 | 253, 254 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝‘𝑚) = 0) |
256 | | oveq1 6917 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑚 → (𝑧↑𝑘) = (𝑚↑𝑘)) |
257 | 256 | oveq2d 6926 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑚 → ((𝐴‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑚↑𝑘))) |
258 | 257 | sumeq2sdv 14819 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘))) |
259 | | eqid 2825 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) |
260 | | sumex 14802 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈
(0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ V |
261 | 258, 259,
260 | fvmpt 6533 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘))) |
262 | 253, 261 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘))) |
263 | 252, 255,
262 | 3eqtr3d 2869 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘))) |
264 | 263 | oveq1d 6925 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀))) |
265 | | expcl 13179 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝑚↑𝑀) ∈
ℂ) |
266 | 127, 81, 265 | syl2anr 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ∈ ℂ) |
267 | 134 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0) |
268 | 253, 267,
154 | expne0d 13315 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ≠ 0) |
269 | 266, 268 | div0d 11133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = 0) |
270 | | fzfid 13074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin) |
271 | | expcl 13179 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑚↑𝑘) ∈
ℂ) |
272 | 253, 19, 271 | syl2an 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑘) ∈ ℂ) |
273 | 151, 272 | mulcld 10384 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ ℂ) |
274 | 270, 266,
273, 268 | fsumdivc 14899 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀))) |
275 | 264, 269,
274 | 3eqtr3d 2869 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀))) |
276 | | fvconst2g 6728 |
. . . . . . . 8
⊢ ((0
∈ ℂ ∧ 𝑚
∈ ℕ) → ((ℕ × {0})‘𝑚) = 0) |
277 | 8, 276 | sylan 575 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ ×
{0})‘𝑚) =
0) |
278 | 154 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ) |
279 | 48 | adantl 475 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ) |
280 | 152, 153,
278, 279 | expsubd 13320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) = ((𝑚↑𝑘) / (𝑚↑𝑀))) |
281 | 280 | oveq2d 6926 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀)))) |
282 | 266 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ∈ ℂ) |
283 | 268 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ≠ 0) |
284 | 151, 272,
282, 283 | divassd 11169 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀)))) |
285 | 281, 149,
284 | 3eqtr4d 2871 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀))) |
286 | 285 | sumeq2dv 14817 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀))) |
287 | 275, 277,
286 | 3eqtr4d 2871 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ ×
{0})‘𝑚) =
Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) |
288 | 1, 2, 3, 245, 248, 249, 287 | climfsum 14933 |
. . . . 5
⊢ (𝜑 → (ℕ × {0})
⇝ Σ𝑘 ∈
(0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
289 | | suprleub 11326 |
. . . . . . . . . . . 12
⊢ ((((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) ∧ 𝑁 ∈ ℝ) → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁)) |
290 | 196, 54, 77, 56, 289 | syl31anc 1496 |
. . . . . . . . . . 11
⊢ (𝜑 → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁)) |
291 | 75, 290 | mpbird 249 |
. . . . . . . . . 10
⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁) |
292 | 51, 291 | syl5eqbr 4910 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
293 | | nn0uz 12011 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
294 | 81, 293 | syl6eleq 2916 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
295 | 55 | nn0zd 11815 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
296 | | elfz5 12634 |
. . . . . . . . . 10
⊢ ((𝑀 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁)) |
297 | 294, 295,
296 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁)) |
298 | 292, 297 | mpbird 249 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (0...𝑁)) |
299 | 298 | snssd 4560 |
. . . . . . 7
⊢ (𝜑 → {𝑀} ⊆ (0...𝑁)) |
300 | 18, 81 | ffvelrnd 6614 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ) |
301 | | elsni 4416 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑀} → 𝑘 = 𝑀) |
302 | 301 | fveq2d 6441 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑀} → (𝐴‘𝑘) = (𝐴‘𝑀)) |
303 | 302 | eleq1d 2891 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑀} → ((𝐴‘𝑘) ∈ ℂ ↔ (𝐴‘𝑀) ∈ ℂ)) |
304 | 300, 303 | syl5ibrcom 239 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ {𝑀} → (𝐴‘𝑘) ∈ ℂ)) |
305 | 304 | ralrimiv 3174 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ) |
306 | 3 | olcd 905 |
. . . . . . 7
⊢ (𝜑 → ((0...𝑁) ⊆ (ℤ≥‘0)
∨ (0...𝑁) ∈
Fin)) |
307 | | sumss2 14841 |
. . . . . . 7
⊢ ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
308 | 299, 305,
306, 307 | syl21anc 871 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)) |
309 | | ltso 10444 |
. . . . . . . . 9
⊢ < Or
ℝ |
310 | 309 | supex 8644 |
. . . . . . . 8
⊢
sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈
V |
311 | 51, 310 | eqeltri 2902 |
. . . . . . 7
⊢ 𝑀 ∈ V |
312 | | fveq2 6437 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐴‘𝑘) = (𝐴‘𝑀)) |
313 | 312 | sumsn 14859 |
. . . . . . 7
⊢ ((𝑀 ∈ V ∧ (𝐴‘𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀)) |
314 | 311, 300,
313 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀)) |
315 | 308, 314 | eqtr3d 2863 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑀)) |
316 | 288, 315 | breqtrd 4901 |
. . . 4
⊢ (𝜑 → (ℕ × {0})
⇝ (𝐴‘𝑀)) |
317 | 241, 27 | climconst2 14663 |
. . . . 5
⊢ ((0
∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝
0) |
318 | 7, 240, 317 | mp2an 683 |
. . . 4
⊢ (ℕ
× {0}) ⇝ 0 |
319 | | climuni 14667 |
. . . 4
⊢
(((ℕ × {0}) ⇝ (𝐴‘𝑀) ∧ (ℕ × {0}) ⇝ 0)
→ (𝐴‘𝑀) = 0) |
320 | 316, 318,
319 | sylancl 580 |
. . 3
⊢ (𝜑 → (𝐴‘𝑀) = 0) |
321 | | fvex 6450 |
. . . 4
⊢ (𝐴‘𝑀) ∈ V |
322 | 321 | elsn 4414 |
. . 3
⊢ ((𝐴‘𝑀) ∈ {0} ↔ (𝐴‘𝑀) = 0) |
323 | 320, 322 | sylibr 226 |
. 2
⊢ (𝜑 → (𝐴‘𝑀) ∈ {0}) |
324 | | elpreima 6591 |
. . . . . 6
⊢ (𝐴 Fn ℕ0 →
(𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0})))) |
325 | 57, 324 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0})))) |
326 | 80, 325 | mpbid 224 |
. . . 4
⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))) |
327 | 326 | simprd 491 |
. . 3
⊢ (𝜑 → (𝐴‘𝑀) ∈ (𝑆 ∖ {0})) |
328 | 327 | eldifbd 3811 |
. 2
⊢ (𝜑 → ¬ (𝐴‘𝑀) ∈ {0}) |
329 | 323, 328 | pm2.65i 186 |
1
⊢ ¬
𝜑 |