MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plyeq0lem Structured version   Visualization version   GIF version

Theorem plyeq0lem 24786
Description: Lemma for plyeq0 24787. If 𝐴 is the coefficient function for a nonzero polynomial such that 𝑃(𝑧) = Σ𝑘 ∈ ℕ0𝐴(𝑘) · 𝑧𝑘 = 0 for every 𝑧 ∈ ℂ and 𝐴(𝑀) is the nonzero leading coefficient, then the function 𝐹(𝑧) = 𝑃(𝑧) / 𝑧𝑀 is a sum of powers of 1 / 𝑧, and so the limit of this function as 𝑧 ⇝ +∞ is the constant term, 𝐴(𝑀). But 𝐹(𝑧) = 0 everywhere, so this limit is also equal to zero so that 𝐴(𝑀) = 0, a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.)
Hypotheses
Ref Expression
plyeq0.1 (𝜑𝑆 ⊆ ℂ)
plyeq0.2 (𝜑𝑁 ∈ ℕ0)
plyeq0.3 (𝜑𝐴 ∈ ((𝑆 ∪ {0}) ↑m0))
plyeq0.4 (𝜑 → (𝐴 “ (ℤ‘(𝑁 + 1))) = {0})
plyeq0.5 (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))))
plyeq0.6 𝑀 = sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < )
plyeq0.7 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
Assertion
Ref Expression
plyeq0lem ¬ 𝜑
Distinct variable groups:   𝑧,𝑘,𝐴   𝑘,𝑀   𝑘,𝑁,𝑧   𝜑,𝑘,𝑧   𝑆,𝑘,𝑧
Allowed substitution hint:   𝑀(𝑧)

