Theorem dvradcnv 26390

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 12793	. 2 ⊢ ℕ0 = (ℤ≥‘0)
2		1nn0 12421	. . 3 ⊢ 1 ∈ ℕ0
3	2	a1i 11	. 2 ⊢ (𝜑 → 1 ∈ ℕ0)
4		ax-1cn 11088	. . . . 5 ⊢ 1 ∈ ℂ
5		nn0cn 12415	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
6	5	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
7		nn0ex 12411	. . . . . . 7 ⊢ ℕ0 ∈ V
8	7	mptex 7171	. . . . . 6 ⊢ (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) ∈ V
9	8	shftval4 15004	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
10	4, 6, 9	sylancr 588	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
11		addcom 11323	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + 𝑘) = (𝑘 + 1))
12	4, 6, 11	sylancr 588	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 + 𝑘) = (𝑘 + 1))
13	12	fveq2d 6839	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)))
14		peano2nn0 12445	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
15	14	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
16		id 22	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
17		2fveq3 6840	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))
18	16, 17	oveq12d 7378	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
19		eqid 2737	. . . . . . 7 ⊢ (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))
20		ovex 7393	. . . . . . 7 ⊢ ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) ∈ V
21	18, 19, 20	fvmpt 6942	. . . . . 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 26380	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ0) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
26	23, 14, 25	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
27	26	fveq2d 6839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐺‘𝑋)‘(𝑘 + 1))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
28	27	oveq2d 7376	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
29	22, 28	eqtrd 2772	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
30	10, 13, 29	3eqtrd 2776	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
31	15	nn0red 12467	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
32		dvradcnv.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
33		ffvelcdm 7028	. . . . . . 7 ⊢ ((𝐴:ℕ0⟶ℂ ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
34	32, 14, 33	syl2an 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
35		expcl 14006	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
36	23, 14, 35	syl2an 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
37	34, 36	mulcld 11156	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
38	37	abscld 15366	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
39	31, 38	remulcld 11166	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℝ)
40	30, 39	eqeltrd 2837	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℝ)
41		oveq1 7367	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
42	41	fveq2d 6839	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑘 + 1)))
43	41, 42	oveq12d 7378	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
44		oveq2 7368	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑋↑𝑛) = (𝑋↑𝑘))
45	43, 44	oveq12d 7378	. . . . 5 ⊢ (𝑛 = 𝑘 → (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
46		dvradcnv.h	. . . . 5 ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
47		ovex 7393	. . . . 5 ⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ V
48	45, 46, 47	fvmpt 6942	. . . 4 ⊢ (𝑘 ∈ ℕ0 → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
49	48	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
50	15	nn0cnd 12468	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℂ)
51	50, 34	mulcld 11156	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ ℂ)
52		expcl 14006	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑋↑𝑘) ∈ ℂ)
53	23, 52	sylan 581	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑋↑𝑘) ∈ ℂ)
54	51, 53	mulcld 11156	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ ℂ)
55	49, 54	eqeltrd 2837	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) ∈ ℂ)
56		dvradcnv.r	. . . . . . . 8 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
57		dvradcnv.l	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝑋) < 𝑅)
58		id 22	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
59		2fveq3 6840	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘𝑘)))
60	58, 59	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
61	60	cbvmptv 5203	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑘 ∈ ℕ0 ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
62	24, 32, 56, 23, 57, 61	radcnvlt1 26387	. . . . . . 7 ⊢ (𝜑 → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))
63	62	simpld 494	. . . . . 6 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ )
64		climdm 15481	. . . . . 6 ⊢ (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
65	63, 64	sylib 218	. . . . 5 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
66		0z 12503	. . . . . 6 ⊢ 0 ∈ ℤ
67		neg1z 12531	. . . . . 6 ⊢ -1 ∈ ℤ
68	8	isershft 15591	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ -1 ∈ ℤ) → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))))
69	66, 67, 68	mp2an 693	. . . . 5 ⊢ (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
70	65, 69	sylib 218	. . . 4 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
71		seqex 13930	. . . . 5 ⊢ seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ V
72		fvex 6848	. . . . 5 ⊢ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ∈ V
73	71, 72	breldm 5858	. . . 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 2737	. . . 4 ⊢ (ℤ≥‘(0 + -1)) = (ℤ≥‘(0 + -1))
76		neg1cn 12134	. . . . . . . 8 ⊢ -1 ∈ ℂ
77	76	addlidi 11325	. . . . . . 7 ⊢ (0 + -1) = -1
78		0le1 11664	. . . . . . . 8 ⊢ 0 ≤ 1
79		1re 11136	. . . . . . . . 9 ⊢ 1 ∈ ℝ
80		le0neg2 11650	. . . . . . . . 9 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
81	79, 80	ax-mp 5	. . . . . . . 8 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
82	78, 81	mpbi 230	. . . . . . 7 ⊢ -1 ≤ 0
83	77, 82	eqbrtri 5120	. . . . . 6 ⊢ (0 + -1) ≤ 0
84	77, 67	eqeltri 2833	. . . . . . 7 ⊢ (0 + -1) ∈ ℤ
85	84	eluz1i 12763	. . . . . 6 ⊢ (0 ∈ (ℤ≥‘(0 + -1)) ↔ (0 ∈ ℤ ∧ (0 + -1) ≤ 0))
86	66, 83, 85	mpbir2an 712	. . . . 5 ⊢ 0 ∈ (ℤ≥‘(0 + -1))
87	86	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (ℤ≥‘(0 + -1)))
88		eluzelcn 12767	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → 𝑘 ∈ ℂ)
89	88	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → 𝑘 ∈ ℂ)
90	4, 89, 9	sylancr 588	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
91		nn0re 12414	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ)
92	91	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℝ)
93	24, 32, 23	psergf 26381	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ)
94	93	ffvelcdmda 7031	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑖) ∈ ℂ)
95	94	abscld 15366	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (abs‘((𝐺‘𝑋)‘𝑖)) ∈ ℝ)
96	92, 95	remulcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℝ)
97	96	recnd 11164	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℂ)
98	97	fmpttd 7062	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ0⟶ℂ)
99	4, 88, 11	sylancr 588	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (1 + 𝑘) = (𝑘 + 1))
100		eluzp1p1 12783	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (𝑘 + 1) ∈ (ℤ≥‘((0 + -1) + 1)))
101	77	oveq1i 7370	. . . . . . . . . . 11 ⊢ ((0 + -1) + 1) = (-1 + 1)
102		1pneg1e0 12263	. . . . . . . . . . . 12 ⊢ (1 + -1) = 0
103	4, 76, 102	addcomli 11329	. . . . . . . . . . 11 ⊢ (-1 + 1) = 0
104	101, 103	eqtri 2760	. . . . . . . . . 10 ⊢ ((0 + -1) + 1) = 0
105	104	fveq2i 6838	. . . . . . . . 9 ⊢ (ℤ≥‘((0 + -1) + 1)) = (ℤ≥‘0)
106	1, 105	eqtr4i 2763	. . . . . . . 8 ⊢ ℕ0 = (ℤ≥‘((0 + -1) + 1))
107	100, 106	eleqtrrdi 2848	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (𝑘 + 1) ∈ ℕ0)
108	99, 107	eqeltrd 2837	. . . . . 6 ⊢ (𝑘 ∈ (ℤ≥‘(0 + -1)) → (1 + 𝑘) ∈ ℕ0)
109		ffvelcdm 7028	. . . . . 6 ⊢ (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ0⟶ℂ ∧ (1 + 𝑘) ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
110	98, 108, 109	syl2an 597	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
111	90, 110	eqeltrd 2837	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 + -1))) → (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℂ)
112	75, 87, 111	iserex 15584	. . 3 ⊢ (𝜑 → (seq(0 + -1)( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ↔ seq0( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ))
113	74, 112	mpbid 232	. 2 ⊢ (𝜑 → seq0( + , ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
114		1red 11137	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0) → 1 ∈ ℝ)
115		neqne 2941	. . . . 5 ⊢ (¬ 𝑋 = 0 → 𝑋 ≠ 0)
116		absrpcl 15215	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ+)
117	23, 115, 116	syl2an 597	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (abs‘𝑋) ∈ ℝ+)
118	117	rprecred 12964	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (1 / (abs‘𝑋)) ∈ ℝ)
119	114, 118	ifclda 4516	. 2 ⊢ (𝜑 → if(𝑋 = 0, 1, (1 / (abs‘𝑋))) ∈ ℝ)
120		oveq1 7367	. . . . 5 ⊢ (1 = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
121	120	breq2d 5111	. . . 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 7367	. . . . 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 5111	. . . 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 12795	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ≥‘1))
125		nnnn0 12412	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
126	124, 125	sylbir 235	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ≥‘1) → 𝑘 ∈ ℕ0)
127	15	nn0ge0d 12469	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝑘 + 1))
128	37	absge0d 15374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
129	31, 38, 127, 128	mulge0d 11718	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
130	126, 129	sylan2 594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
131	130	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
132		oveq1 7367	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝑋↑𝑘) = (0↑𝑘))
133		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → 𝑘 ∈ (ℤ≥‘1))
134	133, 124	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → 𝑘 ∈ ℕ)
135	134	0expd 14066	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (0↑𝑘) = 0)
136	132, 135	sylan9eqr 2794	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (𝑋↑𝑘) = 0)
137	136	oveq2d 7376	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0))
138	51	mul01d 11336	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
139	126, 138	sylan2 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
140	139	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
141	137, 140	eqtrd 2772	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = 0)
142	141	abs00bd 15218	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = 0)
143	39	recnd 11164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℂ)
144	143	mullidd 11154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
145	126, 144	sylan2 594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
146	145	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
147	131, 142, 146	3brtr4d 5131	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
148		df-ne 2934	. . . . 5 ⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0)
149	54	abscld 15366	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ∈ ℝ)
150	50, 34, 53	mulassd 11159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
151	150	fveq2d 6839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
152	34, 53	mulcld 11156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) ∈ ℂ)
153	50, 152	absmuld 15384	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
154	31, 127	absidd 15350	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(𝑘 + 1)) = (𝑘 + 1))
155	154	oveq1d 7375	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
156	151, 153, 155	3eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
157	149, 156	eqled 11240	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
158	157	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
159	23	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ ℂ)
160	116	rpreccld 12963	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ+)
161	159, 160	sylan 581	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ+)
162	161	rpcnd 12955	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℂ)
163	50	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℂ)
164	38	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
165	164	recnd 11164	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℂ)
166	162, 163, 165	mul12d 11346	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
167	37	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
168	23	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑋 ∈ ℂ)
169		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0)
170	167, 168, 169	absdivd 15385	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)))
171	34	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
172	36	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
173	171, 172, 168, 169	divassd 11956	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
174	6	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑘 ∈ ℂ)
175		pncan 11390	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
176	174, 4, 175	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) − 1) = 𝑘)
177	176	oveq2d 7376	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = (𝑋↑𝑘))
178	15	nn0zd 12517	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℤ)
179	178	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℤ)
180	168, 169, 179	expm1d 14083	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = ((𝑋↑(𝑘 + 1)) / 𝑋))
181	177, 180	eqtr3d 2774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑𝑘) = ((𝑋↑(𝑘 + 1)) / 𝑋))
182	181	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
183	173, 182	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))
184	183	fveq2d 6839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
185	23	abscld 15366	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘𝑋) ∈ ℝ)
186	185	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ)
187	186	recnd 11164	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℂ)
188	159, 116	sylan 581	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ+)
189	188	rpne0d 12958	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ≠ 0)
190	165, 187, 189	divrec2d 11925	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)) = ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
191	170, 184, 190	3eqtr3rd 2781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
192	191	oveq2d 7376	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
193	166, 192	eqtrd 2772	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
194	158, 193	breqtrrd 5127	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
195	126, 194	sylanl2 682	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
196	148, 195	sylan2br 596	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) ∧ ¬ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
197	121, 123, 147, 196	ifbothda 4519	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
198	49	fveq2d 6839	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
199	126, 198	sylan2 594	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
200	30	oveq2d 7376	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
201	126, 200	sylan2 594	. . 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 5131	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (abs‘(𝐻‘𝑘)) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)))
203	1, 3, 40, 55, 113, 119, 202	cvgcmpce 15745	1 ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  {crab 3400  ifcif 4480   class class class wbr 5099   ↦ cmpt 5180  dom cdm 5625   ∘ ccom 5629  ⟶wf 6489  ‘cfv 6493  (class class class)co 7360  supcsup 9347  ℂcc 11028  ℝcr 11029  0cc0 11030  1c1 11031   + caddc 11033   · cmul 11035  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171   − cmin 11368  -cneg 11369   / cdiv 11798  ℕcn 12149  ℕ₀cn0 12405  ℤcz 12492  ℤ_≥cuz 12755  ℝ⁺crp 12909  seqcseq 13928  ↑cexp 13988   shift cshi 14993  abscabs 15161   ⇝ cli 15411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-inf2 9554  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107  ax-pre-sup 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-pm 8770  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-sup 9349  df-inf 9350  df-oi 9419  df-card 9855  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12150  df-2 12212  df-3 12213  df-n0 12406  df-z 12493  df-uz 12756  df-rp 12910  df-ico 13271  df-icc 13272  df-fz 13428  df-fzo 13575  df-fl 13716  df-seq 13929  df-exp 13989  df-hash 14258  df-shft 14994  df-cj 15026  df-re 15027  df-im 15028  df-sqrt 15162  df-abs 15163  df-limsup 15398  df-clim 15415  df-rlim 15416  df-sum 15614

This theorem is referenced by:  pserdvlem2  26398  dvradcnv2  44655