Theorem plyeq0lem 25276

Description: Lemma for plyeq0 25277. If 𝐴 is the coefficient function for a nonzero polynomial such that 𝑃(𝑧) = Σ𝑘 ∈ ℕ₀𝐴(𝑘) · 𝑧↑𝑘 = 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}) ↑m ℕ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.

Step	Hyp	Ref	Expression
1		nnuz 12550	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12281	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
3		fzfid 13621	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
4		1zzd 12281	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5		plyeq0.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))
6		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7		0cn 10898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 ∈ ℂ)
9	8	snssd 4739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {0} ⊆ ℂ)
10	6, 9	unssd 4116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11		cnex 10883	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂ ∈ V
12		ssexg 5242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
13	10, 11, 12	sylancl 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V)
14		nn0ex 12169	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
15		elmapg 8586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
16	13, 14, 15	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
17	5, 16	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
18	17, 10	fssd 6602	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
19		elfznn0 13278	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20		ffvelrn 6941	. . . . . . . . . . . . . . 15 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
21	18, 19, 20	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
22	21	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴‘𝑘) ∈ ℂ)
23	22	abscld 15076	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
24	23	recnd 10934	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
25		divcnv 15493	. . . . . . . . . . 11 ⊢ ((abs‘(𝐴‘𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
26	24, 25	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
27		nnex 11909	. . . . . . . . . . . 12 ⊢ ℕ ∈ V
28	27	mptex 7081	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
29	28	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
30		oveq2 7263	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) / 𝑛) = ((abs‘(𝐴‘𝑘)) / 𝑚))
31		eqid 2738	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))
32		ovex 7288	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ V
33	30, 31, 32	fvmpt 6857	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
34	33	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
35		nndivre 11944	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴‘𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
36	23, 35	sylan 579	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
37	34, 36	eqeltrd 2839	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38		oveq1 7262	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → (𝑛↑(𝑘 − 𝑀)) = (𝑚↑(𝑘 − 𝑀)))
39	38	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
40		eqid 2738	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))
41		ovex 7288	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ V
42	39, 40, 41	fvmpt 6857	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
43	42	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
44	21	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴‘𝑘) ∈ ℂ)
45	44	abscld 15076	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
46		nnrp 12670	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
47	46	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48		elfzelz 13185	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49		cnvimass 5978	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
50	49, 17	fssdm 6604	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
51		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < )
52		nn0ssz 12271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ⊆ ℤ
53	50, 52	sstrdi 3929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
54		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
55		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
56	55	nn0red 12224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℝ)
57	17	ffnd 6585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 Fn ℕ0)
58		elpreima 6917	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 Fn ℕ0 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
60	59	simplbda 499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))
61		eldifsni 4720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑧) ∈ (𝑆 ∖ {0}) → (𝐴‘𝑧) ≠ 0)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ≠ 0)
63		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑧 → (𝐴‘𝑘) = (𝐴‘𝑧))
64	63	neeq1d 3002	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → ((𝐴‘𝑘) ≠ 0 ↔ (𝐴‘𝑧) ≠ 0))
65		breq1 5073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → (𝑘 ≤ 𝑁 ↔ 𝑧 ≤ 𝑁))
66	64, 65	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑧 → (((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁)))
67		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})
68		plyco0 25258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
69	55, 18, 68	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
70	67, 69	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
71	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
72	50	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
73	66, 71, 72	rspcdva 3554	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁))
74	62, 73	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ≤ 𝑁)
75	74	ralrimiva 3107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁)
76		brralrspcev 5130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
77	56, 75, 76	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
78		suprzcl 12330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
79	53, 54, 77, 78	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
80	51, 79	eqeltrid 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
81	50, 80	sseldd 3918	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
82	81	nn0zd 12353	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83		zsubcl 12292	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 − 𝑀) ∈ ℤ)
84	48, 82, 83	syl2anr 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
85	84	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℤ)
86	47, 85	rpexpcld 13890	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ+)
87	86	rpred 12701	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ)
88	45, 87	remulcld 10936	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ ℝ)
89	43, 88	eqeltrd 2839	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℝ)
90		nnrecre 11945	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
91	90	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
92	22	absge0d 15084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴‘𝑘)))
93	92	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴‘𝑘)))
94		nnre 11910	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
95	94	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
96		nnge1 11931	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 1 ≤ 𝑚)
97	96	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
98		1red 10907	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
99	85	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℝ)
100		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
101	48	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
102	101	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
103	82	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
104		zltp1le 12300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
105	102, 103, 104	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
106	100, 105	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
107	19	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
108	107	nn0red 12224	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
109	108	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
110	81	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
111	110	nn0red 12224	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
112	111	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
113	109, 98, 112	leaddsub2d 11507	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀 − 𝑘)))
114	106, 113	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀 − 𝑘))
115	108	recnd 10934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
116	115	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
117	111	recnd 10934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
118	117	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
119	116, 118	negsubdi2d 11278	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘 − 𝑀) = (𝑀 − 𝑘))
120	114, 119	breqtrrd 5098	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘 − 𝑀))
121	98, 99, 120	lenegcon2d 11488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ≤ -1)
122		neg1z 12286	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
123		eluz 12525	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 − 𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
124	85, 122, 123	sylancl 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
125	121, 124	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ≥‘(𝑘 − 𝑀)))
126	95, 97, 125	leexp2ad 13899	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (𝑚↑-1))
127		nncn 11911	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
128	127	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
129		expn1 13720	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
130	128, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
131	126, 130	breqtrd 5096	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (1 / 𝑚))
132	87, 91, 45, 93, 131	lemul2ad 11845	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ≤ ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
133	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
134		nnne0 11937	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
135	134	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
136	133, 128, 135	divrecd 11684	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
137	34, 136	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
138	132, 43, 137	3brtr4d 5102	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚))
139	86	rpge0d 12705	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘 − 𝑀)))
140	45, 87, 93, 139	mulge0d 11482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
141	140, 43	breqtrrd 5098	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
142	1, 4, 26, 29, 37, 89, 138, 141	climsqz2 15279	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
143	27	mptex 7081	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
144	143	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
145	38	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
146		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))
147		ovex 7288	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ V
148	145, 146, 147	fvmpt 6857	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
149	148	ad2antlr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
150	18	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
151	150, 19, 20	syl2an 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
152	127	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
153	134	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
154	82	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
155	48, 154, 83	syl2anr 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
156	152, 153, 155	expclzd 13797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
157	151, 156	mulcld 10926	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ ℂ)
158	149, 157	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
159	158	an32s 648	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
160	159	adantlr 711	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
161	87	recnd 10934	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
162	44, 161	absmuld 15094	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))))
163	87, 139	absidd 15062	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘 − 𝑀))) = (𝑚↑(𝑘 − 𝑀)))
164	163	oveq2d 7271	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
165	162, 164	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
166	148	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
167	166	fveq2d 6760	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) = (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))))
168	165, 167, 43	3eqtr4rd 2789	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)))
169	1, 4, 144, 29, 160, 168	climabs0 15222	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0))
170	142, 169	mpbird 256	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
171	108	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
172		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
173	171, 172	ltned 11041	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ≠ 𝑀)
174		velsn 4574	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
175	174	necon3bbii 2990	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ {𝑀} ↔ 𝑘 ≠ 𝑀)
176	173, 175	sylibr 233	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
177	176	iffalsed 4467	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
178	170, 177	breqtrrd 5098	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
179		nncn 11911	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
180	179	ad2antlr 723	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ∈ ℂ)
181		nnne0 11937	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
182	181	ad2antlr 723	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ≠ 0)
183	84	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑘 − 𝑀) ∈ ℤ)
184	180, 182, 183	expclzd 13797	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑛↑(𝑘 − 𝑀)) ∈ ℂ)
185	184	mul02d 11103	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (0 · (𝑛↑(𝑘 − 𝑀))) = 0)
186		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)
187	186	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = (0 · (𝑛↑(𝑘 − 𝑀))))
188	186	ifeq1d 4475	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
189		ifid 4496	. . . . . . . . . . . . 13 ⊢ if(𝑘 ∈ {𝑀}, 0, 0) = 0
190	188, 189	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
191	185, 187, 190	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
192	21	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝐴‘𝑘) ∈ ℂ)
193	192	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ℂ)
194	193	mulid1d 10923	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · 1) = (𝐴‘𝑘))
195		nn0ssre 12167	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ0 ⊆ ℝ
196	50, 195	sstrdi 3929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
197	196	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
198	54	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
199	77	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
200	19	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
201		ffvelrn 6941	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
202	17, 19, 201	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
203	202	anim1i 614	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
204		eldifsn 4717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
205	203, 204	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
206		difun2 4411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
207	205, 206	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))
208		elpreima 6917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 Fn ℕ0 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
209	57, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
210	209	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
211	200, 207, 210	mpbir2and 709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
212	197, 198, 199, 211	suprubd 11867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
213	212, 51	breqtrrdi 5112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
214	213	ad4ant14 748	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
215		simpllr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ≤ 𝑘)
216	108	ad3antrrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℝ)
217	111	ad3antrrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℝ)
218	216, 217	letri3d 11047	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘)))
219	214, 215, 218	mpbir2and 709	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 = 𝑀)
220	219	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = (𝑀 − 𝑀))
221	117	ad3antrrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℂ)
222	221	subidd 11250	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑀 − 𝑀) = 0)
223	220, 222	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = 0)
224	223	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = (𝑛↑0))
225	179	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑛 ∈ ℂ)
226	225	exp0d 13786	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑0) = 1)
227	224, 226	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = 1)
228	227	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · 1))
229	219, 174	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
230	229	iftrued 4464	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑘))
231	194, 228, 230	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
232	191, 231	pm2.61dane 3031	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
233	232	mpteq2dva 5170	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)))
234		fconstmpt 5640	. . . . . . . . 9 ⊢ (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
235	233, 234	eqtr4di 2797	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}))
236		ifcl 4501	. . . . . . . . . 10 ⊢ (((𝐴‘𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
237	192, 7, 236	sylancl 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
238		1z 12280	. . . . . . . . 9 ⊢ 1 ∈ ℤ
239	1	eqimss2i 3976	. . . . . . . . . 10 ⊢ (ℤ≥‘1) ⊆ ℕ
240	239, 27	climconst2 15185	. . . . . . . . 9 ⊢ ((if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
241	237, 238, 240	sylancl 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
242	235, 241	eqbrtrd 5092	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
243	178, 242, 108, 111	ltlecasei 11013	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
244		snex 5349	. . . . . . . 8 ⊢ {0} ∈ V
245	27, 244	xpex 7581	. . . . . . 7 ⊢ (ℕ × {0}) ∈ V
246	245	a1i 11	. . . . . 6 ⊢ (𝜑 → (ℕ × {0}) ∈ V)
247	159	anasss 466	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
248		plyeq0.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
249	248	fveq1d 6758	. . . . . . . . . . 11 ⊢ (𝜑 → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
250	249	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
251	127	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
252		0pval 24740	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → (0𝑝‘𝑚) = 0)
253	251, 252	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = 0)
254		oveq1 7262	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑚 → (𝑧↑𝑘) = (𝑚↑𝑘))
255	254	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑚 → ((𝐴‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑚↑𝑘)))
256	255	sumeq2sdv 15344	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
257		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))
258		sumex 15327	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ V
259	256, 257, 258	fvmpt 6857	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
260	251, 259	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
261	250, 253, 260	3eqtr3d 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
262	261	oveq1d 7270	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
263		expcl 13728	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚↑𝑀) ∈ ℂ)
264	127, 81, 263	syl2anr 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ∈ ℂ)
265	134	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
266	251, 265, 154	expne0d 13798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ≠ 0)
267	264, 266	div0d 11680	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = 0)
268		fzfid 13621	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
269		expcl 13728	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚↑𝑘) ∈ ℂ)
270	251, 19, 269	syl2an 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑘) ∈ ℂ)
271	151, 270	mulcld 10926	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ ℂ)
272	268, 264, 271, 266	fsumdivc 15426	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
273	262, 267, 272	3eqtr3d 2786	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
274		fvconst2g 7059	. . . . . . . 8 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
275	8, 274	sylan 579	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
276	154	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
277	48	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
278	152, 153, 276, 277	expsubd 13803	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) = ((𝑚↑𝑘) / (𝑚↑𝑀)))
279	278	oveq2d 7271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
280	264	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ∈ ℂ)
281	266	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ≠ 0)
282	151, 270, 280, 281	divassd 11716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
283	279, 149, 282	3eqtr4d 2788	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
284	283	sumeq2dv 15343	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
285	273, 275, 284	3eqtr4d 2788	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
286	1, 2, 3, 243, 246, 247, 285	climfsum 15460	. . . . 5 ⊢ (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
287		suprleub 11871	. . . . . . . . . . . 12 ⊢ ((((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) ∧ 𝑁 ∈ ℝ) → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
288	196, 54, 77, 56, 287	syl31anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
289	75, 288	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
290	51, 289	eqbrtrid 5105	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
291		nn0uz 12549	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
292	81, 291	eleqtrdi 2849	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
293	55	nn0zd 12353	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
294		elfz5 13177	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
295	292, 293, 294	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
296	290, 295	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
297	296	snssd 4739	. . . . . . 7 ⊢ (𝜑 → {𝑀} ⊆ (0...𝑁))
298	18, 81	ffvelrnd 6944	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ)
299		elsni 4575	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
300	299	fveq2d 6760	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑀} → (𝐴‘𝑘) = (𝐴‘𝑀))
301	300	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑀} → ((𝐴‘𝑘) ∈ ℂ ↔ (𝐴‘𝑀) ∈ ℂ))
302	298, 301	syl5ibrcom 246	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ {𝑀} → (𝐴‘𝑘) ∈ ℂ))
303	302	ralrimiv 3106	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ)
304	3	olcd 870	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin))
305		sumss2 15366	. . . . . . 7 ⊢ ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
306	297, 303, 304, 305	syl21anc 834	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
307		ltso 10986	. . . . . . . . 9 ⊢ < Or ℝ
308	307	supex 9152	. . . . . . . 8 ⊢ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
309	51, 308	eqeltri 2835	. . . . . . 7 ⊢ 𝑀 ∈ V
310		fveq2 6756	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐴‘𝑘) = (𝐴‘𝑀))
311	310	sumsn 15386	. . . . . . 7 ⊢ ((𝑀 ∈ V ∧ (𝐴‘𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
312	309, 298, 311	sylancr 586	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
313	306, 312	eqtr3d 2780	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑀))
314	286, 313	breqtrd 5096	. . . 4 ⊢ (𝜑 → (ℕ × {0}) ⇝ (𝐴‘𝑀))
315	239, 27	climconst2 15185	. . . . 5 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
316	7, 238, 315	mp2an 688	. . . 4 ⊢ (ℕ × {0}) ⇝ 0
317		climuni 15189	. . . 4 ⊢ (((ℕ × {0}) ⇝ (𝐴‘𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴‘𝑀) = 0)
318	314, 316, 317	sylancl 585	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) = 0)
319		fvex 6769	. . . 4 ⊢ (𝐴‘𝑀) ∈ V
320	319	elsn 4573	. . 3 ⊢ ((𝐴‘𝑀) ∈ {0} ↔ (𝐴‘𝑀) = 0)
321	318, 320	sylibr 233	. 2 ⊢ (𝜑 → (𝐴‘𝑀) ∈ {0})
322		elpreima 6917	. . . . . 6 ⊢ (𝐴 Fn ℕ0 → (𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))))
323	57, 322	syl 17	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))))
324	80, 323	mpbid 231	. . . 4 ⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0})))
325	324	simprd 495	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))
326	325	eldifbd 3896	. 2 ⊢ (𝜑 → ¬ (𝐴‘𝑀) ∈ {0})
327	321, 326	pm2.65i 193	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4253  ifcif 4456  {csn 4558   class class class wbr 5070   ↦ cmpt 5153   × cxp 5578  ^◡ccnv 5579   “ cima 5583   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255   ↑_m cmap 8573  Fincfn 8691  supcsup 9129  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807   < clt 10940   ≤ cle 10941   − cmin 11135  -cneg 11136   / cdiv 11562  ℕcn 11903  ℕ₀cn0 12163  ℤcz 12249  ℤ_≥cuz 12511  ℝ⁺crp 12659  ...cfz 13168  ↑cexp 13710  abscabs 14873   ⇝ cli 15121  Σcsu 15325  0_𝑝c0p 24738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-er 8456  df-map 8575  df-pm 8576  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-sup 9131  df-inf 9132  df-oi 9199  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-n0 12164  df-z 12250  df-uz 12512  df-rp 12660  df-fz 13169  df-fzo 13312  df-fl 13440  df-seq 13650  df-exp 13711  df-hash 13973  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-clim 15125  df-rlim 15126  df-sum 15326  df-0p 24739

This theorem is referenced by:  plyeq0  25277