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

Theorem plyeq0lem 24011
Description: Lemma for plyeq0 24012. 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 11761 . . . . . 6 ℕ = (ℤ‘1)
2 1zzd 11446 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 fzfid 12812 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
4 1zzd 11446 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5 plyeq0.3 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚0))
6 plyeq0.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ⊆ ℂ)
7 0cn 10070 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
87a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ∈ ℂ)
98snssd 4372 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {0} ⊆ ℂ)
106, 9unssd 3822 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11 cnex 10055 . . . . . . . . . . . . . . . . . . 19 ℂ ∈ V
12 ssexg 4837 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
1310, 11, 12sylancl 695 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 ∪ {0}) ∈ V)
14 nn0ex 11336 . . . . . . . . . . . . . . . . . 18 0 ∈ V
15 elmapg 7912 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
1613, 14, 15sylancl 695 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
175, 16mpbid 222 . . . . . . . . . . . . . . . 16 (𝜑𝐴:ℕ0⟶(𝑆 ∪ {0}))
1817, 10fssd 6095 . . . . . . . . . . . . . . 15 (𝜑𝐴:ℕ0⟶ℂ)
19 elfznn0 12471 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20 ffvelrn 6397 . . . . . . . . . . . . . . 15 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
2118, 19, 20syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
2221adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴𝑘) ∈ ℂ)
2322abscld 14219 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴𝑘)) ∈ ℝ)
2423recnd 10106 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴𝑘)) ∈ ℂ)
25 divcnv 14629 . . . . . . . . . . 11 ((abs‘(𝐴𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) ⇝ 0)
2624, 25syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) ⇝ 0)
27 nnex 11064 . . . . . . . . . . . 12 ℕ ∈ V
2827mptex 6527 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ∈ V
2928a1i 11 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ∈ V)
30 oveq2 6698 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((abs‘(𝐴𝑘)) / 𝑛) = ((abs‘(𝐴𝑘)) / 𝑚))
31 eqid 2651 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))
32 ovex 6718 . . . . . . . . . . . . 13 ((abs‘(𝐴𝑘)) / 𝑚) ∈ V
3330, 31, 32fvmpt 6321 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) / 𝑚))
3433adantl 481 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) / 𝑚))
35 nndivre 11094 . . . . . . . . . . . 12 (((abs‘(𝐴𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) ∈ ℝ)
3623, 35sylan 487 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) ∈ ℝ)
3734, 36eqeltrd 2730 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38 oveq1 6697 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝑛↑(𝑘𝑀)) = (𝑚↑(𝑘𝑀)))
3938oveq2d 6706 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
40 eqid 2651 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))
41 ovex 6718 . . . . . . . . . . . . 13 ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ∈ V
4239, 40, 41fvmpt 6321 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
4342adantl 481 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
4421ad2antrr 762 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴𝑘) ∈ ℂ)
4544abscld 14219 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴𝑘)) ∈ ℝ)
46 nnrp 11880 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
4746adantl 481 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48 elfzelz 12380 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49 cnvimass 5520 . . . . . . . . . . . . . . . . . . 19 (𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
50 fdm 6089 . . . . . . . . . . . . . . . . . . . 20 (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 = ℕ0)
5117, 50syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝐴 = ℕ0)
5249, 51syl5sseq 3686 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
53 plyeq0.6 . . . . . . . . . . . . . . . . . . 19 𝑀 = sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < )
54 nn0ssz 11436 . . . . . . . . . . . . . . . . . . . . 21 0 ⊆ ℤ
5552, 54syl6ss 3648 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
56 plyeq0.7 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
57 plyeq0.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑁 ∈ ℕ0)
5857nn0red 11390 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℝ)
5952sselda 3636 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
60 plyeq0.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 “ (ℤ‘(𝑁 + 1))) = {0})
61 plyco0 23993 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
6257, 18, 61syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
6360, 62mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
6463adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
65 ffn 6083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴:ℕ0⟶(𝑆 ∪ {0}) → 𝐴 Fn ℕ0)
6617, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐴 Fn ℕ0)
67 elpreima 6377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 Fn ℕ0 → (𝑧 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴𝑧) ∈ (𝑆 ∖ {0}))))
6866, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑧 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴𝑧) ∈ (𝑆 ∖ {0}))))
6968simplbda 653 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → (𝐴𝑧) ∈ (𝑆 ∖ {0}))
70 eldifsni 4353 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑧) ∈ (𝑆 ∖ {0}) → (𝐴𝑧) ≠ 0)
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → (𝐴𝑧) ≠ 0)
72 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑧 → (𝐴𝑘) = (𝐴𝑧))
7372neeq1d 2882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑧 → ((𝐴𝑘) ≠ 0 ↔ (𝐴𝑧) ≠ 0))
74 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑧 → (𝑘𝑁𝑧𝑁))
7573, 74imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑧 → (((𝐴𝑘) ≠ 0 → 𝑘𝑁) ↔ ((𝐴𝑧) ≠ 0 → 𝑧𝑁)))
7675rspcv 3336 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℕ0 → (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) → ((𝐴𝑧) ≠ 0 → 𝑧𝑁)))
7759, 64, 71, 76syl3c 66 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑧𝑁)
7877ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁)
79 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑁 → (𝑧𝑥𝑧𝑁))
8079ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑁 → (∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
8180rspcev 3340 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
8258, 78, 81syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
83 suprzcl 11495 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (𝐴 “ (𝑆 ∖ {0})))
8455, 56, 82, 83syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 (𝜑 → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (𝐴 “ (𝑆 ∖ {0})))
8553, 84syl5eqel 2734 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})))
8652, 85sseldd 3637 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ0)
8786nn0zd 11518 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
88 zsubcl 11457 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘𝑀) ∈ ℤ)
8948, 87, 88syl2anr 494 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑘𝑀) ∈ ℤ)
9089ad2antrr 762 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ∈ ℤ)
9147, 90rpexpcld 13072 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℝ+)
9291rpred 11910 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℝ)
9345, 92remulcld 10108 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ∈ ℝ)
9443, 93eqeltrd 2730 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℝ)
95 nnrecre 11095 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
9695adantl 481 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
9722absge0d 14227 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴𝑘)))
9897adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴𝑘)))
99 nnre 11065 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
10099adantl 481 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
101 nnge1 11084 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 1 ≤ 𝑚)
102101adantl 481 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
103 1red 10093 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
10490zred 11520 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ∈ ℝ)
105 simplr 807 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
10648adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
107106ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
10887ad3antrrr 766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
109 zltp1le 11465 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
110107, 108, 109syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
111105, 110mpbid 222 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
11219adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
113112nn0red 11390 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
114113ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
11586adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
116115nn0red 11390 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
117116ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
118114, 103, 117leaddsub2d 10667 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀𝑘)))
119111, 118mpbid 222 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀𝑘))
120113recnd 10106 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
121120ad2antrr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
122116recnd 10106 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
123122ad2antrr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
124121, 123negsubdi2d 10446 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘𝑀) = (𝑀𝑘))
125119, 124breqtrrd 4713 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘𝑀))
126103, 104, 125lenegcon2d 10648 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘𝑀) ≤ -1)
127 neg1z 11451 . . . . . . . . . . . . . . . 16 -1 ∈ ℤ
128 eluz 11739 . . . . . . . . . . . . . . . 16 (((𝑘𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ‘(𝑘𝑀)) ↔ (𝑘𝑀) ≤ -1))
12990, 127, 128sylancl 695 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ‘(𝑘𝑀)) ↔ (𝑘𝑀) ≤ -1))
130126, 129mpbird 247 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ‘(𝑘𝑀)))
131100, 102, 130leexp2ad 13081 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ≤ (𝑚↑-1))
132 nncn 11066 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
133132adantl 481 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
134 expn1 12910 . . . . . . . . . . . . . 14 (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
135133, 134syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
136131, 135breqtrd 4711 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ≤ (1 / 𝑚))
13792, 96, 45, 98, 136lemul2ad 11002 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))) ≤ ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
13824adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴𝑘)) ∈ ℂ)
139 nnne0 11091 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
140139adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
141138, 133, 140divrecd 10842 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) / 𝑚) = ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
14234, 141eqtrd 2685 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴𝑘)) · (1 / 𝑚)))
143137, 43, 1423brtr4d 4717 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) / 𝑛))‘𝑚))
14491rpge0d 11914 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘𝑀)))
14545, 92, 98, 144mulge0d 10642 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
146145, 43breqtrrd 4713 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚))
1471, 4, 26, 29, 37, 94, 143, 146climsqz2 14416 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ⇝ 0)
14827mptex 6527 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ∈ V
149148a1i 11 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ∈ V)
15038oveq2d 6706 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
151 eqid 2651 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))
152 ovex 6718 . . . . . . . . . . . . . . 15 ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) ∈ V
153150, 151, 152fvmpt 6321 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
154153ad2antlr 763 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
15518adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
156155, 19, 20syl2an 493 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
157132ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
158139ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
15987adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
16048, 159, 88syl2anr 494 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘𝑀) ∈ ℤ)
161157, 158, 160expclzd 13053 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘𝑀)) ∈ ℂ)
162156, 161mulcld 10098 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) ∈ ℂ)
163154, 162eqeltrd 2730 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
164163an32s 863 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
165164adantlr 751 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
16692recnd 10106 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘𝑀)) ∈ ℂ)
16744, 166absmuld 14237 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑚↑(𝑘𝑀)))))
16892, 144absidd 14205 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘𝑀))) = (𝑚↑(𝑘𝑀)))
169168oveq2d 6706 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴𝑘)) · (abs‘(𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
170167, 169eqtrd 2685 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))) = ((abs‘(𝐴𝑘)) · (𝑚↑(𝑘𝑀))))
171153adantl 481 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = ((𝐴𝑘) · (𝑚↑(𝑘𝑀))))
172171fveq2d 6233 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚)) = (abs‘((𝐴𝑘) · (𝑚↑(𝑘𝑀)))))
173170, 172, 433eqtr4rd 2696 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚)))
1741, 4, 149, 29, 165, 173climabs0 14360 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴𝑘)) · (𝑛↑(𝑘𝑀)))) ⇝ 0))
175147, 174mpbird 247 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ 0)
176113adantr 480 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
177 simpr 476 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
178176, 177ltned 10211 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘𝑀)
179 velsn 4226 . . . . . . . . . . 11 (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
180179necon3bbii 2870 . . . . . . . . . 10 𝑘 ∈ {𝑀} ↔ 𝑘𝑀)
181178, 180sylibr 224 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
182181iffalsed 4130 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = 0)
183175, 182breqtrrd 4713 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
184 nncn 11066 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
185184ad2antlr 763 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → 𝑛 ∈ ℂ)
186 nnne0 11091 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
187186ad2antlr 763 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → 𝑛 ≠ 0)
18889ad3antrrr 766 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝑘𝑀) ∈ ℤ)
189185, 187, 188expclzd 13053 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝑛↑(𝑘𝑀)) ∈ ℂ)
190189mul02d 10272 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (0 · (𝑛↑(𝑘𝑀))) = 0)
191 simpr 476 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → (𝐴𝑘) = 0)
192191oveq1d 6705 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = (0 · (𝑛↑(𝑘𝑀))))
193191ifeq1d 4137 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
194 ifid 4158 . . . . . . . . . . . . 13 if(𝑘 ∈ {𝑀}, 0, 0) = 0
195193, 194syl6eq 2701 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = 0)
196190, 192, 1953eqtr4d 2695 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) = 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
19721adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝐴𝑘) ∈ ℂ)
198197ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ ℂ)
199198mulid1d 10095 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · 1) = (𝐴𝑘))
200 nn0ssre 11334 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ⊆ ℝ
20152, 200syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
202201ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
20356ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
20482ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥)
20519ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
206 ffvelrn 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ (𝑆 ∪ {0}))
20717, 19, 206syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ (𝑆 ∪ {0}))
208207anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴𝑘) ≠ 0))
209 eldifsn 4350 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴𝑘) ≠ 0))
210208, 209sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
211 difun2 4081 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
212210, 211syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝐴𝑘) ∈ (𝑆 ∖ {0}))
213 elpreima 6377 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 Fn ℕ0 → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
21466, 213syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
215214ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → (𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ∈ (𝑆 ∖ {0}))))
216205, 212, 215mpbir2and 977 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ (𝐴 “ (𝑆 ∖ {0})))
217 suprub 11022 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) ∧ 𝑘 ∈ (𝐴 “ (𝑆 ∖ {0}))) → 𝑘 ≤ sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
218202, 203, 204, 216, 217syl31anc 1369 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ≤ sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
219218, 53syl6breqr 4727 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝑁)) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
220219adantlr 751 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
221220adantlr 751 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘𝑀)
222 simpllr 815 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀𝑘)
223113ad3antrrr 766 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ ℝ)
224116ad3antrrr 766 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀 ∈ ℝ)
225223, 224letri3d 10217 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘𝑀𝑀𝑘)))
226221, 222, 225mpbir2and 977 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 = 𝑀)
227226oveq1d 6705 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘𝑀) = (𝑀𝑀))
228122ad3antrrr 766 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑀 ∈ ℂ)
229228subidd 10418 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑀𝑀) = 0)
230227, 229eqtrd 2685 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑘𝑀) = 0)
231230oveq2d 6706 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑(𝑘𝑀)) = (𝑛↑0))
232184ad2antlr 763 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑛 ∈ ℂ)
233232exp0d 13042 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑0) = 1)
234231, 233eqtrd 2685 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → (𝑛↑(𝑘𝑀)) = 1)
235234oveq2d 6706 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = ((𝐴𝑘) · 1))
236226, 179sylibr 224 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
237236iftrued 4127 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = (𝐴𝑘))
238199, 235, 2373eqtr4d 2695 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴𝑘) ≠ 0) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
239196, 238pm2.61dane 2910 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴𝑘) · (𝑛↑(𝑘𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
240239mpteq2dva 4777 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)))
241 fconstmpt 5197 . . . . . . . . 9 (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
242240, 241syl6eqr 2703 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}))
243 ifcl 4163 . . . . . . . . . 10 (((𝐴𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ)
244197, 7, 243sylancl 695 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ)
245 1z 11445 . . . . . . . . 9 1 ∈ ℤ
2461eqimss2i 3693 . . . . . . . . . 10 (ℤ‘1) ⊆ ℕ
247246, 27climconst2 14323 . . . . . . . . 9 ((if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
248244, 245, 247sylancl 695 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
249242, 248eqbrtrd 4707 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑀𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
250183, 249, 113, 116ltlecasei 10183 . . . . . 6 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
251 snex 4938 . . . . . . . 8 {0} ∈ V
25227, 251xpex 7004 . . . . . . 7 (ℕ × {0}) ∈ V
253252a1i 11 . . . . . 6 (𝜑 → (ℕ × {0}) ∈ V)
254164anasss 680 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) ∈ ℂ)
255 plyeq0.5 . . . . . . . . . . . 12 (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))))
256255fveq1d 6231 . . . . . . . . . . 11 (𝜑 → (0𝑝𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚))
257256adantr 480 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (0𝑝𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚))
258132adantl 481 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
259 0pval 23483 . . . . . . . . . . 11 (𝑚 ∈ ℂ → (0𝑝𝑚) = 0)
260258, 259syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (0𝑝𝑚) = 0)
261 oveq1 6697 . . . . . . . . . . . . . 14 (𝑧 = 𝑚 → (𝑧𝑘) = (𝑚𝑘))
262261oveq2d 6706 . . . . . . . . . . . . 13 (𝑧 = 𝑚 → ((𝐴𝑘) · (𝑧𝑘)) = ((𝐴𝑘) · (𝑚𝑘)))
263262sumeq2sdv 14479 . . . . . . . . . . . 12 (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
264 eqid 2651 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))
265 sumex 14462 . . . . . . . . . . . 12 Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) ∈ V
266263, 264, 265fvmpt 6321 . . . . . . . . . . 11 (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
267258, 266syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
268257, 260, 2673eqtr3d 2693 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)))
269268oveq1d 6705 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (0 / (𝑚𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
270 expcl 12918 . . . . . . . . . 10 ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚𝑀) ∈ ℂ)
271132, 86, 270syl2anr 494 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑚𝑀) ∈ ℂ)
272139adantl 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ≠ 0)
273258, 272, 159expne0d 13054 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑚𝑀) ≠ 0)
274271, 273div0d 10838 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (0 / (𝑚𝑀)) = 0)
275 fzfid 12812 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
276 expcl 12918 . . . . . . . . . . 11 ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚𝑘) ∈ ℂ)
277258, 19, 276syl2an 493 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑘) ∈ ℂ)
278156, 277mulcld 10098 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚𝑘)) ∈ ℂ)
279275, 271, 278, 273fsumdivc 14562 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
280269, 274, 2793eqtr3d 2693 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
281 fvconst2g 6508 . . . . . . . 8 ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
2828, 281sylan 487 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
283159adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
28448adantl 481 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
285157, 158, 283, 284expsubd 13059 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘𝑀)) = ((𝑚𝑘) / (𝑚𝑀)))
286285oveq2d 6706 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · (𝑚↑(𝑘𝑀))) = ((𝐴𝑘) · ((𝑚𝑘) / (𝑚𝑀))))
287271adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑀) ∈ ℂ)
288273adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚𝑀) ≠ 0)
289156, 277, 287, 288divassd 10874 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)) = ((𝐴𝑘) · ((𝑚𝑘) / (𝑚𝑀))))
290286, 154, 2893eqtr4d 2695 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = (((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
291290sumeq2dv 14477 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴𝑘) · (𝑚𝑘)) / (𝑚𝑀)))
292280, 282, 2913eqtr4d 2695 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴𝑘) · (𝑛↑(𝑘𝑀))))‘𝑚))
2931, 2, 3, 250, 253, 254, 292climfsum 14596 . . . . 5 (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
294 suprleub 11027 . . . . . . . . . . . 12 ((((𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑥) ∧ 𝑁 ∈ ℝ) → (sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
295201, 56, 82, 58, 294syl31anc 1369 . . . . . . . . . . 11 (𝜑 → (sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (𝐴 “ (𝑆 ∖ {0}))𝑧𝑁))
29678, 295mpbird 247 . . . . . . . . . 10 (𝜑 → sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
29753, 296syl5eqbr 4720 . . . . . . . . 9 (𝜑𝑀𝑁)
298 nn0uz 11760 . . . . . . . . . . 11 0 = (ℤ‘0)
29986, 298syl6eleq 2740 . . . . . . . . . 10 (𝜑𝑀 ∈ (ℤ‘0))
30057nn0zd 11518 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
301 elfz5 12372 . . . . . . . . . 10 ((𝑀 ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀𝑁))
302299, 300, 301syl2anc 694 . . . . . . . . 9 (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀𝑁))
303297, 302mpbird 247 . . . . . . . 8 (𝜑𝑀 ∈ (0...𝑁))
304303snssd 4372 . . . . . . 7 (𝜑 → {𝑀} ⊆ (0...𝑁))
30518, 86ffvelrnd 6400 . . . . . . . . 9 (𝜑 → (𝐴𝑀) ∈ ℂ)
306 elsni 4227 . . . . . . . . . . 11 (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
307306fveq2d 6233 . . . . . . . . . 10 (𝑘 ∈ {𝑀} → (𝐴𝑘) = (𝐴𝑀))
308307eleq1d 2715 . . . . . . . . 9 (𝑘 ∈ {𝑀} → ((𝐴𝑘) ∈ ℂ ↔ (𝐴𝑀) ∈ ℂ))
309305, 308syl5ibrcom 237 . . . . . . . 8 (𝜑 → (𝑘 ∈ {𝑀} → (𝐴𝑘) ∈ ℂ))
310309ralrimiv 2994 . . . . . . 7 (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴𝑘) ∈ ℂ)
3113olcd 407 . . . . . . 7 (𝜑 → ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin))
312 sumss2 14501 . . . . . . 7 ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
313304, 310, 311, 312syl21anc 1365 . . . . . 6 (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0))
314 ltso 10156 . . . . . . . . 9 < Or ℝ
315314supex 8410 . . . . . . . 8 sup((𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
31653, 315eqeltri 2726 . . . . . . 7 𝑀 ∈ V
317 fveq2 6229 . . . . . . . 8 (𝑘 = 𝑀 → (𝐴𝑘) = (𝐴𝑀))
318317sumsn 14519 . . . . . . 7 ((𝑀 ∈ V ∧ (𝐴𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = (𝐴𝑀))
319316, 305, 318sylancr 696 . . . . . 6 (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴𝑘) = (𝐴𝑀))
320313, 319eqtr3d 2687 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴𝑘), 0) = (𝐴𝑀))
321293, 320breqtrd 4711 . . . 4 (𝜑 → (ℕ × {0}) ⇝ (𝐴𝑀))
322246, 27climconst2 14323 . . . . 5 ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
3237, 245, 322mp2an 708 . . . 4 (ℕ × {0}) ⇝ 0
324 climuni 14327 . . . 4 (((ℕ × {0}) ⇝ (𝐴𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴𝑀) = 0)
325321, 323, 324sylancl 695 . . 3 (𝜑 → (𝐴𝑀) = 0)
326 fvex 6239 . . . 4 (𝐴𝑀) ∈ V
327326elsn 4225 . . 3 ((𝐴𝑀) ∈ {0} ↔ (𝐴𝑀) = 0)
328325, 327sylibr 224 . 2 (𝜑 → (𝐴𝑀) ∈ {0})
329 elpreima 6377 . . . . . 6 (𝐴 Fn ℕ0 → (𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0}))))
33066, 329syl 17 . . . . 5 (𝜑 → (𝑀 ∈ (𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0}))))
33185, 330mpbid 222 . . . 4 (𝜑 → (𝑀 ∈ ℕ0 ∧ (𝐴𝑀) ∈ (𝑆 ∖ {0})))
332331simprd 478 . . 3 (𝜑 → (𝐴𝑀) ∈ (𝑆 ∖ {0}))
333332eldifbd 3620 . 2 (𝜑 → ¬ (𝐴𝑀) ∈ {0})
334328, 333pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cun 3605  wss 3607  c0 3948  ifcif 4119  {csn 4210   class class class wbr 4685  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  cima 5146   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  Fincfn 7997  supcsup 8387  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304  -cneg 10305   / cdiv 10722  cn 11058  0cn0 11330  cz 11415  cuz 11725  +crp 11870  ...cfz 12364  cexp 12900  abscabs 14018  cli 14259  Σcsu 14460  0𝑝c0p 23481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-0p 23482
This theorem is referenced by:  plyeq0  24012
  Copyright terms: Public domain W3C validator