Proof of Theorem plyeq0lem
Dummy variables 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12260 . . . . . 6 ℕ = (ℤ‘1)
2 1zzd 11992 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 fzfid 13325 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
4 1zzd 11992 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5 plyeq0.3 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ((𝑆 ∪ {0}) ↑m0))
6 plyeq0.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ⊆ ℂ)
7 0cn 10611 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
87a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ∈ ℂ)
98snssd 4718 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {0} ⊆ ℂ)
106, 9unssd 4141 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11 cnex 10596 . . . . . . . . . . . . . . . . . . 19 ℂ ∈ V
12 ssexg 5203 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
1310, 11, 12sylancl 588 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 ∪ {0}) ∈ V)
14 nn0ex 11882 . . . . . . . . . . . . . . . . . 18 0 ∈ V
15 elmapg 8397 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
1613, 14, 15sylancl 588 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
175, 16mpbid 234 . . . . . . . . . . . . . . . 16 (𝜑𝐴:ℕ0⟶(𝑆 ∪ {0}))
1817, 10fssd 6504 . . . . . . . . . . . . . . 15 (𝜑𝐴:ℕ0⟶ℂ)
19 elfznn0 12984 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20 ffvelrn 6825 . . . . . . . . . . . . . . 15 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
2118, 19, 20syl2an 597 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
2221adantr 483 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴𝑘) ∈ ℂ)
2322abscld 14776 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴𝑘)) ∈ ℝ)
2423recnd 10647 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴𝑘)) ∈ ℂ)
25 divcnv 15188 . . . . . . . . . . 11 ((abs‘(𝐴𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) ⇝ 0)
2624, 25syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) ⇝ 0)
27 nnex 11622 . . . . . . . . . . . 12 ℕ ∈ V
2827mptex 6962 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ∈ V
2928a1i 11 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ∈ V)
30 oveq2 7141 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((abs‘(𝐴𝑘)) / 𝑛) = ((abs‘(𝐴𝑘)) / 𝑚))
31 eqid 2820 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))
32 ovex 7166 . . . . . . . . . . . . 13 ((abs‘(𝐴𝑘)) / 𝑚) ∈ V
3330, 31, 32fvmpt 6744 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) / 𝑚))
3433adantl 484 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) / 𝑚))
35 nndivre 11657 . . . . . . . . . . . 12 (((abs‘(𝐴𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) ∈ ℝ)
3623, 35sylan 582 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) ∈ ℝ)
3734, 36eqeltrd 2911 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38 oveq1 7140 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝑛↑(𝑘𝑀)) = (𝑚↑(𝑘𝑀)))
3938oveq2d 7149 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
40 eqid 2820 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))
41 ovex 7166 . . . . . . . . . . . . 13 ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ∈ V
4239, 40, 41fvmpt 6744 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
4342adantl 484 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
4421ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴𝑘) ∈ ℂ)
4544abscld 14776 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴𝑘)) ∈ ℝ)
46 nnrp 12379 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
4746adantl 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48 elfzelz 12892 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49 cnvimass 5925 . . . . . . . . . . . . . . . . . . 19 (𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
5049, 17fssdm 6506 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
51 plyeq0.6 . . . . . . . . . . . . . . . . . . 19 𝑀 = sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < )
52 nn0ssz 11982 . . . . . . . . . . . . . . . . . . . . 21 0 ⊆ ℤ
5350, 52sstrdi 3958 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
54 plyeq0.7 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
55 plyeq0.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑁 ∈ ℕ0)
5655nn0red 11935 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℝ)
5717ffnd 6491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐴 Fn ℕ0)
58 elpreima 6804 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 Fn ℕ0 → (𝑧 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴𝑧) ∈ (𝑆 ∖ {0}))))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑧 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴𝑧) ∈ (𝑆 ∖ {0}))))
6059simplbda 502 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → (𝐴𝑧) ∈ (𝑆 ∖ {0}))
61 eldifsni 4698 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑧) ∈ (𝑆 ∖ {0}) → (𝐴𝑧) ≠ 0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → (𝐴𝑧) ≠ 0)
63 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑧 → (𝐴𝑘) = (𝐴𝑧))
6463neeq1d 3065 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑧 → ((𝐴𝑘) ≠ 0 ↔ (𝐴𝑧) ≠ 0))
65 breq1 5045 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑧 → (𝑘𝑁𝑧𝑁))
6664, 65imbi12d 347 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑧 → (((𝐴𝑘) ≠ 0 → 𝑘𝑁) ↔ ((𝐴𝑧) ≠ 0 → 𝑧𝑁)))
67 plyeq0.4 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 “ (ℤ‘(𝑁 + 1))) = {0})
68 plyco0 24768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
6955, 18, 68syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
7067, 69mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
7170adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
7250sselda 3946 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
7366, 71, 72rspcdva 3604 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → ((𝐴𝑧) ≠ 0 → 𝑧𝑁))
7462, 73mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑧𝑁)
7574ralrimiva 3169 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁)
76 brralrspcev 5102 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
7756, 75, 76syl2anc 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
78 suprzcl 12041 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (𝐴 “ (𝑆 ∖ {0})))
7953, 54, 77, 78syl3anc 1367 . . . . . . . . . . . . . . . . . . 19 (𝜑 → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (𝐴 “ (𝑆 ∖ {0})))
8051, 79eqeltrid 2915 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})))
8150, 80sseldd 3947 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ0)
8281nn0zd 12064 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
83 zsubcl 12003 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘𝑀) ∈ ℤ)
8448, 82, 83syl2anr 598 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑘𝑀) ∈ ℤ)
8584ad2antrr 724 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ∈ ℤ)
8647, 85rpexpcld 13593 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℝ+)
8786rpred 12410 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℝ)
8845, 87remulcld 10649 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ∈ ℝ)
8943, 88eqeltrd 2911 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℝ)
90 nnrecre 11658 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
9190adantl 484 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
9222absge0d 14784 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴𝑘)))
9392adantr 483 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴𝑘)))
94 nnre 11623 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
9594adantl 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
96 nnge1 11644 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 1 ≤ 𝑚)
9796adantl 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
98 1red 10620 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
9985zred 12066 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ∈ ℝ)
100 simplr 767 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
10148adantl 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
102101ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
10382ad3antrrr 728 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
104 zltp1le 12011 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
105102, 103, 104syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
106100, 105mpbid 234 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
10719adantl 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
108107nn0red 11935 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
109108ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
11081adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
111110nn0red 11935 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
112111ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
113109, 98, 112leaddsub2d 11220 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀𝑘)))
114106, 113mpbid 234 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀𝑘))
115108recnd 10647 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
116115ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
117111recnd 10647 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
118117ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
119116, 118negsubdi2d 10991 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘𝑀) = (𝑀𝑘))
120114, 119breqtrrd 5070 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘𝑀))
12198, 99, 120lenegcon2d 11201 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ≤ -1)
122 neg1z 11997 . . . . . . . . . . . . . . . 16 -1 ∈ ℤ
123 eluz 12236 . . . . . . . . . . . . . . . 16 (((𝑘𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ‘(𝑘𝑀)) ↔ (𝑘𝑀) ≤ -1))
12485, 122, 123sylancl 588 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ‘(𝑘𝑀)) ↔ (𝑘𝑀) ≤ -1))
125121, 124mpbird 259 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ‘(𝑘𝑀)))
12695, 97, 125leexp2ad 13602 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ≤ (𝑚↑-1))
127 nncn 11624 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
128127adantl 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
129 expn1 13424 . . . . . . . . . . . . . 14 (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
130128, 129syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
131126, 130breqtrd 5068 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ≤ (1 / 𝑚))
13287, 91, 45, 93, 131lemul2ad 11558 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ≤ ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
13324adantr 483 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴𝑘)) ∈ ℂ)
134 nnne0 11650 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
135134adantl 484 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
136133, 128, 135divrecd 11397 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) = ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
13734, 136eqtrd 2855 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
138132, 43, 1373brtr4d 5074 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚))
13986rpge0d 12414 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘𝑀)))
14045, 87, 93, 139mulge0d 11195 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
141140, 43breqtrrd 5070 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚))
1421, 4, 26, 29, 37, 89, 138, 141climsqz2 14978 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ⇝ 0)
14327mptex 6962 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ∈ V
144143a1i 11 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ∈ V)
14538oveq2d 7149 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
146 eqid 2820 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))
147 ovex 7166 . . . . . . . . . . . . . . 15 ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) ∈ V
148145, 146, 147fvmpt 6744 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
149148ad2antlr 725 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
15018adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
151150, 19, 20syl2an 597 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
152127ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
153134ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
15482adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
15548, 154, 83syl2anr 598 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘𝑀) ∈ ℤ)
156152, 153, 155expclzd 13500 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘𝑀)) ∈ ℂ)
157151, 156mulcld 10639 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) ∈ ℂ)
158149, 157eqeltrd 2911 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
159158an32s 650 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
160159adantlr 713 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
16187recnd 10647 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℂ)
16244, 161absmuld 14794 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑚↑(𝑘𝑀)))))
16387, 139absidd 14762 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘𝑀))) = (𝑚↑(𝑘𝑀)))
164163oveq2d 7149 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (abs‘(𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
165162, 164eqtrd 2855 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
166148adantl 484 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
167166fveq2d 6650 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚)) = (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))))
168165, 167, 433eqtr4rd 2866 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚)))
1691, 4, 144, 29, 160, 168climabs0 14922 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ⇝ 0))
170142, 169mpbird 259 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ 0)
171108adantr 483 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
172 simpr 487 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
173171, 172ltned 10754 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘𝑀)
174 velsn 4559 . . . . . . . . . . 11 (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
175174necon3bbii 3053 . . . . . . . . . 10 𝑘 ∈ {𝑀} ↔ 𝑘𝑀)
176173, 175sylibr 236 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
177176iffalsed 4454 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = 0)
178170, 177breqtrrd 5070 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
179 nncn 11624 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
180179ad2antlr 725 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → 𝑛 ∈ ℂ)
181 nnne0 11650 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
182181ad2antlr 725 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → 𝑛 ≠ 0)
18384ad3antrrr 728 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝑘𝑀) ∈ ℤ)
184180, 182, 183expclzd 13500 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝑛↑(𝑘𝑀)) ∈ ℂ)
185184mul02d 10816 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (0 · (𝑛↑(𝑘𝑀))) = 0)
186 simpr 487 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝐴𝑘) = 0)
187186oveq1d 7148 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = (0 · (𝑛↑(𝑘𝑀))))
188186ifeq1d 4461 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
189 ifid 4482 . . . . . . . . . . . . 13 if(𝑘 ∈ {𝑀}, 0, 0) = 0
190188, 189syl6eq 2871 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = 0)
191185, 187, 1903eqtr4d 2865 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
19221adantr 483 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝐴𝑘) ∈ ℂ)
193192ad2antrr 724 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ ℂ)
194193mulid1d 10636 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · 1) = (𝐴𝑘))
195 nn0ssre 11880 . . . . . . . . . . . . . . . . . . . . . . 23 0 ⊆ ℝ
19650, 195sstrdi 3958 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
197196ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
19854ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
19977ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
20019ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
201 ffvelrn 6825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ (𝑆 ∪ {0}))
20217, 19, 201syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ (𝑆 ∪ {0}))
203202anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴𝑘) ≠ 0))
204 eldifsn 4695 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴𝑘) ≠ 0))
205203, 204sylibr 236 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
206 difun2 4405 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
207205, 206eleqtrdi 2921 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ (𝑆 ∖ {0}))
208 elpreima 6804 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 Fn ℕ0 → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
20957, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
210209ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
211200, 207, 210mpbir2and 711 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})))
212197, 198, 199, 211suprubd 11581 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ≤ sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
213212, 51breqtrrdi 5084 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
214213ad4ant14 750 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
215 simpllr 774 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀𝑘)
216108ad3antrrr 728 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ ℝ)
217111ad3antrrr 728 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀 ∈ ℝ)
218216, 217letri3d 10760 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘𝑀𝑀𝑘)))
219214, 215, 218mpbir2and 711 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 = 𝑀)
220219oveq1d 7148 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘𝑀) = (𝑀𝑀))
221117ad3antrrr 728 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀 ∈ ℂ)
222221subidd 10963 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑀𝑀) = 0)
223220, 222eqtrd 2855 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘𝑀) = 0)
224223oveq2d 7149 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑(𝑘𝑀)) = (𝑛↑0))
225179ad2antlr 725 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑛 ∈ ℂ)
226225exp0d 13489 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑0) = 1)
227224, 226eqtrd 2855 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑(𝑘𝑀)) = 1)
228227oveq2d 7149 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = ((𝐴𝑘) · 1))
229219, 174sylibr 236 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
230229iftrued 4451 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = (𝐴𝑘))
231194, 228, 2303eqtr4d 2865 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
232191, 231pm2.61dane 3093 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
233232mpteq2dva 5137 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)))
234 fconstmpt 5590 . . . . . . . . 9 (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
235233, 234syl6eqr 2873 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}))
236 ifcl 4487 . . . . . . . . . 10 (((𝐴𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ)
237192, 7, 236sylancl 588 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ)
238 1z 11991 . . . . . . . . 9 1 ∈ ℤ
2391eqimss2i 4005 . . . . . . . . . 10 (ℤ‘1) ⊆ ℕ
240239, 27climconst2 14885 . . . . . . . . 9 ((if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
241237, 238, 240sylancl 588 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
242235, 241eqbrtrd 5064 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
243178, 242, 108, 111ltlecasei 10726 . . . . . 6 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
244 snex 5308 . . . . . . . 8 {0} ∈ V
24527, 244xpex 7454 . . . . . . 7 (ℕ × {0}) ∈ V
246245a1i 11 . . . . . 6 (𝜑 → (ℕ × {0}) ∈ V)
247159anasss 469 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
248 plyeq0.5 . . . . . . . . . . . 12 (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))))
249248fveq1d 6648 . . . . . . . . . . 11 (𝜑 → (0𝑝𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚))
250249adantr 483 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (0𝑝𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚))
251127adantl 484 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
252 0pval 24254 . . . . . . . . . . 11 (𝑚 ∈ ℂ → (0𝑝𝑚) = 0)
253251, 252syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (0𝑝𝑚) = 0)
254 oveq1 7140 . . . . . . . . . . . . . 14 (𝑧 = 𝑚 → (𝑧𝑘) = (𝑚𝑘))
255254oveq2d 7149 . . . . . . . . . . . . 13 (𝑧 = 𝑚 → ((𝐴𝑘) · (𝑧𝑘)) = ((𝐴𝑘) · (𝑚𝑘)))
256255sumeq2sdv 15041 . . . . . . . . . . . 12 (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
257 eqid 2820 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))
258 sumex 15024 . . . . . . . . . . . 12 Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) ∈ V
259256, 257, 258fvmpt 6744 . . . . . . . . . . 11 (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
260251, 259syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
261250, 253, 2603eqtr3d 2863 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
262261oveq1d 7148 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (0 / (𝑚𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
263 expcl 13432 . . . . . . . . . 10 ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚𝑀) ∈ ℂ)
264127, 81, 263syl2anr 598 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑚𝑀) ∈ ℂ)
265134adantl 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ≠ 0)
266251, 265, 154expne0d 13501 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑚𝑀) ≠ 0)
267264, 266div0d 11393 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (0 / (𝑚𝑀)) = 0)
268 fzfid 13325 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
269 expcl 13432 . . . . . . . . . . 11 ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚𝑘) ∈ ℂ)
270251, 19, 269syl2an 597 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑘) ∈ ℂ)
271151, 270mulcld 10639 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚𝑘)) ∈ ℂ)
272268, 264, 271, 266fsumdivc 15121 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
273262, 267, 2723eqtr3d 2863 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
274 fvconst2g 6940 . . . . . . . 8 ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
2758, 274sylan 582 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
276154adantr 483 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
27748adantl 484 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
278152, 153, 276, 277expsubd 13506 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘𝑀)) = ((𝑚𝑘) / (𝑚𝑀)))
279278oveq2d 7149 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) = ((𝐴𝑘) · ((𝑚𝑘) / (𝑚𝑀))))
280264adantr 483 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑀) ∈ ℂ)
281266adantr 483 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑀) ≠ 0)
282151, 270, 280, 281divassd 11429 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)) = ((𝐴𝑘) · ((𝑚𝑘) / (𝑚𝑀))))
283279, 149, 2823eqtr4d 2865 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = (((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
284283sumeq2dv 15040 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
285273, 275, 2843eqtr4d 2865 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚))
2861, 2, 3, 243, 246, 247, 285climfsum 15155 . . . . 5 (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
287 suprleub 11585 . . . . . . . . . . . 12 ((((𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) ∧ 𝑁 ∈ ℝ) → (sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
288196, 54, 77, 56, 287syl31anc 1369 . . . . . . . . . . 11 (𝜑 → (sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
28975, 288mpbird 259 . . . . . . . . . 10 (𝜑 → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
29051, 289eqbrtrid 5077 . . . . . . . . 9 (𝜑𝑀𝑁)
291 nn0uz 12259 . . . . . . . . . . 11 0 = (ℤ‘0)
29281, 291eleqtrdi 2921 . . . . . . . . . 10 (𝜑𝑀 ∈ (ℤ‘0))
29355nn0zd 12064 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
294 elfz5 12884 . . . . . . . . . 10 ((𝑀 ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀𝑁))
295292, 293, 294syl2anc 586 . . . . . . . . 9 (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀𝑁))
296290, 295mpbird 259 . . . . . . . 8 (𝜑𝑀 ∈ (0...𝑁))
297296snssd 4718 . . . . . . 7 (𝜑 → {𝑀} ⊆ (0...𝑁))
29818, 81ffvelrnd 6828 . . . . . . . . 9 (𝜑 → (𝐴𝑀) ∈ ℂ)
299 elsni 4560 . . . . . . . . . . 11 (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
300299fveq2d 6650 . . . . . . . . . 10 (𝑘 ∈ {𝑀} → (𝐴𝑘) = (𝐴𝑀))
301300eleq1d 2895 . . . . . . . . 9 (𝑘 ∈ {𝑀} → ((𝐴𝑘) ∈ ℂ ↔ (𝐴𝑀) ∈ ℂ))
302298, 301syl5ibrcom 249 . . . . . . . 8 (𝜑 → (𝑘 ∈ {𝑀} → (𝐴𝑘) ∈ ℂ))
303302ralrimiv 3168 . . . . . . 7 (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴𝑘) ∈ ℂ)
3043olcd 870 . . . . . . 7 (𝜑 → ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin))
305 sumss2 15063 . . . . . . 7 ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
306297, 303, 304, 305syl21anc 835 . . . . . 6 (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
307 ltso 10699 . . . . . . . . 9 < Or ℝ
308307supex 8905 . . . . . . . 8 sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
30951, 308eqeltri 2907 . . . . . . 7 𝑀 ∈ V
310 fveq2 6646 . . . . . . . 8 (𝑘 = 𝑀 → (𝐴𝑘) = (𝐴𝑀))
311310sumsn 15081 . . . . . . 7 ((𝑀 ∈ V ∧ (𝐴𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = (𝐴𝑀))
312309, 298, 311sylancr 589 . . . . . 6 (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = (𝐴𝑀))
313306, 312eqtr3d 2857 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = (𝐴𝑀))
314286, 313breqtrd 5068 . . . 4 (𝜑 → (ℕ × {0}) ⇝ (𝐴𝑀))
315239, 27climconst2 14885 . . . . 5 ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
3167, 238, 315mp2an 690 . . . 4 (ℕ × {0}) ⇝ 0
317 climuni 14889 . . . 4 (((ℕ × {0}) ⇝ (𝐴𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴𝑀) = 0)
318314, 316, 317sylancl 588 . . 3 (𝜑 → (𝐴𝑀) = 0)
319 fvex 6659 . . . 4 (𝐴𝑀) ∈ V
320319elsn 4558 . . 3 ((𝐴𝑀) ∈ {0} ↔ (𝐴𝑀) = 0)
321318, 320sylibr 236 . 2 (𝜑 → (𝐴𝑀) ∈ {0})
322 elpreima 6804 . . . . . 6 (𝐴 Fn ℕ0 → (𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0}))))
32357, 322syl 17 . . . . 5 (𝜑 → (𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0}))))
32480, 323mpbid 234 . . . 4 (𝜑 → (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0})))
325324simprd 498 . . 3 (𝜑 → (𝐴𝑀) ∈ (𝑆 ∖ {0}))
326325eldifbd 3926 . 2 (𝜑 → ¬ (𝐴𝑀) ∈ {0})
327321, 326pm2.65i 196 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   = wceq 1537  wcel 2114  wne 3006  wral 3125  wrex 3126  Vcvv 3473  cdif 3910  cun 3911  wss 3913  c0 4269  ifcif 4443  {csn 4543   class class class wbr 5042  cmpt 5122   × cxp 5529  ccnv 5530  cima 5534   Fn wfn 6326  wf 6327  cfv 6331  (class class class)co 7133  m cmap 8384  Fincfn 8487  supcsup 8882  cc 10513  cr 10514  0cc0 10515  1c1 10516   + caddc 10518   · cmul 10520   < clt 10653  cle 10654  cmin 10848  -cneg 10849   / cdiv 11275  cn 11616  0cn0 11876  cz 11960  cuz 12222  +crp 12368  ...cfz 12876  cexp 13414  abscabs 14573  cli 14821  Σcsu 15022  0𝑝c0p 24252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593  ax-addf 10594
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-map 8386  df-pm 8387  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-sup 8884  df-inf 8885  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-n0 11877  df-z 11961  df-uz 12223  df-rp 12369  df-fz 12877  df-fzo 13018  df-fl 13146  df-seq 13354  df-exp 13415  df-hash 13676  df-cj 14438  df-re 14439  df-im 14440  df-sqrt 14574  df-abs 14575  df-clim 14825  df-rlim 14826  df-sum 15023  df-0p 24253
This theorem is referenced by:  plyeq0  24787
  Copyright terms: Public domain W3C validator