Theorem plyeq0lem 26422

Description: Lemma for plyeq0 26423. 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 12921	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12644	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
3		fzfid 14031	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
4		1zzd 12644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5		plyeq0.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))
6		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7		0cn 11217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 ∈ ℂ)
9	8	snssd 4754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {0} ⊆ ℂ)
10	6, 9	unssd 4145	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11		cnex 11200	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂ ∈ V
12		ssexg 5292	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
13	10, 11, 12	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V)
14		nn0ex 12529	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
15		elmapg 8842	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
16	13, 14, 15	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
17	5, 16	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
18	17, 10	fssd 6727	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
19		elfznn0 13669	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20		ffvelcdm 7080	. . . . . . . . . . . . . . 15 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
21	18, 19, 20	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
22	21	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴‘𝑘) ∈ ℂ)
23	22	abscld 15518	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
24	23	recnd 11256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
25		divcnv 15934	. . . . . . . . . . 11 ⊢ ((abs‘(𝐴‘𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
26	24, 25	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
27		nnex 12258	. . . . . . . . . . . 12 ⊢ ℕ ∈ V
28	27	mptex 7228	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
29	28	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
30		oveq2 7427	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) / 𝑛) = ((abs‘(𝐴‘𝑘)) / 𝑚))
31		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))
32		ovex 7452	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ V
33	30, 31, 32	fvmpt 6993	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
34	33	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
35		nndivre 12296	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴‘𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
36	23, 35	sylan 592	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
37	34, 36	eqeltrd 2865	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38		oveq1 7426	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → (𝑛↑(𝑘 − 𝑀)) = (𝑚↑(𝑘 − 𝑀)))
39	38	oveq2d 7435	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
40		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))
41		ovex 7452	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ V
42	39, 40, 41	fvmpt 6993	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
43	42	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
44	21	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴‘𝑘) ∈ ℂ)
45	44	abscld 15518	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
46		nnrp 13048	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
47	46	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48		elfzelz 13572	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49		cnvimass 6086	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
50	49, 17	fssdm 6729	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
51		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < )
52		nn0ssz 12633	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ⊆ ℤ
53	50, 52	sstrdi 3950	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
54		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
55		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
56	55	nn0red 12585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℝ)
57	17	ffnd 6710	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 Fn ℕ0)
58		elpreima 7057	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 Fn ℕ0 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
59	57, 58	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
60	59	simplbda 505	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))
61		eldifsni 4760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑧) ∈ (𝑆 ∖ {0}) → (𝐴‘𝑧) ≠ 0)
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ≠ 0)
63		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑧 → (𝐴‘𝑘) = (𝐴‘𝑧))
64	63	neeq1d 3019	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → ((𝐴‘𝑘) ≠ 0 ↔ (𝐴‘𝑧) ≠ 0))
65		breq1 5114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → (𝑘 ≤ 𝑁 ↔ 𝑧 ≤ 𝑁))
66	64, 65	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑧 → (((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁)))
67		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})
68		plyco0 26404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
69	55, 18, 68	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
70	67, 69	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
71	70	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
72	50	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
73	66, 71, 72	rspcdva 3584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁))
74	62, 73	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ≤ 𝑁)
75	74	ralrimiva 3159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁)
76		brralrspcev 5173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
77	56, 75, 76	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
78		suprzcl 12696	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
79	53, 54, 77, 78	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
80	51, 79	eqeltrid 2869	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
81	50, 80	sseldd 3939	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
82	81	nn0zd 12635	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83		zsubcl 12655	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 − 𝑀) ∈ ℤ)
84	48, 82, 83	syl2anr 609	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
85	84	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℤ)
86	47, 85	rpexpcld 14305	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ+)
87	86	rpred 13080	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ)
88	45, 87	remulcld 11258	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ ℝ)
89	43, 88	eqeltrd 2865	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℝ)
90		nnrecre 12297	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
91	90	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
92	22	absge0d 15526	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴‘𝑘)))
93	92	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴‘𝑘)))
94		nnre 12259	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
95	94	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
96		nnge1 12283	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 1 ≤ 𝑚)
97	96	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
98		1red 11228	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
99	85	zred 12720	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℝ)
100		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
101	48	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
102	101	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
103	82	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
104		zltp1le 12663	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
105	102, 103, 104	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
106	100, 105	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
107	19	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
108	107	nn0red 12585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
109	108	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
110	81	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
111	110	nn0red 12585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
112	111	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
113	109, 98, 112	leaddsub2d 11835	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀 − 𝑘)))
114	106, 113	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀 − 𝑘))
115	108	recnd 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
116	115	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
117	111	recnd 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
118	117	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
119	116, 118	negsubdi2d 11604	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘 − 𝑀) = (𝑀 − 𝑘))
120	114, 119	breqtrrd 5141	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘 − 𝑀))
121	98, 99, 120	lenegcon2d 11816	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ≤ -1)
122		neg1z 12649	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
123		eluz 12896	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 − 𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
124	85, 122, 123	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
125	121, 124	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ≥‘(𝑘 − 𝑀)))
126	95, 97, 125	leexp2ad 14312	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (𝑚↑-1))
127		nncn 12260	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
128	127	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
129		expn1 14129	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
130	128, 129	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
131	126, 130	breqtrd 5139	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (1 / 𝑚))
132	87, 91, 45, 93, 131	lemul2ad 12174	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ≤ ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
133	24	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
134		nnne0 12289	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
135	134	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
136	133, 128, 135	divrecd 12013	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
137	34, 136	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
138	132, 43, 137	3brtr4d 5145	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚))
139	86	rpge0d 13084	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘 − 𝑀)))
140	45, 87, 93, 139	mulge0d 11810	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
141	140, 43	breqtrrd 5141	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
142	1, 4, 26, 29, 37, 89, 138, 141	climsqz2 15721	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
143	27	mptex 7228	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
144	143	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
145	38	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
146		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))
147		ovex 7452	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ V
148	145, 146, 147	fvmpt 6993	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
149	148	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
150	18	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
151	150, 19, 20	syl2an 608	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
152	127	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
153	134	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
154	82	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
155	48, 154, 83	syl2anr 609	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
156	152, 153, 155	expclzd 14209	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
157	151, 156	mulcld 11248	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ ℂ)
158	149, 157	eqeltrd 2865	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
159	158	an32s 665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
160	159	adantlr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
161	87	recnd 11256	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
162	44, 161	absmuld 15536	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))))
163	87, 139	absidd 15502	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘 − 𝑀))) = (𝑚↑(𝑘 − 𝑀)))
164	163	oveq2d 7435	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
165	162, 164	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
166	148	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
167	166	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) = (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))))
168	165, 167, 43	3eqtr4rd 2811	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)))
169	1, 4, 144, 29, 160, 168	climabs0 15664	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0))
170	142, 169	mpbird 260	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
171	108	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
172		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
173	171, 172	ltned 11365	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ≠ 𝑀)
174		velsn 4607	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
175	174	necon3bbii 3007	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ {𝑀} ↔ 𝑘 ≠ 𝑀)
176	173, 175	sylibr 237	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
177	176	iffalsed 4500	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
178	170, 177	breqtrrd 5141	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
179		nncn 12260	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
180	179	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ∈ ℂ)
181		nnne0 12289	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
182	181	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ≠ 0)
183	84	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑘 − 𝑀) ∈ ℤ)
184	180, 182, 183	expclzd 14209	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑛↑(𝑘 − 𝑀)) ∈ ℂ)
185	184	mul02d 11427	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (0 · (𝑛↑(𝑘 − 𝑀))) = 0)
186		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)
187	186	oveq1d 7434	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = (0 · (𝑛↑(𝑘 − 𝑀))))
188	186	ifeq1d 4509	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
189		ifid 4530	. . . . . . . . . . . . 13 ⊢ if(𝑘 ∈ {𝑀}, 0, 0) = 0
190	188, 189	eqtrdi 2816	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
191	185, 187, 190	3eqtr4d 2810	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
192	21	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝐴‘𝑘) ∈ ℂ)
193	192	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ℂ)
194	193	mulridd 11245	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · 1) = (𝐴‘𝑘))
195		nn0ssre 12527	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ0 ⊆ ℝ
196	50, 195	sstrdi 3950	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
197	196	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
198	54	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
199	77	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
200	19	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
201		ffvelcdm 7080	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
202	17, 19, 201	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
203	202	anim1i 627	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
204		eldifsn 4755	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
205	203, 204	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
206		difun2 4444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
207	205, 206	eleqtrdi 2875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))
208		elpreima 7057	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 Fn ℕ0 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
209	57, 208	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
210	209	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
211	200, 207, 210	mpbir2and 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
212	197, 198, 199, 211	suprubd 12196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
213	212, 51	breqtrrdi 5155	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
214	213	ad4ant14 765	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
215		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ≤ 𝑘)
216	108	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℝ)
217	111	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℝ)
218	216, 217	letri3d 11371	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘)))
219	214, 215, 218	mpbir2and 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 = 𝑀)
220	219	oveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = (𝑀 − 𝑀))
221	117	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℂ)
222	221	subidd 11576	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑀 − 𝑀) = 0)
223	220, 222	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = 0)
224	223	oveq2d 7435	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = (𝑛↑0))
225	179	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑛 ∈ ℂ)
226	225	exp0d 14198	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑0) = 1)
227	224, 226	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = 1)
228	227	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · 1))
229	219, 174	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
230	229	iftrued 4497	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑘))
231	194, 228, 230	3eqtr4d 2810	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
232	191, 231	pm2.61dane 3047	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
233	232	mpteq2dva 5206	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)))
234		fconstmpt 5725	. . . . . . . . 9 ⊢ (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
235	233, 234	eqtr4di 2818	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}))
236		ifcl 4535	. . . . . . . . . 10 ⊢ (((𝐴‘𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
237	192, 7, 236	sylancl 598	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
238		1z 12643	. . . . . . . . 9 ⊢ 1 ∈ ℤ
239	1	eqimss2i 3999	. . . . . . . . . 10 ⊢ (ℤ≥‘1) ⊆ ℕ
240	239, 27	climconst2 15627	. . . . . . . . 9 ⊢ ((if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
241	237, 238, 240	sylancl 598	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
242	235, 241	eqbrtrd 5135	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
243	178, 242, 108, 111	ltlecasei 11337	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
244		snex 5412	. . . . . . . 8 ⊢ {0} ∈ V
245	27, 244	xpex 7758	. . . . . . 7 ⊢ (ℕ × {0}) ∈ V
246	245	a1i 11	. . . . . 6 ⊢ (𝜑 → (ℕ × {0}) ∈ V)
247	159	anasss 472	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
248		plyeq0.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
249	248	fveq1d 6887	. . . . . . . . . . 11 ⊢ (𝜑 → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
250	249	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
251	127	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
252		0pval 25885	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → (0𝑝‘𝑚) = 0)
253	251, 252	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = 0)
254		oveq1 7426	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑚 → (𝑧↑𝑘) = (𝑚↑𝑘))
255	254	oveq2d 7435	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑚 → ((𝐴‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑚↑𝑘)))
256	255	sumeq2sdv 15782	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
257		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))
258		sumex 15767	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ V
259	256, 257, 258	fvmpt 6993	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
260	251, 259	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
261	250, 253, 260	3eqtr3d 2808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
262	261	oveq1d 7434	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
263		expcl 14137	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚↑𝑀) ∈ ℂ)
264	127, 81, 263	syl2anr 609	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ∈ ℂ)
265	134	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
266	251, 265, 154	expne0d 14210	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ≠ 0)
267	264, 266	div0d 12009	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = 0)
268		fzfid 14031	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
269		expcl 14137	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚↑𝑘) ∈ ℂ)
270	251, 19, 269	syl2an 608	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑘) ∈ ℂ)
271	151, 270	mulcld 11248	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ ℂ)
272	268, 264, 271, 266	fsumdivc 15864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
273	262, 267, 272	3eqtr3d 2808	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
274		fvconst2g 7207	. . . . . . . 8 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
275	8, 274	sylan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
276	154	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
277	48	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
278	152, 153, 276, 277	expsubd 14215	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) = ((𝑚↑𝑘) / (𝑚↑𝑀)))
279	278	oveq2d 7435	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
280	264	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ∈ ℂ)
281	266	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ≠ 0)
282	151, 270, 280, 281	divassd 12045	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
283	279, 149, 282	3eqtr4d 2810	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
284	283	sumeq2dv 15781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
285	273, 275, 284	3eqtr4d 2810	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
286	1, 2, 3, 243, 246, 247, 285	climfsum 15899	. . . . 5 ⊢ (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
287		suprleub 12200	. . . . . . . . . . . 12 ⊢ ((((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) ∧ 𝑁 ∈ ℝ) → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
288	196, 54, 77, 56, 287	syl31anc 1400	. . . . . . . . . . 11 ⊢ (𝜑 → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
289	75, 288	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
290	51, 289	eqbrtrid 5148	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
291		nn0uz 12920	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
292	81, 291	eleqtrdi 2875	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
293	55	nn0zd 12635	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
294		elfz5 13564	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
295	292, 293, 294	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
296	290, 295	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
297	296	snssd 4754	. . . . . . 7 ⊢ (𝜑 → {𝑀} ⊆ (0...𝑁))
298	18, 81	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ)
299		elsni 4608	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
300	299	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑀} → (𝐴‘𝑘) = (𝐴‘𝑀))
301	300	eleq1d 2850	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑀} → ((𝐴‘𝑘) ∈ ℂ ↔ (𝐴‘𝑀) ∈ ℂ))
302	298, 301	syl5ibrcom 250	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ {𝑀} → (𝐴‘𝑘) ∈ ℂ))
303	302	ralrimiv 3158	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ)
304	3	olcd 888	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin))
305		sumss2 15804	. . . . . . 7 ⊢ ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
306	297, 303, 304, 305	syl21anc 851	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
307		ltso 11309	. . . . . . . . 9 ⊢ < Or ℝ
308	307	supex 9431	. . . . . . . 8 ⊢ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
309	51, 308	eqeltri 2861	. . . . . . 7 ⊢ 𝑀 ∈ V
310		fveq2 6885	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐴‘𝑘) = (𝐴‘𝑀))
311	310	sumsn 15824	. . . . . . 7 ⊢ ((𝑀 ∈ V ∧ (𝐴‘𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
312	309, 298, 311	sylancr 599	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
313	306, 312	eqtr3d 2802	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑀))
314	286, 313	breqtrd 5139	. . . 4 ⊢ (𝜑 → (ℕ × {0}) ⇝ (𝐴‘𝑀))
315	239, 27	climconst2 15627	. . . . 5 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
316	7, 238, 315	mp2an 705	. . . 4 ⊢ (ℕ × {0}) ⇝ 0
317		climuni 15631	. . . 4 ⊢ (((ℕ × {0}) ⇝ (𝐴‘𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴‘𝑀) = 0)
318	314, 316, 317	sylancl 598	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) = 0)
319		fvex 6898	. . . 4 ⊢ (𝐴‘𝑀) ∈ V
320	319	elsn 4606	. . 3 ⊢ ((𝐴‘𝑀) ∈ {0} ↔ (𝐴‘𝑀) = 0)
321	318, 320	sylibr 237	. 2 ⊢ (𝜑 → (𝐴‘𝑀) ∈ {0})
322		elpreima 7057	. . . . . 6 ⊢ (𝐴 Fn ℕ0 → (𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))))
323	57, 322	syl 18	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))))
324	80, 323	mpbid 235	. . . 4 ⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ∈ (𝑆 ∖ {0})))
325	324	simprd 501	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))
326	325	eldifbd 3919	. 2 ⊢ (𝜑 → ¬ (𝐴‘𝑀) ∈ {0})
327	321, 326	pm2.65i 196	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ⊆ wss 3906  ∅c0 4286  ifcif 4489  {csn 4591   class class class wbr 5111   ↦ cmpt 5194   × cxp 5661  ^◡ccnv 5662   “ cima 5666   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419   ↑_m cmap 8830  Fincfn 8949  supcsup 9407  ℂcc 11117  ℝcr 11118  0cc0 11119  1c1 11120   + caddc 11122   · cmul 11124   < clt 11262   ≤ cle 11263   − cmin 11460  -cneg 11461   / cdiv 11890  ℕcn 12252  ℕ₀cn0 12523  ℤcz 12610  ℤ_≥cuz 12882  ℝ⁺crp 13036  ...cfz 13555  ↑cexp 14119  abscabs 15313   ⇝ cli 15563  Σcsu 15765  0_𝑝c0p 25883

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-inf2 9617  ax-cnex 11175  ax-resscn 11176  ax-1cn 11177  ax-icn 11178  ax-addcl 11179  ax-addrcl 11180  ax-mulcl 11181  ax-mulrcl 11182  ax-mulcom 11183  ax-addass 11184  ax-mulass 11185  ax-distr 11186  ax-i2m1 11187  ax-1ne0 11188  ax-1rid 11189  ax-rnegex 11190  ax-rrecex 11191  ax-cnre 11192  ax-pre-lttri 11193  ax-pre-lttrn 11194  ax-pre-ltadd 11195  ax-pre-mulgt0 11196  ax-pre-sup 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-er 8700  df-map 8832  df-pm 8833  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-sup 9409  df-inf 9410  df-oi 9479  df-card 9941  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11462  df-neg 11463  df-div 11891  df-nn 12253  df-2 12322  df-3 12323  df-n0 12524  df-z 12611  df-uz 12883  df-rp 13037  df-fz 13556  df-fzo 13704  df-fl 13847  df-seq 14060  df-exp 14120  df-hash 14389  df-cj 15178  df-re 15179  df-im 15180  df-sqrt 15314  df-abs 15315  df-clim 15567  df-rlim 15568  df-sum 15766  df-0p 25884

This theorem is used by:  plyeq0  26423