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

Theorem plyeq0lem 23684
Description: Lemma for plyeq0 23685. 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}) ↑𝑚0))
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 11552 . . . . . 6 ℕ = (ℤ‘1)
2 1zzd 11238 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 fzfid 12586 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
4 1zzd 11238 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5 plyeq0.3 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚0))
6 plyeq0.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ⊆ ℂ)
7 0cn 9885 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
87a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ∈ ℂ)
98snssd 4277 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {0} ⊆ ℂ)
106, 9unssd 3747 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11 cnex 9870 . . . . . . . . . . . . . . . . . . 19 ℂ ∈ V
12 ssexg 4724 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
1310, 11, 12sylancl 692 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 ∪ {0}) ∈ V)
14 nn0ex 11142 . . . . . . . . . . . . . . . . . 18 0 ∈ V
15 elmapg 7731 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
1613, 14, 15sylancl 692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
175, 16mpbid 220 . . . . . . . . . . . . . . . 16 (𝜑𝐴:ℕ0⟶(𝑆 ∪ {0}))
1817, 10fssd 5953 . . . . . . . . . . . . . . 15 (𝜑𝐴:ℕ0⟶ℂ)
19 elfznn0 12254 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20 ffvelrn 6247 . . . . . . . . . . . . . . 15 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
2118, 19, 20syl2an 492 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
2221adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴𝑘) ∈ ℂ)
2322abscld 13966 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴𝑘)) ∈ ℝ)
2423recnd 9921 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴𝑘)) ∈ ℂ)
25 divcnv 14367 . . . . . . . . . . 11 ((abs‘(𝐴𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) ⇝ 0)
2624, 25syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) ⇝ 0)
27 nnex 10870 . . . . . . . . . . . 12 ℕ ∈ V
2827mptex 6365 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ∈ V
2928a1i 11 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ∈ V)
30 oveq2 6532 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((abs‘(𝐴𝑘)) / 𝑛) = ((abs‘(𝐴𝑘)) / 𝑚))
31 eqid 2606 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))
32 ovex 6552 . . . . . . . . . . . . 13 ((abs‘(𝐴𝑘)) / 𝑚) ∈ V
3330, 31, 32fvmpt 6173 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) / 𝑚))
3433adantl 480 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) / 𝑚))
35 nndivre 10900 . . . . . . . . . . . 12 (((abs‘(𝐴𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) ∈ ℝ)
3623, 35sylan 486 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) ∈ ℝ)
3734, 36eqeltrd 2684 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38 oveq1 6531 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝑛↑(𝑘𝑀)) = (𝑚↑(𝑘𝑀)))
3938oveq2d 6540 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
40 eqid 2606 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))
41 ovex 6552 . . . . . . . . . . . . 13 ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ∈ V
4239, 40, 41fvmpt 6173 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
4342adantl 480 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
4421ad2antrr 757 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴𝑘) ∈ ℂ)
4544abscld 13966 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴𝑘)) ∈ ℝ)
46 nnrp 11671 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
4746adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48 elfzelz 12165 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49 cnvimass 5388 . . . . . . . . . . . . . . . . . . 19 (𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
50 fdm 5947 . . . . . . . . . . . . . . . . . . . 20 (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 = ℕ0)
5117, 50syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝐴 = ℕ0)
5249, 51syl5sseq 3612 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
53 plyeq0.6 . . . . . . . . . . . . . . . . . . 19 𝑀 = sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < )
54 nn0ssz 11228 . . . . . . . . . . . . . . . . . . . . 21 0 ⊆ ℤ
5552, 54syl6ss 3576 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
56 plyeq0.7 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
57 plyeq0.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑁 ∈ ℕ0)
5857nn0red 11196 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℝ)
5952sselda 3564 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
60 plyeq0.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 “ (ℤ‘(𝑁 + 1))) = {0})
61 plyco0 23666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
6257, 18, 61syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
6360, 62mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
6463adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
65 ffn 5941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴:ℕ0⟶(𝑆 ∪ {0}) → 𝐴 Fn ℕ0)
6617, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐴 Fn ℕ0)
67 elpreima 6227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 Fn ℕ0 → (𝑧 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴𝑧) ∈ (𝑆 ∖ {0}))))
6866, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑧 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴𝑧) ∈ (𝑆 ∖ {0}))))
6968simplbda 651 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → (𝐴𝑧) ∈ (𝑆 ∖ {0}))
70 eldifsni 4257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑧) ∈ (𝑆 ∖ {0}) → (𝐴𝑧) ≠ 0)
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → (𝐴𝑧) ≠ 0)
72 fveq2 6085 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑧 → (𝐴𝑘) = (𝐴𝑧))
7372neeq1d 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑧 → ((𝐴𝑘) ≠ 0 ↔ (𝐴𝑧) ≠ 0))
74 breq1 4577 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑧 → (𝑘𝑁𝑧𝑁))
7573, 74imbi12d 332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑧 → (((𝐴𝑘) ≠ 0 → 𝑘𝑁) ↔ ((𝐴𝑧) ≠ 0 → 𝑧𝑁)))
7675rspcv 3274 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℕ0 → (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) → ((𝐴𝑧) ≠ 0 → 𝑧𝑁)))
7759, 64, 71, 76syl3c 63 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑧𝑁)
7877ralrimiva 2945 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁)
79 breq2 4578 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑁 → (𝑧𝑥𝑧𝑁))
8079ralbidv 2965 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑁 → (∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
8180rspcev 3278 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
8258, 78, 81syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
83 suprzcl 11286 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (𝐴 “ (𝑆 ∖ {0})))
8455, 56, 82, 83syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 (𝜑 → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (𝐴 “ (𝑆 ∖ {0})))
8553, 84syl5eqel 2688 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})))
8652, 85sseldd 3565 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ0)
8786nn0zd 11309 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
88 zsubcl 11249 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘𝑀) ∈ ℤ)
8948, 87, 88syl2anr 493 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑘𝑀) ∈ ℤ)
9089ad2antrr 757 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ∈ ℤ)
9147, 90rpexpcld 12846 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℝ+)
9291rpred 11701 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℝ)
9345, 92remulcld 9923 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ∈ ℝ)
9443, 93eqeltrd 2684 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℝ)
95 nnrecre 10901 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
9695adantl 480 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
9722absge0d 13974 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴𝑘)))
9897adantr 479 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴𝑘)))
99 nnre 10871 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
10099adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
101 nnge1 10890 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 1 ≤ 𝑚)
102101adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
103 1red 9908 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
10490zred 11311 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ∈ ℝ)
105 simplr 787 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
10648adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
107106ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
10887ad3antrrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
109 zltp1le 11257 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
110107, 108, 109syl2anc 690 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
111105, 110mpbid 220 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
11219adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
113112nn0red 11196 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
114113ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
11586adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
116115nn0red 11196 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
117116ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
118114, 103, 117leaddsub2d 10475 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀𝑘)))
119111, 118mpbid 220 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀𝑘))
120113recnd 9921 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
121120ad2antrr 757 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
122116recnd 9921 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
123122ad2antrr 757 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
124121, 123negsubdi2d 10256 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘𝑀) = (𝑀𝑘))
125119, 124breqtrrd 4602 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘𝑀))
126103, 104, 125lenegcon2d 10456 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ≤ -1)
127 neg1z 11243 . . . . . . . . . . . . . . . 16 -1 ∈ ℤ
128 eluz 11530 . . . . . . . . . . . . . . . 16 (((𝑘𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ‘(𝑘𝑀)) ↔ (𝑘𝑀) ≤ -1))
12990, 127, 128sylancl 692 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ‘(𝑘𝑀)) ↔ (𝑘𝑀) ≤ -1))
130126, 129mpbird 245 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ‘(𝑘𝑀)))
131100, 102, 130leexp2ad 12855 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ≤ (𝑚↑-1))
132 nncn 10872 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
133132adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
134 expn1 12684 . . . . . . . . . . . . . 14 (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
135133, 134syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
136131, 135breqtrd 4600 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ≤ (1 / 𝑚))
13792, 96, 45, 98, 136lemul2ad 10810 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ≤ ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
13824adantr 479 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴𝑘)) ∈ ℂ)
139 nnne0 10897 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
140139adantl 480 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
141138, 133, 140divrecd 10650 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) = ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
14234, 141eqtrd 2640 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
143137, 43, 1423brtr4d 4606 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚))
14491rpge0d 11705 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘𝑀)))
14545, 92, 98, 144mulge0d 10450 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
146145, 43breqtrrd 4602 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚))
1471, 4, 26, 29, 37, 94, 143, 146climsqz2 14163 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ⇝ 0)
14827mptex 6365 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ∈ V
149148a1i 11 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ∈ V)
15038oveq2d 6540 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
151 eqid 2606 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))
152 ovex 6552 . . . . . . . . . . . . . . 15 ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) ∈ V
153150, 151, 152fvmpt 6173 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
154153ad2antlr 758 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
15518adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
156155, 19, 20syl2an 492 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
157132ad2antlr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
158139ad2antlr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
15987adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
16048, 159, 88syl2anr 493 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘𝑀) ∈ ℤ)
161157, 158, 160expclzd 12827 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘𝑀)) ∈ ℂ)
162156, 161mulcld 9913 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) ∈ ℂ)
163154, 162eqeltrd 2684 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
164163an32s 841 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
165164adantlr 746 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
16692recnd 9921 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℂ)
16744, 166absmuld 13984 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑚↑(𝑘𝑀)))))
16892, 144absidd 13952 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘𝑀))) = (𝑚↑(𝑘𝑀)))
169168oveq2d 6540 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (abs‘(𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
170167, 169eqtrd 2640 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
171153adantl 480 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
172171fveq2d 6089 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚)) = (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))))
173170, 172, 433eqtr4rd 2651 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚)))
1741, 4, 149, 29, 165, 173climabs0 14107 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ⇝ 0))
175147, 174mpbird 245 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ 0)
176113adantr 479 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
177 simpr 475 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
178176, 177ltned 10021 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘𝑀)
179 velsn 4137 . . . . . . . . . . 11 (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
180179necon3bbii 2825 . . . . . . . . . 10 𝑘 ∈ {𝑀} ↔ 𝑘𝑀)
181178, 180sylibr 222 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
182181iffalsed 4043 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = 0)
183175, 182breqtrrd 4602 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
184 nncn 10872 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
185184ad2antlr 758 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → 𝑛 ∈ ℂ)
186 nnne0 10897 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
187186ad2antlr 758 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → 𝑛 ≠ 0)
18889ad3antrrr 761 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝑘𝑀) ∈ ℤ)
189185, 187, 188expclzd 12827 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝑛↑(𝑘𝑀)) ∈ ℂ)
190189mul02d 10082 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (0 · (𝑛↑(𝑘𝑀))) = 0)
191 simpr 475 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝐴𝑘) = 0)
192191oveq1d 6539 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = (0 · (𝑛↑(𝑘𝑀))))
193191ifeq1d 4050 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
194 ifid 4071 . . . . . . . . . . . . 13 if(𝑘 ∈ {𝑀}, 0, 0) = 0
195193, 194syl6eq 2656 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = 0)
196190, 192, 1953eqtr4d 2650 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
19721adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝐴𝑘) ∈ ℂ)
198197ad2antrr 757 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ ℂ)
199198mulid1d 9910 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · 1) = (𝐴𝑘))
200 nn0ssre 11140 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ⊆ ℝ
20152, 200syl6ss 3576 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
202201ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
20356ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
20482ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
20519ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
206 ffvelrn 6247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ (𝑆 ∪ {0}))
20717, 19, 206syl2an 492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ (𝑆 ∪ {0}))
208207anim1i 589 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴𝑘) ≠ 0))
209 eldifsn 4256 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴𝑘) ≠ 0))
210208, 209sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
211 difun2 3996 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
212210, 211syl6eleq 2694 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ (𝑆 ∖ {0}))
213 elpreima 6227 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 Fn ℕ0 → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
21466, 213syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
215214ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
216205, 212, 215mpbir2and 958 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})))
217 suprub 10830 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) ∧ 𝑘 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑘 ≤ sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
218202, 203, 204, 216, 217syl31anc 1320 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ≤ sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
219218, 53syl6breqr 4616 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
220219adantlr 746 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
221220adantlr 746 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
222 simpllr 794 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀𝑘)
223113ad3antrrr 761 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ ℝ)
224116ad3antrrr 761 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀 ∈ ℝ)
225223, 224letri3d 10027 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘𝑀𝑀𝑘)))
226221, 222, 225mpbir2and 958 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 = 𝑀)
227226oveq1d 6539 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘𝑀) = (𝑀𝑀))
228122ad3antrrr 761 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀 ∈ ℂ)
229228subidd 10228 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑀𝑀) = 0)
230227, 229eqtrd 2640 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘𝑀) = 0)
231230oveq2d 6540 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑(𝑘𝑀)) = (𝑛↑0))
232184ad2antlr 758 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑛 ∈ ℂ)
233232exp0d 12816 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑0) = 1)
234231, 233eqtrd 2640 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑(𝑘𝑀)) = 1)
235234oveq2d 6540 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = ((𝐴𝑘) · 1))
236226, 179sylibr 222 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
237236iftrued 4040 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = (𝐴𝑘))
238199, 235, 2373eqtr4d 2650 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
239196, 238pm2.61dane 2865 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
240239mpteq2dva 4663 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)))
241 fconstmpt 5072 . . . . . . . . 9 (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
242240, 241syl6eqr 2658 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}))
243 ifcl 4076 . . . . . . . . . 10 (((𝐴𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ)
244197, 7, 243sylancl 692 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ)
245 1z 11237 . . . . . . . . 9 1 ∈ ℤ
2461eqimss2i 3619 . . . . . . . . . 10 (ℤ‘1) ⊆ ℕ
247246, 27climconst2 14070 . . . . . . . . 9 ((if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
248244, 245, 247sylancl 692 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
249242, 248eqbrtrd 4596 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
250183, 249, 113, 116ltlecasei 9993 . . . . . 6 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
251 snex 4827 . . . . . . . 8 {0} ∈ V
25227, 251xpex 6834 . . . . . . 7 (ℕ × {0}) ∈ V
253252a1i 11 . . . . . 6 (𝜑 → (ℕ × {0}) ∈ V)
254164anasss 676 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
255 plyeq0.5 . . . . . . . . . . . 12 (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))))
256255fveq1d 6087 . . . . . . . . . . 11 (𝜑 → (0𝑝𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚))
257256adantr 479 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (0𝑝𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚))
258132adantl 480 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
259 0pval 23158 . . . . . . . . . . 11 (𝑚 ∈ ℂ → (0𝑝𝑚) = 0)
260258, 259syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (0𝑝𝑚) = 0)
261 oveq1 6531 . . . . . . . . . . . . . 14 (𝑧 = 𝑚 → (𝑧𝑘) = (𝑚𝑘))
262261oveq2d 6540 . . . . . . . . . . . . 13 (𝑧 = 𝑚 → ((𝐴𝑘) · (𝑧𝑘)) = ((𝐴𝑘) · (𝑚𝑘)))
263262sumeq2sdv 14225 . . . . . . . . . . . 12 (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
264 eqid 2606 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))
265 sumex 14209 . . . . . . . . . . . 12 Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) ∈ V
266263, 264, 265fvmpt 6173 . . . . . . . . . . 11 (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
267258, 266syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
268257, 260, 2673eqtr3d 2648 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
269268oveq1d 6539 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (0 / (𝑚𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
270 expcl 12692 . . . . . . . . . 10 ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚𝑀) ∈ ℂ)
271132, 86, 270syl2anr 493 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑚𝑀) ∈ ℂ)
272139adantl 480 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ≠ 0)
273258, 272, 159expne0d 12828 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑚𝑀) ≠ 0)
274271, 273div0d 10646 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (0 / (𝑚𝑀)) = 0)
275 fzfid 12586 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
276 expcl 12692 . . . . . . . . . . 11 ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚𝑘) ∈ ℂ)
277258, 19, 276syl2an 492 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑘) ∈ ℂ)
278156, 277mulcld 9913 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚𝑘)) ∈ ℂ)
279275, 271, 278, 273fsumdivc 14303 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
280269, 274, 2793eqtr3d 2648 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
281 fvconst2g 6347 . . . . . . . 8 ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
2828, 281sylan 486 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
283159adantr 479 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
28448adantl 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
285157, 158, 283, 284expsubd 12833 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘𝑀)) = ((𝑚𝑘) / (𝑚𝑀)))
286285oveq2d 6540 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) = ((𝐴𝑘) · ((𝑚𝑘) / (𝑚𝑀))))
287271adantr 479 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑀) ∈ ℂ)
288273adantr 479 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑀) ≠ 0)
289156, 277, 287, 288divassd 10682 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)) = ((𝐴𝑘) · ((𝑚𝑘) / (𝑚𝑀))))
290286, 154, 2893eqtr4d 2650 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = (((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
291290sumeq2dv 14224 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
292280, 282, 2913eqtr4d 2650 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚))
2931, 2, 3, 250, 253, 254, 292climfsum 14336 . . . . 5 (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
294 suprleub 10833 . . . . . . . . . . . 12 ((((𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) ∧ 𝑁 ∈ ℝ) → (sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
295201, 56, 82, 58, 294syl31anc 1320 . . . . . . . . . . 11 (𝜑 → (sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
29678, 295mpbird 245 . . . . . . . . . 10 (𝜑 → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
29753, 296syl5eqbr 4609 . . . . . . . . 9 (𝜑𝑀𝑁)
298 nn0uz 11551 . . . . . . . . . . 11 0 = (ℤ‘0)
29986, 298syl6eleq 2694 . . . . . . . . . 10 (𝜑𝑀 ∈ (ℤ‘0))
30057nn0zd 11309 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
301 elfz5 12157 . . . . . . . . . 10 ((𝑀 ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀𝑁))
302299, 300, 301syl2anc 690 . . . . . . . . 9 (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀𝑁))
303297, 302mpbird 245 . . . . . . . 8 (𝜑𝑀 ∈ (0...𝑁))
304303snssd 4277 . . . . . . 7 (𝜑 → {𝑀} ⊆ (0...𝑁))
30518, 86ffvelrnd 6250 . . . . . . . . 9 (𝜑 → (𝐴𝑀) ∈ ℂ)
306 elsni 4138 . . . . . . . . . . 11 (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
307306fveq2d 6089 . . . . . . . . . 10 (𝑘 ∈ {𝑀} → (𝐴𝑘) = (𝐴𝑀))
308307eleq1d 2668 . . . . . . . . 9 (𝑘 ∈ {𝑀} → ((𝐴𝑘) ∈ ℂ ↔ (𝐴𝑀) ∈ ℂ))
309305, 308syl5ibrcom 235 . . . . . . . 8 (𝜑 → (𝑘 ∈ {𝑀} → (𝐴𝑘) ∈ ℂ))
310309ralrimiv 2944 . . . . . . 7 (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴𝑘) ∈ ℂ)
3113olcd 406 . . . . . . 7 (𝜑 → ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin))
312 sumss2 14247 . . . . . . 7 ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
313304, 310, 311, 312syl21anc 1316 . . . . . 6 (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
314 ltso 9966 . . . . . . . . 9 < Or ℝ
315314supex 8226 . . . . . . . 8 sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
31653, 315eqeltri 2680 . . . . . . 7 𝑀 ∈ V
317 fveq2 6085 . . . . . . . 8 (𝑘 = 𝑀 → (𝐴𝑘) = (𝐴𝑀))
318317sumsn 14262 . . . . . . 7 ((𝑀 ∈ V ∧ (𝐴𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = (𝐴𝑀))
319316, 305, 318sylancr 693 . . . . . 6 (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = (𝐴𝑀))
320313, 319eqtr3d 2642 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = (𝐴𝑀))
321293, 320breqtrd 4600 . . . 4 (𝜑 → (ℕ × {0}) ⇝ (𝐴𝑀))
322246, 27climconst2 14070 . . . . 5 ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
3237, 245, 322mp2an 703 . . . 4 (ℕ × {0}) ⇝ 0
324 climuni 14074 . . . 4 (((ℕ × {0}) ⇝ (𝐴𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴𝑀) = 0)
325321, 323, 324sylancl 692 . . 3 (𝜑 → (𝐴𝑀) = 0)
326 fvex 6095 . . . 4 (𝐴𝑀) ∈ V
327326elsn 4136 . . 3 ((𝐴𝑀) ∈ {0} ↔ (𝐴𝑀) = 0)
328325, 327sylibr 222 . 2 (𝜑 → (𝐴𝑀) ∈ {0})
329 elpreima 6227 . . . . . 6 (𝐴 Fn ℕ0 → (𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0}))))
33066, 329syl 17 . . . . 5 (𝜑 → (𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0}))))
33185, 330mpbid 220 . . . 4 (𝜑 → (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0})))
332331simprd 477 . . 3 (𝜑 → (𝐴𝑀) ∈ (𝑆 ∖ {0}))
333332eldifbd 3549 . 2 (𝜑 → ¬ (𝐴𝑀) ∈ {0})
334328, 333pm2.65i 183 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1976  wne 2776  wral 2892  wrex 2893  Vcvv 3169  cdif 3533  cun 3534  wss 3536  c0 3870  ifcif 4032  {csn 4121   class class class wbr 4574  cmpt 4634   × cxp 5023  ccnv 5024  dom cdm 5025  cima 5028   Fn wfn 5782  wf 5783  cfv 5787  (class class class)co 6524  𝑚 cmap 7718  Fincfn 7815  supcsup 8203  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794   < clt 9927  cle 9928  cmin 10114  -cneg 10115   / cdiv 10530  cn 10864  0cn0 11136  cz 11207  cuz 11516  +crp 11661  ...cfz 12149  cexp 12674  abscabs 13765  cli 14006  Σcsu 14207  0𝑝c0p 23156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-sum 14208  df-0p 23157
This theorem is referenced by:  plyeq0  23685
  Copyright terms: Public domain W3C validator