Theorem plyeq0lem 25380

Description: Lemma for plyeq0 25381. 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 12630	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12360	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
3		fzfid 13702	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
4		1zzd 12360	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5		plyeq0.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))
6		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7		0cn 10976	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 ∈ ℂ)
9	8	snssd 4743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {0} ⊆ ℂ)
10	6, 9	unssd 4121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11		cnex 10961	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂ ∈ V
12		ssexg 5248	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
13	10, 11, 12	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V)
14		nn0ex 12248	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
15		elmapg 8637	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
16	13, 14, 15	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
17	5, 16	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
18	17, 10	fssd 6627	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
19		elfznn0 13358	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20		ffvelrn 6968	. . . . . . . . . . . . . . 15 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
21	18, 19, 20	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
22	21	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴‘𝑘) ∈ ℂ)
23	22	abscld 15157	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
24	23	recnd 11012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
25		divcnv 15574	. . . . . . . . . . 11 ⊢ ((abs‘(𝐴‘𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
26	24, 25	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
27		nnex 11988	. . . . . . . . . . . 12 ⊢ ℕ ∈ V
28	27	mptex 7108	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
29	28	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
30		oveq2 7292	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) / 𝑛) = ((abs‘(𝐴‘𝑘)) / 𝑚))
31		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))
32		ovex 7317	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ V
33	30, 31, 32	fvmpt 6884	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
34	33	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
35		nndivre 12023	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴‘𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
36	23, 35	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
37	34, 36	eqeltrd 2840	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38		oveq1 7291	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → (𝑛↑(𝑘 − 𝑀)) = (𝑚↑(𝑘 − 𝑀)))
39	38	oveq2d 7300	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
40		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))
41		ovex 7317	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ V
42	39, 40, 41	fvmpt 6884	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
43	42	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
44	21	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴‘𝑘) ∈ ℂ)
45	44	abscld 15157	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
46		nnrp 12750	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
47	46	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48		elfzelz 13265	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49		cnvimass 5992	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
50	49, 17	fssdm 6629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
51		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < )
52		nn0ssz 12350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ⊆ ℤ
53	50, 52	sstrdi 3934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
54		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
55		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
56	55	nn0red 12303	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℝ)
57	17	ffnd 6610	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 Fn ℕ0)
58		elpreima 6944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 Fn ℕ0 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
60	59	simplbda 500	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))
61		eldifsni 4724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑧) ∈ (𝑆 ∖ {0}) → (𝐴‘𝑧) ≠ 0)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ≠ 0)
63		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑧 → (𝐴‘𝑘) = (𝐴‘𝑧))
64	63	neeq1d 3004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → ((𝐴‘𝑘) ≠ 0 ↔ (𝐴‘𝑧) ≠ 0))
65		breq1 5078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → (𝑘 ≤ 𝑁 ↔ 𝑧 ≤ 𝑁))
66	64, 65	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑧 → (((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁)))
67		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})
68		plyco0 25362	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
69	55, 18, 68	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
70	67, 69	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
72	50	sselda 3922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
73	66, 71, 72	rspcdva 3563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁))
74	62, 73	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ≤ 𝑁)
75	74	ralrimiva 3104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁)
76		brralrspcev 5135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
77	56, 75, 76	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
78		suprzcl 12409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
79	53, 54, 77, 78	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
80	51, 79	eqeltrid 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
81	50, 80	sseldd 3923	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
82	81	nn0zd 12433	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83		zsubcl 12371	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 − 𝑀) ∈ ℤ)
84	48, 82, 83	syl2anr 597	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
85	84	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℤ)
86	47, 85	rpexpcld 13971	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ+)
87	86	rpred 12781	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ)
88	45, 87	remulcld 11014	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ ℝ)
89	43, 88	eqeltrd 2840	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℝ)
90		nnrecre 12024	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
91	90	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
92	22	absge0d 15165	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴‘𝑘)))
93	92	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴‘𝑘)))
94		nnre 11989	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
95	94	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
96		nnge1 12010	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 1 ≤ 𝑚)
97	96	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
98		1red 10985	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
99	85	zred 12435	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℝ)
100		simplr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
101	48	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
102	101	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
103	82	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
104		zltp1le 12379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
105	102, 103, 104	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
106	100, 105	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
107	19	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
108	107	nn0red 12303	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
109	108	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
110	81	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
111	110	nn0red 12303	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
112	111	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
113	109, 98, 112	leaddsub2d 11586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀 − 𝑘)))
114	106, 113	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀 − 𝑘))
115	108	recnd 11012	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
116	115	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
117	111	recnd 11012	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
118	117	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
119	116, 118	negsubdi2d 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘 − 𝑀) = (𝑀 − 𝑘))
120	114, 119	breqtrrd 5103	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘 − 𝑀))
121	98, 99, 120	lenegcon2d 11567	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ≤ -1)
122		neg1z 12365	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
123		eluz 12605	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 − 𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
124	85, 122, 123	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
125	121, 124	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ≥‘(𝑘 − 𝑀)))
126	95, 97, 125	leexp2ad 13980	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (𝑚↑-1))
127		nncn 11990	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
128	127	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
129		expn1 13801	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
130	128, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
131	126, 130	breqtrd 5101	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (1 / 𝑚))
132	87, 91, 45, 93, 131	lemul2ad 11924	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ≤ ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
133	24	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
134		nnne0 12016	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
135	134	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
136	133, 128, 135	divrecd 11763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
137	34, 136	eqtrd 2779	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
138	132, 43, 137	3brtr4d 5107	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚))
139	86	rpge0d 12785	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘 − 𝑀)))
140	45, 87, 93, 139	mulge0d 11561	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
141	140, 43	breqtrrd 5103	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
142	1, 4, 26, 29, 37, 89, 138, 141	climsqz2 15360	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
143	27	mptex 7108	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
144	143	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
145	38	oveq2d 7300	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
146		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))
147		ovex 7317	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ V
148	145, 146, 147	fvmpt 6884	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
149	148	ad2antlr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
150	18	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
151	150, 19, 20	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
152	127	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
153	134	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
154	82	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
155	48, 154, 83	syl2anr 597	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
156	152, 153, 155	expclzd 13878	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
157	151, 156	mulcld 11004	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ ℂ)
158	149, 157	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
159	158	an32s 649	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
160	159	adantlr 712	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
161	87	recnd 11012	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
162	44, 161	absmuld 15175	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))))
163	87, 139	absidd 15143	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘 − 𝑀))) = (𝑚↑(𝑘 − 𝑀)))
164	163	oveq2d 7300	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
165	162, 164	eqtrd 2779	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
166	148	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
167	166	fveq2d 6787	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) = (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))))
168	165, 167, 43	3eqtr4rd 2790	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)))
169	1, 4, 144, 29, 160, 168	climabs0 15303	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0))
170	142, 169	mpbird 256	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
171	108	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
172		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
173	171, 172	ltned 11120	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ≠ 𝑀)
174		velsn 4578	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
175	174	necon3bbii 2992	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ {𝑀} ↔ 𝑘 ≠ 𝑀)
176	173, 175	sylibr 233	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
177	176	iffalsed 4471	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
178	170, 177	breqtrrd 5103	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
179		nncn 11990	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
180	179	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ∈ ℂ)
181		nnne0 12016	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
182	181	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ≠ 0)
183	84	ad3antrrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑘 − 𝑀) ∈ ℤ)
184	180, 182, 183	expclzd 13878	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑛↑(𝑘 − 𝑀)) ∈ ℂ)
185	184	mul02d 11182	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (0 · (𝑛↑(𝑘 − 𝑀))) = 0)
186		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)
187	186	oveq1d 7299	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = (0 · (𝑛↑(𝑘 − 𝑀))))
188	186	ifeq1d 4479	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
189		ifid 4500	. . . . . . . . . . . . 13 ⊢ if(𝑘 ∈ {𝑀}, 0, 0) = 0
190	188, 189	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
191	185, 187, 190	3eqtr4d 2789	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
192	21	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝐴‘𝑘) ∈ ℂ)
193	192	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ℂ)
194	193	mulid1d 11001	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · 1) = (𝐴‘𝑘))
195		nn0ssre 12246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ0 ⊆ ℝ
196	50, 195	sstrdi 3934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
197	196	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
198	54	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
199	77	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
200	19	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
201		ffvelrn 6968	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
202	17, 19, 201	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
203	202	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
204		eldifsn 4721	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
205	203, 204	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
206		difun2 4415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
207	205, 206	eleqtrdi 2850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))
208		elpreima 6944	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 Fn ℕ0 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
209	57, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
210	209	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
211	200, 207, 210	mpbir2and 710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
212	197, 198, 199, 211	suprubd 11946	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
213	212, 51	breqtrrdi 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
214	213	ad4ant14 749	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
215		simpllr 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ≤ 𝑘)
216	108	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℝ)
217	111	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℝ)
218	216, 217	letri3d 11126	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘)))
219	214, 215, 218	mpbir2and 710	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 = 𝑀)
220	219	oveq1d 7299	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = (𝑀 − 𝑀))
221	117	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℂ)
222	221	subidd 11329	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑀 − 𝑀) = 0)
223	220, 222	eqtrd 2779	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = 0)
224	223	oveq2d 7300	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = (𝑛↑0))
225	179	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑛 ∈ ℂ)
226	225	exp0d 13867	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑0) = 1)
227	224, 226	eqtrd 2779	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = 1)
228	227	oveq2d 7300	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · 1))
229	219, 174	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
230	229	iftrued 4468	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑘))
231	194, 228, 230	3eqtr4d 2789	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
232	191, 231	pm2.61dane 3033	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
233	232	mpteq2dva 5175	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)))
234		fconstmpt 5650	. . . . . . . . 9 ⊢ (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
235	233, 234	eqtr4di 2797	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}))
236		ifcl 4505	. . . . . . . . . 10 ⊢ (((𝐴‘𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
237	192, 7, 236	sylancl 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
238		1z 12359	. . . . . . . . 9 ⊢ 1 ∈ ℤ
239	1	eqimss2i 3981	. . . . . . . . . 10 ⊢ (ℤ≥‘1) ⊆ ℕ
240	239, 27	climconst2 15266	. . . . . . . . 9 ⊢ ((if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
241	237, 238, 240	sylancl 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
242	235, 241	eqbrtrd 5097	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
243	178, 242, 108, 111	ltlecasei 11092	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
244		snex 5355	. . . . . . . 8 ⊢ {0} ∈ V
245	27, 244	xpex 7612	. . . . . . 7 ⊢ (ℕ × {0}) ∈ V
246	245	a1i 11	. . . . . 6 ⊢ (𝜑 → (ℕ × {0}) ∈ V)
247	159	anasss 467	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
248		plyeq0.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
249	248	fveq1d 6785	. . . . . . . . . . 11 ⊢ (𝜑 → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
250	249	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
251	127	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
252		0pval 24844	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → (0𝑝‘𝑚) = 0)
253	251, 252	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = 0)
254		oveq1 7291	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑚 → (𝑧↑𝑘) = (𝑚↑𝑘))
255	254	oveq2d 7300	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑚 → ((𝐴‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑚↑𝑘)))
256	255	sumeq2sdv 15425	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
257		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))
258		sumex 15408	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ V
259	256, 257, 258	fvmpt 6884	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
260	251, 259	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
261	250, 253, 260	3eqtr3d 2787	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
262	261	oveq1d 7299	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
263		expcl 13809	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚↑𝑀) ∈ ℂ)
264	127, 81, 263	syl2anr 597	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ∈ ℂ)
265	134	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
266	251, 265, 154	expne0d 13879	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ≠ 0)
267	264, 266	div0d 11759	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = 0)
268		fzfid 13702	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
269		expcl 13809	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚↑𝑘) ∈ ℂ)
270	251, 19, 269	syl2an 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑘) ∈ ℂ)
271	151, 270	mulcld 11004	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ ℂ)
272	268, 264, 271, 266	fsumdivc 15507	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
273	262, 267, 272	3eqtr3d 2787	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
274		fvconst2g 7086	. . . . . . . 8 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
275	8, 274	sylan 580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
276	154	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
277	48	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
278	152, 153, 276, 277	expsubd 13884	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) = ((𝑚↑𝑘) / (𝑚↑𝑀)))
279	278	oveq2d 7300	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
280	264	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ∈ ℂ)
281	266	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ≠ 0)
282	151, 270, 280, 281	divassd 11795	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
283	279, 149, 282	3eqtr4d 2789	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
284	283	sumeq2dv 15424	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
285	273, 275, 284	3eqtr4d 2789	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
286	1, 2, 3, 243, 246, 247, 285	climfsum 15541	. . . . 5 ⊢ (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
287		suprleub 11950	. . . . . . . . . . . 12 ⊢ ((((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) ∧ 𝑁 ∈ ℝ) → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
288	196, 54, 77, 56, 287	syl31anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
289	75, 288	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
290	51, 289	eqbrtrid 5110	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
291		nn0uz 12629	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
292	81, 291	eleqtrdi 2850	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
293	55	nn0zd 12433	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
294		elfz5 13257	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
295	292, 293, 294	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
296	290, 295	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
297	296	snssd 4743	. . . . . . 7 ⊢ (𝜑 → {𝑀} ⊆ (0...𝑁))
298	18, 81	ffvelrnd 6971	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ)
299		elsni 4579	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
300	299	fveq2d 6787	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑀} → (𝐴‘𝑘) = (𝐴‘𝑀))
301	300	eleq1d 2824	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑀} → ((𝐴‘𝑘) ∈ ℂ ↔ (𝐴‘𝑀) ∈ ℂ))
302	298, 301	syl5ibrcom 246	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ {𝑀} → (𝐴‘𝑘) ∈ ℂ))
303	302	ralrimiv 3103	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ)
304	3	olcd 871	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin))
305		sumss2 15447	. . . . . . 7 ⊢ ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
306	297, 303, 304, 305	syl21anc 835	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
307		ltso 11064	. . . . . . . . 9 ⊢ < Or ℝ
308	307	supex 9231	. . . . . . . 8 ⊢ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
309	51, 308	eqeltri 2836	. . . . . . 7 ⊢ 𝑀 ∈ V
310		fveq2 6783	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐴‘𝑘) = (𝐴‘𝑀))
311	310	sumsn 15467	. . . . . . 7 ⊢ ((𝑀 ∈ V ∧ (𝐴‘𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
312	309, 298, 311	sylancr 587	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
313	306, 312	eqtr3d 2781	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑀))
314	286, 313	breqtrd 5101	. . . 4 ⊢ (𝜑 → (ℕ × {0}) ⇝ (𝐴‘𝑀))
315	239, 27	climconst2 15266	. . . . 5 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
316	7, 238, 315	mp2an 689	. . . 4 ⊢ (ℕ × {0}) ⇝ 0
317		climuni 15270	. . . 4 ⊢ (((ℕ × {0}) ⇝ (𝐴‘𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴‘𝑀) = 0)
318	314, 316, 317	sylancl 586	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) = 0)
319		fvex 6796	. . . 4 ⊢ (𝐴‘𝑀) ∈ V
320	319	elsn 4577	. . 3 ⊢ ((𝐴‘𝑀) ∈ {0} ↔ (𝐴‘𝑀) = 0)
321	318, 320	sylibr 233	. 2 ⊢ (𝜑 → (𝐴‘𝑀) ∈ {0})
322		elpreima 6944	. . . . . 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 496	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))
326	325	eldifbd 3901	. 2 ⊢ (𝜑 → ¬ (𝐴‘𝑀) ∈ {0})
327	321, 326	pm2.65i 193	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  Vcvv 3433   ∖ cdif 3885   ∪ cun 3886   ⊆ wss 3888  ∅c0 4257  ifcif 4460  {csn 4562   class class class wbr 5075   ↦ cmpt 5158   × cxp 5588  ^◡ccnv 5589   “ cima 5593   Fn wfn 6432  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284   ↑_m cmap 8624  Fincfn 8742  supcsup 9208  ℂcc 10878  ℝcr 10879  0cc0 10880  1c1 10881   + caddc 10883   · cmul 10885   < clt 11018   ≤ cle 11019   − cmin 11214  -cneg 11215   / cdiv 11641  ℕcn 11982  ℕ₀cn0 12242  ℤcz 12328  ℤ_≥cuz 12591  ℝ⁺crp 12739  ...cfz 13248  ↑cexp 13791  abscabs 14954   ⇝ cli 15202  Σcsu 15406  0_𝑝c0p 24842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-er 8507  df-map 8626  df-pm 8627  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-sup 9210  df-inf 9211  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-n0 12243  df-z 12329  df-uz 12592  df-rp 12740  df-fz 13249  df-fzo 13392  df-fl 13521  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-rlim 15207  df-sum 15407  df-0p 24843

This theorem is referenced by:  plyeq0  25381