Theorem dvradcnv 25589

Description: The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is at least as large as the radius of convergence of 𝐺. (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.)

Hypotheses

Ref	Expression
dvradcnv.g	⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
dvradcnv.r	⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
dvradcnv.h	⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
dvradcnv.a	⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
dvradcnv.x	⊢ (𝜑 → 𝑋 ∈ ℂ)
dvradcnv.l	⊢ (𝜑 → (abs‘𝑋) < 𝑅)

Assertion

Ref	Expression
dvradcnv	⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )

Distinct variable groups:   𝑥,𝑛,𝐴   𝐺,𝑟   𝑛,𝑟,𝑋,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝐴(𝑟)   𝑅(𝑥,𝑛,𝑟)   𝐺(𝑥,𝑛)   𝐻(𝑥,𝑛,𝑟)

Proof of Theorem dvradcnv

Dummy variables 𝑘 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 12629	. 2 ⊢ ℕ0 = (ℤ≥‘0)
2		1nn0 12258	. . 3 ⊢ 1 ∈ ℕ0
3	2	a1i 11	. 2 ⊢ (𝜑 → 1 ∈ ℕ0)
4		ax-1cn 10938	. . . . 5 ⊢ 1 ∈ ℂ
5		nn0cn 12252	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
6	5	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
7		nn0ex 12248	. . . . . . 7 ⊢ ℕ0 ∈ V
8	7	mptex 7108	. . . . . 6 ⊢ (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) ∈ V
9	8	shftval4 14797	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
10	4, 6, 9	sylancr 587	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
11		addcom 11170	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + 𝑘) = (𝑘 + 1))
12	4, 6, 11	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 + 𝑘) = (𝑘 + 1))
13	12	fveq2d 6787	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)))
14		peano2nn0 12282	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
15	14	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
16		id 22	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
17		2fveq3 6788	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))
18	16, 17	oveq12d 7302	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
19		eqid 2739	. . . . . . 7 ⊢ (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))
20		ovex 7317	. . . . . . 7 ⊢ ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) ∈ V
21	18, 19, 20	fvmpt 6884	. . . . . 6 ⊢ ((𝑘 + 1) ∈ ℕ0 → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
22	15, 21	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
23		dvradcnv.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℂ)
24		dvradcnv.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
25	24	pserval2 25579	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ0) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
26	23, 14, 25	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
27	26	fveq2d 6787	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐺‘𝑋)‘(𝑘 + 1))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
28	27	oveq2d 7300	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
29	22, 28	eqtrd 2779	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
30	10, 13, 29	3eqtrd 2783	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
31	15	nn0red 12303	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
32		dvradcnv.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
33		ffvelrn 6968	. . . . . . 7 ⊢ ((𝐴:ℕ0⟶ℂ ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
34	32, 14, 33	syl2an 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
35		expcl 13809	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
36	23, 14, 35	syl2an 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
37	34, 36	mulcld 11004	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
38	37	abscld 15157	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
39	31, 38	remulcld 11014	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℝ)
40	30, 39	eqeltrd 2840	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℝ)
41		oveq1 7291	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
42	41	fveq2d 6787	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑘 + 1)))
43	41, 42	oveq12d 7302	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
44		oveq2 7292	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑋↑𝑛) = (𝑋↑𝑘))
45	43, 44	oveq12d 7302	. . . . 5 ⊢ (𝑛 = 𝑘 → (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
46		dvradcnv.h	. . . . 5 ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
47		ovex 7317	. . . . 5 ⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ V
48	45, 46, 47	fvmpt 6884	. . . 4 ⊢ (𝑘 ∈ ℕ0 → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
49	48	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
50	15	nn0cnd 12304	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℂ)
51	50, 34	mulcld 11004	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ ℂ)
52		expcl 13809	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑋↑𝑘) ∈ ℂ)
53	23, 52	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑋↑𝑘) ∈ ℂ)
54	51, 53	mulcld 11004	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ ℂ)
55	49, 54	eqeltrd 2840	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) ∈ ℂ)
56		dvradcnv.r	. . . . . . . 8 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
57		dvradcnv.l	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝑋) < 𝑅)
58		id 22	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
59		2fveq3 6788	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘𝑘)))
60	58, 59	oveq12d 7302	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
61	60	cbvmptv 5188	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑘 ∈ ℕ0 ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
62	24, 32, 56, 23, 57, 61	radcnvlt1 25586	. . . . . . 7 ⊢ (𝜑 → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))
63	62	simpld 495	. . . . . 6 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ )
64		climdm 15272	. . . . . 6 ⊢ (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
65	63, 64	sylib 217	. . . . 5 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
66		0z 12339	. . . . . 6 ⊢ 0 ∈ ℤ
67		neg1z 12365	. . . . . 6 ⊢ -1 ∈ ℤ
68	8	isershft 15384	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ -1 ∈ ℤ) → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))))
69	66, 67, 68	mp2an 689	. . . . 5 ⊢ (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
70	65, 69	sylib 217	. . . 4 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
71		seqex 13732	. . . . 5 ⊢ seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ V
72		fvex 6796	. . . . 5 ⊢ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ∈ V
73	71, 72	breldm 5820	. . . 4 ⊢ (seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) → seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
74	70, 73	syl 17	. . 3 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
75		eqid 2739	. . . 4 ⊢ (ℤ≥‘(0 + -1)) = (ℤ≥‘(0 + -1))
76		neg1cn 12096	. . . . . . . 8 ⊢ -1 ∈ ℂ
77	76	addid2i 11172	. . . . . . 7 ⊢ (0 + -1) = -1
78		0le1 11507	. . . . . . . 8 ⊢ 0 ≤ 1
79		1re 10984	. . . . . . . . 9 ⊢ 1 ∈ ℝ
80		le0neg2 11493	. . . . . . . . 9 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
81	79, 80	ax-mp 5	. . . . . . . 8 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
82	78, 81	mpbi 229	. . . . . . 7 ⊢ -1 ≤ 0
83	77, 82	eqbrtri 5096	. . . . . 6 ⊢ (0 + -1) ≤ 0
84	77, 67	eqeltri 2836	. . . . . . 7 ⊢ (0 + -1) ∈ ℤ
85	84	eluz1i 12599	. . . . . 6 ⊢ (0 ∈ (ℤ≥‘(0 + -1)) ↔ (0 ∈ ℤ ∧ (0 + -1) ≤ 0))
86	66, 83, 85	mpbir2an 708	. . . . 5 ⊢ 0 ∈ (ℤ≥‘(0 + -1))
87	86	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (ℤ≥‘(0 + -1)))
88		eluzelcn 12603	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → 𝑘 ∈ ℂ)
89	88	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → 𝑘 ∈ ℂ)
90	4, 89, 9	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
91		nn0re 12251	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ)
92	91	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℝ)
93	24, 32, 23	psergf 25580	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ)
94	93	ffvelrnda 6970	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑖) ∈ ℂ)
95	94	abscld 15157	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (abs‘((𝐺‘𝑋)‘𝑖)) ∈ ℝ)
96	92, 95	remulcld 11014	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℝ)
97	96	recnd 11012	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℂ)
98	97	fmpttd 6998	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ0⟶ℂ)
99	4, 88, 11	sylancr 587	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (1 + 𝑘) = (𝑘 + 1))
100		eluzp1p1 12619	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (𝑘 + 1) ∈ (ℤ≥‘((0 + -1) + 1)))
101	77	oveq1i 7294	. . . . . . . . . . 11 ⊢ ((0 + -1) + 1) = (-1 + 1)
102		1pneg1e0 12101	. . . . . . . . . . . 12 ⊢ (1 + -1) = 0
103	4, 76, 102	addcomli 11176	. . . . . . . . . . 11 ⊢ (-1 + 1) = 0
104	101, 103	eqtri 2767	. . . . . . . . . 10 ⊢ ((0 + -1) + 1) = 0
105	104	fveq2i 6786	. . . . . . . . 9 ⊢ (ℤ≥‘((0 + -1) + 1)) = (ℤ≥‘0)
106	1, 105	eqtr4i 2770	. . . . . . . 8 ⊢ ℕ0 = (ℤ≥‘((0 + -1) + 1))
107	100, 106	eleqtrrdi 2851	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (𝑘 + 1) ∈ ℕ0)
108	99, 107	eqeltrd 2840	. . . . . 6 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (1 + 𝑘) ∈ ℕ0)
109		ffvelrn 6968	. . . . . 6 ⊢ (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ0⟶ℂ ∧ (1 + 𝑘) ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
110	98, 108, 109	syl2an 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
111	90, 110	eqeltrd 2840	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℂ)
112	75, 87, 111	iserex 15377	. . 3 ⊢ (𝜑 → (seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ↔ seq0( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ))
113	74, 112	mpbid 231	. 2 ⊢ (𝜑 → seq0( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
114		1red 10985	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0) → 1 ∈ ℝ)
115		neqne 2952	. . . . 5 ⊢ (¬ 𝑋 = 0 → 𝑋 ≠ 0)
116		absrpcl 15009	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ+)
117	23, 115, 116	syl2an 596	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (abs‘𝑋) ∈ ℝ+)
118	117	rprecred 12792	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (1 / (abs‘𝑋)) ∈ ℝ)
119	114, 118	ifclda 4495	. 2 ⊢ (𝜑 → if(𝑋 = 0, 1, (1 / (abs‘𝑋))) ∈ ℝ)
120		oveq1 7291	. . . . 5 ⊢ (1 = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
121	120	breq2d 5087	. . . 4 ⊢ (1 = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → ((abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) ↔ (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))))
122		oveq1 7291	. . . . 5 ⊢ ((1 / (abs‘𝑋)) = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
123	122	breq2d 5087	. . . 4 ⊢ ((1 / (abs‘𝑋)) = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → ((abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) ↔ (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))))
124		elnnuz 12631	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ≥‘1))
125		nnnn0 12249	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
126	124, 125	sylbir 234	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘1) → 𝑘 ∈ ℕ0)
127	15	nn0ge0d 12305	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝑘 + 1))
128	37	absge0d 15165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
129	31, 38, 127, 128	mulge0d 11561	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
130	126, 129	sylan2 593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
131	130	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
132		oveq1 7291	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝑋↑𝑘) = (0↑𝑘))
133		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → 𝑘 ∈ (ℤ≥‘1))
134	133, 124	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → 𝑘 ∈ ℕ)
135	134	0expd 13866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (0↑𝑘) = 0)
136	132, 135	sylan9eqr 2801	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (𝑋↑𝑘) = 0)
137	136	oveq2d 7300	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0))
138	51	mul01d 11183	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
139	126, 138	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
140	139	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
141	137, 140	eqtrd 2779	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = 0)
142	141	abs00bd 15012	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = 0)
143	39	recnd 11012	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℂ)
144	143	mulid2d 11002	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
145	126, 144	sylan2 593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
146	145	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
147	131, 142, 146	3brtr4d 5107	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
148		df-ne 2945	. . . . 5 ⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0)
149	54	abscld 15157	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ∈ ℝ)
150	50, 34, 53	mulassd 11007	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
151	150	fveq2d 6787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
152	34, 53	mulcld 11004	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) ∈ ℂ)
153	50, 152	absmuld 15175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
154	31, 127	absidd 15143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(𝑘 + 1)) = (𝑘 + 1))
155	154	oveq1d 7299	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
156	151, 153, 155	3eqtrd 2783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
157	149, 156	eqled 11087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
158	157	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
159	23	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ ℂ)
160	116	rpreccld 12791	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ+)
161	159, 160	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ+)
162	161	rpcnd 12783	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℂ)
163	50	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℂ)
164	38	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
165	164	recnd 11012	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℂ)
166	162, 163, 165	mul12d 11193	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
167	37	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
168	23	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑋 ∈ ℂ)
169		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0)
170	167, 168, 169	absdivd 15176	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)))
171	34	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
172	36	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
173	171, 172, 168, 169	divassd 11795	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
174	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑘 ∈ ℂ)
175		pncan 11236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
176	174, 4, 175	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) − 1) = 𝑘)
177	176	oveq2d 7300	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = (𝑋↑𝑘))
178	15	nn0zd 12433	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℤ)
179	178	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℤ)
180	168, 169, 179	expm1d 13883	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = ((𝑋↑(𝑘 + 1)) / 𝑋))
181	177, 180	eqtr3d 2781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑𝑘) = ((𝑋↑(𝑘 + 1)) / 𝑋))
182	181	oveq2d 7300	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
183	173, 182	eqtr4d 2782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))
184	183	fveq2d 6787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
185	23	abscld 15157	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘𝑋) ∈ ℝ)
186	185	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ)
187	186	recnd 11012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℂ)
188	159, 116	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ+)
189	188	rpne0d 12786	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ≠ 0)
190	165, 187, 189	divrec2d 11764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)) = ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
191	170, 184, 190	3eqtr3rd 2788	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
192	191	oveq2d 7300	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
193	166, 192	eqtrd 2779	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
194	158, 193	breqtrrd 5103	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
195	126, 194	sylanl2 678	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
196	148, 195	sylan2br 595	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ ¬ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
197	121, 123, 147, 196	ifbothda 4498	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
198	49	fveq2d 6787	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
199	126, 198	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
200	30	oveq2d 7300	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
201	126, 200	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
202	197, 199, 201	3brtr4d 5107	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (abs‘(𝐻‘𝑘)) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)))
203	1, 3, 40, 55, 113, 119, 202	cvgcmpce 15539	1 ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107   ≠ wne 2944  {crab 3069  ifcif 4460   class class class wbr 5075   ↦ cmpt 5158  dom cdm 5590   ∘ ccom 5594  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284  supcsup 9208  ℂcc 10878  ℝcr 10879  0cc0 10880  1c1 10881   + caddc 10883   · cmul 10885  ℝ^*cxr 11017   < clt 11018   ≤ cle 11019   − cmin 11214  -cneg 11215   / cdiv 11641  ℕcn 11982  ℕ₀cn0 12242  ℤcz 12328  ℤ_≥cuz 12591  ℝ⁺crp 12739  seqcseq 13730  ↑cexp 13791   shift cshi 14786  abscabs 14954   ⇝ cli 15202

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-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-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-seq 13731  df-exp 13792  df-hash 14054  df-shft 14787  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-limsup 15189  df-clim 15206  df-rlim 15207  df-sum 15407

This theorem is referenced by:  pserdvlem2  25596  dvradcnv2  41972