Theorem plyeq0lem 26160

Description: Lemma for plyeq0 26161. 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 12893	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12621	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
3		fzfid 13968	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
4		1zzd 12621	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 1 ∈ ℤ)
5		plyeq0.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))
6		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7		0cn 11234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 ∈ ℂ)
9	8	snssd 4808	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {0} ⊆ ℂ)
10	6, 9	unssd 4180	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
11		cnex 11217	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂ ∈ V
12		ssexg 5318	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∪ {0}) ⊆ ℂ ∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V)
13	10, 11, 12	sylancl 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 ∪ {0}) ∈ V)
14		nn0ex 12506	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
15		elmapg 8854	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∪ {0}) ∈ V ∧ ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
16	13, 14, 15	sylancl 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0})))
17	5, 16	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))
18	17, 10	fssd 6734	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
19		elfznn0 13624	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
20		ffvelcdm 7085	. . . . . . . . . . . . . . 15 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
21	18, 19, 20	syl2an 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
22	21	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝐴‘𝑘) ∈ ℂ)
23	22	abscld 15413	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
24	23	recnd 11270	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
25		divcnv 15829	. . . . . . . . . . 11 ⊢ ((abs‘(𝐴‘𝑘)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
26	24, 25	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) ⇝ 0)
27		nnex 12246	. . . . . . . . . . . 12 ⊢ ℕ ∈ V
28	27	mptex 7230	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
29	28	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
30		oveq2 7423	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) / 𝑛) = ((abs‘(𝐴‘𝑘)) / 𝑚))
31		eqid 2725	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))
32		ovex 7448	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ V
33	30, 31, 32	fvmpt 6999	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
34	33	adantl 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) / 𝑚))
35		nndivre 12281	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴‘𝑘)) ∈ ℝ ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
36	23, 35	sylan 578	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) ∈ ℝ)
37	34, 36	eqeltrd 2825	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) ∈ ℝ)
38		oveq1 7422	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → (𝑛↑(𝑘 − 𝑀)) = (𝑚↑(𝑘 − 𝑀)))
39	38	oveq2d 7431	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
40		eqid 2725	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))
41		ovex 7448	. . . . . . . . . . . . 13 ⊢ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ V
42	39, 40, 41	fvmpt 6999	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
43	42	adantl 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
44	21	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝐴‘𝑘) ∈ ℂ)
45	44	abscld 15413	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
46		nnrp 13015	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
47	46	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
48		elfzelz 13531	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
49		cnvimass 6080	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝐴 “ (𝑆 ∖ {0})) ⊆ dom 𝐴
50	49, 17	fssdm 6736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℕ0)
51		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < )
52		nn0ssz 12609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ⊆ ℤ
53	50, 52	sstrdi 3985	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ)
54		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
55		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
56	55	nn0red 12561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℝ)
57	17	ffnd 6717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 Fn ℕ0)
58		elpreima 7061	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 Fn ℕ0 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑧 ∈ ℕ0 ∧ (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))))
60	59	simplbda 498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ∈ (𝑆 ∖ {0}))
61		eldifsni 4789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑧) ∈ (𝑆 ∖ {0}) → (𝐴‘𝑧) ≠ 0)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → (𝐴‘𝑧) ≠ 0)
63		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑧 → (𝐴‘𝑘) = (𝐴‘𝑧))
64	63	neeq1d 2990	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → ((𝐴‘𝑘) ≠ 0 ↔ (𝐴‘𝑧) ≠ 0))
65		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑧 → (𝑘 ≤ 𝑁 ↔ 𝑧 ≤ 𝑁))
66	64, 65	imbi12d 343	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑧 → (((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁)))
67		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})
68		plyco0 26142	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
69	55, 18, 68	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)))
70	67, 69	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
71	70	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
72	50	sselda 3972	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ∈ ℕ0)
73	66, 71, 72	rspcdva 3603	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → ((𝐴‘𝑧) ≠ 0 → 𝑧 ≤ 𝑁))
74	62, 73	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))) → 𝑧 ≤ 𝑁)
75	74	ralrimiva 3136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁)
76		brralrspcev 5203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
77	56, 75, 76	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
78		suprzcl 12670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℤ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
79	53, 54, 77, 78	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ (◡𝐴 “ (𝑆 ∖ {0})))
80	51, 79	eqeltrid 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
81	50, 80	sseldd 3973	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
82	81	nn0zd 12612	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83		zsubcl 12632	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 − 𝑀) ∈ ℤ)
84	48, 82, 83	syl2anr 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
85	84	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℤ)
86	47, 85	rpexpcld 14239	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ+)
87	86	rpred 13046	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℝ)
88	45, 87	remulcld 11272	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ∈ ℝ)
89	43, 88	eqeltrd 2825	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℝ)
90		nnrecre 12282	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
91	90	adantl 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
92	22	absge0d 15421	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 0 ≤ (abs‘(𝐴‘𝑘)))
93	92	adantr 479	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (abs‘(𝐴‘𝑘)))
94		nnre 12247	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
95	94	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
96		nnge1 12268	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 1 ≤ 𝑚)
97	96	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ 𝑚)
98		1red 11243	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ∈ ℝ)
99	85	zred 12694	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ∈ ℝ)
100		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 < 𝑀)
101	48	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
102	101	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℤ)
103	82	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
104		zltp1le 12640	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
105	102, 103, 104	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 < 𝑀 ↔ (𝑘 + 1) ≤ 𝑀))
106	100, 105	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 + 1) ≤ 𝑀)
107	19	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
108	107	nn0red 12561	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
109	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℝ)
110	81	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℕ0)
111	110	nn0red 12561	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℝ)
112	111	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℝ)
113	109, 98, 112	leaddsub2d 11844	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑘 + 1) ≤ 𝑀 ↔ 1 ≤ (𝑀 − 𝑘)))
114	106, 113	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ (𝑀 − 𝑘))
115	108	recnd 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
116	115	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑘 ∈ ℂ)
117	111	recnd 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℂ)
118	117	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℂ)
119	116, 118	negsubdi2d 11615	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -(𝑘 − 𝑀) = (𝑀 − 𝑘))
120	114, 119	breqtrrd 5171	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 1 ≤ -(𝑘 − 𝑀))
121	98, 99, 120	lenegcon2d 11825	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑘 − 𝑀) ≤ -1)
122		neg1z 12626	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
123		eluz 12864	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 − 𝑀) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
124	85, 122, 123	sylancl 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (-1 ∈ (ℤ≥‘(𝑘 − 𝑀)) ↔ (𝑘 − 𝑀) ≤ -1))
125	121, 124	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → -1 ∈ (ℤ≥‘(𝑘 − 𝑀)))
126	95, 97, 125	leexp2ad 14246	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (𝑚↑-1))
127		nncn 12248	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
128	127	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
129		expn1 14066	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℂ → (𝑚↑-1) = (1 / 𝑚))
130	128, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑-1) = (1 / 𝑚))
131	126, 130	breqtrd 5169	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ≤ (1 / 𝑚))
132	87, 91, 45, 93, 131	lemul2ad 12182	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))) ≤ ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
133	24	adantr 479	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
134		nnne0 12274	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
135	134	adantl 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
136	133, 128, 135	divrecd 12021	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) / 𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
137	34, 136	eqtrd 2765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚) = ((abs‘(𝐴‘𝑘)) · (1 / 𝑚)))
138	132, 43, 137	3brtr4d 5175	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) / 𝑛))‘𝑚))
139	86	rpge0d 13050	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ (𝑚↑(𝑘 − 𝑀)))
140	45, 87, 93, 139	mulge0d 11819	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
141	140, 43	breqtrrd 5171	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
142	1, 4, 26, 29, 37, 89, 138, 141	climsqz2 15616	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
143	27	mptex 7230	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V
144	143	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ∈ V)
145	38	oveq2d 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
146		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))
147		ovex 7448	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ V
148	145, 146, 147	fvmpt 6999	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
149	148	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
150	18	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
151	150, 19, 20	syl2an 594	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
152	127	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ∈ ℂ)
153	134	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑚 ≠ 0)
154	82	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑀 ∈ ℤ)
155	48, 154, 83	syl2anr 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 − 𝑀) ∈ ℤ)
156	152, 153, 155	expclzd 14145	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
157	151, 156	mulcld 11262	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) ∈ ℂ)
158	149, 157	eqeltrd 2825	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
159	158	an32s 650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
160	159	adantlr 713	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
161	87	recnd 11270	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (𝑚↑(𝑘 − 𝑀)) ∈ ℂ)
162	44, 161	absmuld 15431	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))))
163	87, 139	absidd 15399	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘(𝑚↑(𝑘 − 𝑀))) = (𝑚↑(𝑘 − 𝑀)))
164	163	oveq2d 7431	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
165	162, 164	eqtrd 2765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))) = ((abs‘(𝐴‘𝑘)) · (𝑚↑(𝑘 − 𝑀))))
166	148	adantl 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))))
167	166	fveq2d 6895	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)) = (abs‘((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀)))))
168	165, 167, 43	3eqtr4rd 2776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (abs‘((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚)))
169	1, 4, 144, 29, 160, 168	climabs0 15559	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘(𝐴‘𝑘)) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0))
170	142, 169	mpbird 256	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ 0)
171	108	adantr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
172		simpr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 < 𝑀)
173	171, 172	ltned 11378	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → 𝑘 ≠ 𝑀)
174		velsn 4640	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
175	174	necon3bbii 2978	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ {𝑀} ↔ 𝑘 ≠ 𝑀)
176	173, 175	sylibr 233	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → ¬ 𝑘 ∈ {𝑀})
177	176	iffalsed 4535	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
178	170, 177	breqtrrd 5171	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑘 < 𝑀) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
179		nncn 12248	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
180	179	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ∈ ℂ)
181		nnne0 12274	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
182	181	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → 𝑛 ≠ 0)
183	84	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑘 − 𝑀) ∈ ℤ)
184	180, 182, 183	expclzd 14145	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝑛↑(𝑘 − 𝑀)) ∈ ℂ)
185	184	mul02d 11440	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (0 · (𝑛↑(𝑘 − 𝑀))) = 0)
186		simpr 483	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)
187	186	oveq1d 7430	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = (0 · (𝑛↑(𝑘 − 𝑀))))
188	186	ifeq1d 4543	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = if(𝑘 ∈ {𝑀}, 0, 0))
189		ifid 4564	. . . . . . . . . . . . 13 ⊢ if(𝑘 ∈ {𝑀}, 0, 0) = 0
190	188, 189	eqtrdi 2781	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = 0)
191	185, 187, 190	3eqtr4d 2775	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) = 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
192	21	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝐴‘𝑘) ∈ ℂ)
193	192	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ℂ)
194	193	mulridd 11259	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · 1) = (𝐴‘𝑘))
195		nn0ssre 12504	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ0 ⊆ ℝ
196	50, 195	sstrdi 3985	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
197	196	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ)
198	54	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅)
199	77	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥)
200	19	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℕ0)
201		ffvelcdm 7085	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
202	17, 19, 201	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ (𝑆 ∪ {0}))
203	202	anim1i 613	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
204		eldifsn 4786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}) ↔ ((𝐴‘𝑘) ∈ (𝑆 ∪ {0}) ∧ (𝐴‘𝑘) ≠ 0))
205	203, 204	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ ((𝑆 ∪ {0}) ∖ {0}))
206		difun2 4476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∪ {0}) ∖ {0}) = (𝑆 ∖ {0})
207	205, 206	eleqtrdi 2835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))
208		elpreima 7061	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 Fn ℕ0 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
209	57, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
210	209	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})) ↔ (𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ∈ (𝑆 ∖ {0}))))
211	200, 207, 210	mpbir2and 711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ (◡𝐴 “ (𝑆 ∖ {0})))
212	197, 198, 199, 211	suprubd 12204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ))
213	212, 51	breqtrrdi 5185	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
214	213	ad4ant14 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑀)
215		simpllr 774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ≤ 𝑘)
216	108	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ ℝ)
217	111	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℝ)
218	216, 217	letri3d 11384	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 = 𝑀 ↔ (𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘)))
219	214, 215, 218	mpbir2and 711	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 = 𝑀)
220	219	oveq1d 7430	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = (𝑀 − 𝑀))
221	117	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑀 ∈ ℂ)
222	221	subidd 11587	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑀 − 𝑀) = 0)
223	220, 222	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑘 − 𝑀) = 0)
224	223	oveq2d 7431	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = (𝑛↑0))
225	179	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑛 ∈ ℂ)
226	225	exp0d 14134	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑0) = 1)
227	224, 226	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → (𝑛↑(𝑘 − 𝑀)) = 1)
228	227	oveq2d 7431	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · 1))
229	219, 174	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ∈ {𝑀})
230	229	iftrued 4532	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑘))
231	194, 228, 230	3eqtr4d 2775	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) ∧ (𝐴‘𝑘) ≠ 0) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
232	191, 231	pm2.61dane 3019	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))) = if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
233	232	mpteq2dva 5243	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)))
234		fconstmpt 5734	. . . . . . . . 9 ⊢ (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) = (𝑛 ∈ ℕ ↦ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
235	233, 234	eqtr4di 2783	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) = (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}))
236		ifcl 4569	. . . . . . . . . 10 ⊢ (((𝐴‘𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
237	192, 7, 236	sylancl 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ)
238		1z 12620	. . . . . . . . 9 ⊢ 1 ∈ ℤ
239	1	eqimss2i 4034	. . . . . . . . . 10 ⊢ (ℤ≥‘1) ⊆ ℕ
240	239, 27	climconst2 15522	. . . . . . . . 9 ⊢ ((if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
241	237, 238, 240	sylancl 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (ℕ × {if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0)}) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
242	235, 241	eqbrtrd 5165	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑀 ≤ 𝑘) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
243	178, 242, 108, 111	ltlecasei 11350	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀)))) ⇝ if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
244		snex 5427	. . . . . . . 8 ⊢ {0} ∈ V
245	27, 244	xpex 7752	. . . . . . 7 ⊢ (ℕ × {0}) ∈ V
246	245	a1i 11	. . . . . 6 ⊢ (𝜑 → (ℕ × {0}) ∈ V)
247	159	anasss 465	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) ∈ ℂ)
248		plyeq0.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
249	248	fveq1d 6893	. . . . . . . . . . 11 ⊢ (𝜑 → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
250	249	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚))
251	127	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
252		0pval 25616	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → (0𝑝‘𝑚) = 0)
253	251, 252	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0𝑝‘𝑚) = 0)
254		oveq1 7422	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑚 → (𝑧↑𝑘) = (𝑚↑𝑘))
255	254	oveq2d 7431	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑚 → ((𝐴‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑚↑𝑘)))
256	255	sumeq2sdv 15680	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑚 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
257		eqid 2725	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))
258		sumex 15664	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ V
259	256, 257, 258	fvmpt 6999	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℂ → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
260	251, 259	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
261	250, 253, 260	3eqtr3d 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)))
262	261	oveq1d 7430	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
263		expcl 14074	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑚↑𝑀) ∈ ℂ)
264	127, 81, 263	syl2anr 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ∈ ℂ)
265	134	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
266	251, 265, 154	expne0d 14146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚↑𝑀) ≠ 0)
267	264, 266	div0d 12017	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0 / (𝑚↑𝑀)) = 0)
268		fzfid 13968	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...𝑁) ∈ Fin)
269		expcl 14074	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑚↑𝑘) ∈ ℂ)
270	251, 19, 269	syl2an 594	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑘) ∈ ℂ)
271	151, 270	mulcld 11262	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑𝑘)) ∈ ℂ)
272	268, 264, 271, 266	fsumdivc 15762	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
273	262, 267, 272	3eqtr3d 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
274		fvconst2g 7209	. . . . . . . 8 ⊢ ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
275	8, 274	sylan 578	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = 0)
276	154	adantr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑀 ∈ ℤ)
277	48	adantl 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
278	152, 153, 276, 277	expsubd 14151	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑(𝑘 − 𝑀)) = ((𝑚↑𝑘) / (𝑚↑𝑀)))
279	278	oveq2d 7431	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑚↑(𝑘 − 𝑀))) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
280	264	adantr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ∈ ℂ)
281	266	adantr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑚↑𝑀) ≠ 0)
282	151, 270, 280, 281	divassd 12053	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)) = ((𝐴‘𝑘) · ((𝑚↑𝑘) / (𝑚↑𝑀))))
283	279, 149, 282	3eqtr4d 2775	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = (((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
284	283	sumeq2dv 15679	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚) = Σ𝑘 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑚↑𝑘)) / (𝑚↑𝑀)))
285	273, 275, 284	3eqtr4d 2775	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ℕ × {0})‘𝑚) = Σ𝑘 ∈ (0...𝑁)((𝑛 ∈ ℕ ↦ ((𝐴‘𝑘) · (𝑛↑(𝑘 − 𝑀))))‘𝑚))
286	1, 2, 3, 243, 246, 247, 285	climfsum 15796	. . . . 5 ⊢ (𝜑 → (ℕ × {0}) ⇝ Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
287		suprleub 12208	. . . . . . . . . . . 12 ⊢ ((((◡𝐴 “ (𝑆 ∖ {0})) ⊆ ℝ ∧ (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑥) ∧ 𝑁 ∈ ℝ) → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
288	196, 54, 77, 56, 287	syl31anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → (sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁 ↔ ∀𝑧 ∈ (◡𝐴 “ (𝑆 ∖ {0}))𝑧 ≤ 𝑁))
289	75, 288	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ≤ 𝑁)
290	51, 289	eqbrtrid 5178	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
291		nn0uz 12892	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
292	81, 291	eleqtrdi 2835	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
293	55	nn0zd 12612	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
294		elfz5 13523	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
295	292, 293, 294	syl2anc 582	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≤ 𝑁))
296	290, 295	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
297	296	snssd 4808	. . . . . . 7 ⊢ (𝜑 → {𝑀} ⊆ (0...𝑁))
298	18, 81	ffvelcdmd 7089	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ)
299		elsni 4641	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑀} → 𝑘 = 𝑀)
300	299	fveq2d 6895	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑀} → (𝐴‘𝑘) = (𝐴‘𝑀))
301	300	eleq1d 2810	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑀} → ((𝐴‘𝑘) ∈ ℂ ↔ (𝐴‘𝑀) ∈ ℂ))
302	298, 301	syl5ibrcom 246	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ {𝑀} → (𝐴‘𝑘) ∈ ℂ))
303	302	ralrimiv 3135	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ)
304	3	olcd 872	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin))
305		sumss2 15702	. . . . . . 7 ⊢ ((({𝑀} ⊆ (0...𝑁) ∧ ∀𝑘 ∈ {𝑀} (𝐴‘𝑘) ∈ ℂ) ∧ ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
306	297, 303, 304, 305	syl21anc 836	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0))
307		ltso 11322	. . . . . . . . 9 ⊢ < Or ℝ
308	307	supex 9484	. . . . . . . 8 ⊢ sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) ∈ V
309	51, 308	eqeltri 2821	. . . . . . 7 ⊢ 𝑀 ∈ V
310		fveq2 6891	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐴‘𝑘) = (𝐴‘𝑀))
311	310	sumsn 15722	. . . . . . 7 ⊢ ((𝑀 ∈ V ∧ (𝐴‘𝑀) ∈ ℂ) → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
312	309, 298, 311	sylancr 585	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑀} (𝐴‘𝑘) = (𝐴‘𝑀))
313	306, 312	eqtr3d 2767	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)if(𝑘 ∈ {𝑀}, (𝐴‘𝑘), 0) = (𝐴‘𝑀))
314	286, 313	breqtrd 5169	. . . 4 ⊢ (𝜑 → (ℕ × {0}) ⇝ (𝐴‘𝑀))
315	239, 27	climconst2 15522	. . . . 5 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {0}) ⇝ 0)
316	7, 238, 315	mp2an 690	. . . 4 ⊢ (ℕ × {0}) ⇝ 0
317		climuni 15526	. . . 4 ⊢ (((ℕ × {0}) ⇝ (𝐴‘𝑀) ∧ (ℕ × {0}) ⇝ 0) → (𝐴‘𝑀) = 0)
318	314, 316, 317	sylancl 584	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) = 0)
319		fvex 6904	. . . 4 ⊢ (𝐴‘𝑀) ∈ V
320	319	elsn 4639	. . 3 ⊢ ((𝐴‘𝑀) ∈ {0} ↔ (𝐴‘𝑀) = 0)
321	318, 320	sylibr 233	. 2 ⊢ (𝜑 → (𝐴‘𝑀) ∈ {0})
322		elpreima 7061	. . . . . 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 494	. . 3 ⊢ (𝜑 → (𝐴‘𝑀) ∈ (𝑆 ∖ {0}))
326	325	eldifbd 3953	. 2 ⊢ (𝜑 → ¬ (𝐴‘𝑀) ∈ {0})
327	321, 326	pm2.65i 193	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098   ≠ wne 2930  ∀wral 3051  ∃wrex 3060  Vcvv 3463   ∖ cdif 3937   ∪ cun 3938   ⊆ wss 3940  ∅c0 4318  ifcif 4524  {csn 4624   class class class wbr 5143   ↦ cmpt 5226   × cxp 5670  ^◡ccnv 5671   “ cima 5675   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  (class class class)co 7415   ↑_m cmap 8841  Fincfn 8960  supcsup 9461  ℂcc 11134  ℝcr 11135  0cc0 11136  1c1 11137   + caddc 11139   · cmul 11141   < clt 11276   ≤ cle 11277   − cmin 11472  -cneg 11473   / cdiv 11899  ℕcn 12240  ℕ₀cn0 12500  ℤcz 12586  ℤ_≥cuz 12850  ℝ⁺crp 13004  ...cfz 13514  ↑cexp 14056  abscabs 15211   ⇝ cli 15458  Σcsu 15662  0_𝑝c0p 25614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-inf2 9662  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-1o 8483  df-er 8721  df-map 8843  df-pm 8844  df-en 8961  df-dom 8962  df-sdom 8963  df-fin 8964  df-sup 9463  df-inf 9464  df-oi 9531  df-card 9960  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-n0 12501  df-z 12587  df-uz 12851  df-rp 13005  df-fz 13515  df-fzo 13658  df-fl 13787  df-seq 13997  df-exp 14057  df-hash 14320  df-cj 15076  df-re 15077  df-im 15078  df-sqrt 15212  df-abs 15213  df-clim 15462  df-rlim 15463  df-sum 15663  df-0p 25615

This theorem is referenced by:  plyeq0  26161