dvradcnv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvradcnv		Structured version Visualization version GIF version

Theorem dvradcnv 26697

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	⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
dvradcnv.r	⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )
dvradcnv.h	⊢ 𝐻 = (𝑛 ∈ ℕ₀ ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
dvradcnv.a	⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
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 12958	. 2 ⊢ ℕ₀ = (ℤ_≥‘0)
2		1nn0 12577	. . 3 ⊢ 1 ∈ ℕ₀
3	2	a1i 11	. 2 ⊢ (𝜑 → 1 ∈ ℕ₀)
4		ax-1cn 11215	. . . . 5 ⊢ 1 ∈ ℂ
5		nn0cn 12571	. . . . . 6 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℂ)
6	5	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
7		nn0ex 12567	. . . . . . 7 ⊢ ℕ₀ ∈ V
8	7	mptex 7218	. . . . . 6 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) ∈ V
9	8	shftval4 15183	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
10	4, 6, 9	sylancr 599	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
11		addcom 11453	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + 𝑘) = (𝑘 + 1))
12	4, 6, 11	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (1 + 𝑘) = (𝑘 + 1))
13	12	fveq2d 6878	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)))
14		peano2nn0 12601	. . . . . . 7 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
15	14	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℕ₀)
16		id 23	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
17		2fveq3 6879	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))
18	16, 17	oveq12d 7427	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
19		eqid 2760	. . . . . . 7 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))
20		ovex 7442	. . . . . . 7 ⊢ ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) ∈ V
21	18, 19, 20	fvmpt 6982	. . . . . 6 ⊢ ((𝑘 + 1) ∈ ℕ₀ → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
22	15, 21	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
23		dvradcnv.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℂ)
24		dvradcnv.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
25	24	pserval2 26687	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
26	23, 14, 25	syl2an 608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
27	26	fveq2d 6878	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐺‘𝑋)‘(𝑘 + 1))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
28	27	oveq2d 7425	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
29	22, 28	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
30	10, 13, 29	3eqtrd 2799	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
31	15	nn0red 12623	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℝ)
32		dvradcnv.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
33		ffvelcdm 7070	. . . . . . 7 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
34	32, 14, 33	syl2an 608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
35		expcl 14176	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
36	23, 14, 35	syl2an 608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
37	34, 36	mulcld 11286	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
38	37	abscld 15559	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
39	31, 38	remulcld 11296	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℝ)
40	30, 39	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℝ)
41		oveq1 7416	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
42	41	fveq2d 6878	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑘 + 1)))
43	41, 42	oveq12d 7427	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
44		oveq2 7417	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑋↑𝑛) = (𝑋↑𝑘))
45	43, 44	oveq12d 7427	. . . . 5 ⊢ (𝑛 = 𝑘 → (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
46		dvradcnv.h	. . . . 5 ⊢ 𝐻 = (𝑛 ∈ ℕ₀ ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
47		ovex 7442	. . . . 5 ⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ V
48	45, 46, 47	fvmpt 6982	. . . 4 ⊢ (𝑘 ∈ ℕ₀ → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
49	48	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
50	15	nn0cnd 12624	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℂ)
51	50, 34	mulcld 11286	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ ℂ)
52		expcl 14176	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑋↑𝑘) ∈ ℂ)
53	23, 52	sylan 592	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑋↑𝑘) ∈ ℂ)
54	51, 53	mulcld 11286	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ ℂ)
55	49, 54	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐻‘𝑘) ∈ ℂ)
56		dvradcnv.r	. . . . . . . 8 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )
57		dvradcnv.l	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝑋) < 𝑅)
58		id 23	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
59		2fveq3 6879	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘𝑘)))
60	58, 59	oveq12d 7427	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
61	60	cbvmptv 5209	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑘 ∈ ℕ₀ ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
62	24, 32, 56, 23, 57, 61	radcnvlt1 26694	. . . . . . 7 ⊢ (𝜑 → (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))
63	62	simpld 500	. . . . . 6 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ )
64		climdm 15674	. . . . . 6 ⊢ (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
65	63, 64	sylib 221	. . . . 5 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
66		0z 12659	. . . . . 6 ⊢ 0 ∈ ℤ
67		neg1z 12687	. . . . . 6 ⊢ -1 ∈ ℤ
68	8	isershft 15784	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ -1 ∈ ℤ) → (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))))
69	66, 67, 68	mp2an 705	. . . . 5 ⊢ (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
70	65, 69	sylib 221	. . . 4 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
71		seqex 14100	. . . . 5 ⊢ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ V
72		fvex 6887	. . . . 5 ⊢ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ∈ V
73	71, 72	breldm 5887	. . . 4 ⊢ (seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) → seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
74	70, 73	syl 18	. . 3 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
75		eqid 2760	. . . 4 ⊢ (ℤ_≥‘(0 + -1)) = (ℤ_≥‘(0 + -1))
76		neg1cn 12260	. . . . . . . 8 ⊢ -1 ∈ ℂ
77	76	addlidi 11455	. . . . . . 7 ⊢ (0 + -1) = -1
78		0le1 11794	. . . . . . . 8 ⊢ 0 ≤ 1
79		1re 11265	. . . . . . . . 9 ⊢ 1 ∈ ℝ
80		le0neg2 11780	. . . . . . . . 9 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
81	79, 80	ax-mp 5	. . . . . . . 8 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
82	78, 81	mpbi 233	. . . . . . 7 ⊢ -1 ≤ 0
83	77, 82	eqbrtri 5126	. . . . . 6 ⊢ (0 + -1) ≤ 0
84	77, 67	eqeltri 2856	. . . . . . 7 ⊢ (0 + -1) ∈ ℤ
85	84	eluz1i 12928	. . . . . 6 ⊢ (0 ∈ (ℤ_≥‘(0 + -1)) ↔ (0 ∈ ℤ ∧ (0 + -1) ≤ 0))
86	66, 83, 85	mpbir2an 724	. . . . 5 ⊢ 0 ∈ (ℤ_≥‘(0 + -1))
87	86	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘(0 + -1)))
88		eluzelcn 12932	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → 𝑘 ∈ ℂ)
89	88	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → 𝑘 ∈ ℂ)
90	4, 89, 9	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
91		nn0re 12570	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℝ)
92	91	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℝ)
93	24, 32, 23	psergf 26688	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑋):ℕ₀⟶ℂ)
94	93	ffvelcdmda 7073	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((𝐺‘𝑋)‘𝑖) ∈ ℂ)
95	94	abscld 15559	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (abs‘((𝐺‘𝑋)‘𝑖)) ∈ ℝ)
96	92, 95	remulcld 11296	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℝ)
97	96	recnd 11294	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℂ)
98	97	fmpttd 7104	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ₀⟶ℂ)
99	4, 88, 11	sylancr 599	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (1 + 𝑘) = (𝑘 + 1))
100		eluzp1p1 12948	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (𝑘 + 1) ∈ (ℤ_≥‘((0 + -1) + 1)))
101	77	oveq1i 7419	. . . . . . . . . . 11 ⊢ ((0 + -1) + 1) = (-1 + 1)
102		1pneg1e0 12415	. . . . . . . . . . . 12 ⊢ (1 + -1) = 0
103	4, 76, 102	addcomli 11459	. . . . . . . . . . 11 ⊢ (-1 + 1) = 0
104	101, 103	eqtri 2783	. . . . . . . . . 10 ⊢ ((0 + -1) + 1) = 0
105	104	fveq2i 6877	. . . . . . . . 9 ⊢ (ℤ_≥‘((0 + -1) + 1)) = (ℤ_≥‘0)
106	1, 105	eqtr4i 2786	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘((0 + -1) + 1))
107	100, 106	eleqtrrdi 2871	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (𝑘 + 1) ∈ ℕ₀)
108	99, 107	eqeltrd 2860	. . . . . 6 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (1 + 𝑘) ∈ ℕ₀)
109		ffvelcdm 7070	. . . . . 6 ⊢ (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ₀⟶ℂ ∧ (1 + 𝑘) ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
110	98, 108, 109	syl2an 608	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
111	90, 110	eqeltrd 2860	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℂ)
112	75, 87, 111	iserex 15777	. . 3 ⊢ (𝜑 → (seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ↔ seq0( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ))
113	74, 112	mpbid 235	. 2 ⊢ (𝜑 → seq0( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
114		1red 11266	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0) → 1 ∈ ℝ)
115		neqne 2963	. . . . 5 ⊢ (¬ 𝑋 = 0 → 𝑋 ≠ 0)
116		absrpcl 15408	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ⁺)
117	23, 115, 116	syl2an 608	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (abs‘𝑋) ∈ ℝ⁺)
118	117	rprecred 13130	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (1 / (abs‘𝑋)) ∈ ℝ)
119	114, 118	ifclda 4518	. 2 ⊢ (𝜑 → if(𝑋 = 0, 1, (1 / (abs‘𝑋))) ∈ ℝ)
120		oveq1 7416	. . . . 5 ⊢ (1 = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
121	120	breq2d 5115	. . . 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 7416	. . . . 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 5115	. . . 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 12960	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
125		nnnn0 12568	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
126	124, 125	sylbir 238	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℕ₀)
127	15	nn0ge0d 12625	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ (𝑘 + 1))
128	37	absge0d 15567	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
129	31, 38, 127, 128	mulge0d 11848	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
130	126, 129	sylan2 605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
131	130	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
132		oveq1 7416	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝑋↑𝑘) = (0↑𝑘))
133	124	bilanri 512	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → 𝑘 ∈ ℕ)
134	133	0expd 14236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (0↑𝑘) = 0)
135	132, 134	sylan9eqr 2817	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (𝑋↑𝑘) = 0)
136	135	oveq2d 7425	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0))
137	51	mul01d 11466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
138	126, 137	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
139	138	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
140	136, 139	eqtrd 2795	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = 0)
141	140	abs00bd 15411	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = 0)
142	39	recnd 11294	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℂ)
143	142	mullidd 11284	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
144	126, 143	sylan2 605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
145	144	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
146	131, 141, 145	3brtr4d 5137	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
147		df-ne 2956	. . . . 5 ⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0)
148	54	abscld 15559	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ∈ ℝ)
149	50, 34, 53	mulassd 11289	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
150	149	fveq2d 6878	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
151	34, 53	mulcld 11286	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) ∈ ℂ)
152	50, 151	absmuld 15577	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
153	31, 127	absidd 15543	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑘 + 1)) = (𝑘 + 1))
154	153	oveq1d 7424	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
155	150, 152, 154	3eqtrd 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
156	148, 155	eqled 11370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
157	156	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
158	23	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑋 ∈ ℂ)
159	116	rpreccld 13129	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ⁺)
160	158, 159	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ⁺)
161	160	rpcnd 13121	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℂ)
162	50	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℂ)
163	38	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
164	163	recnd 11294	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℂ)
165	161, 162, 164	mul12d 11476	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
166	37	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
167	23	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑋 ∈ ℂ)
168		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0)
169	166, 167, 168	absdivd 15578	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)))
170	34	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
171	36	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
172	170, 171, 167, 168	divassd 12083	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
173	6	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑘 ∈ ℂ)
174		pncan 11520	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
175	173, 4, 174	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) − 1) = 𝑘)
176	175	oveq2d 7425	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = (𝑋↑𝑘))
177	15	nn0zd 12673	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℤ)
178	177	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℤ)
179	167, 168, 178	expm1d 14253	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = ((𝑋↑(𝑘 + 1)) / 𝑋))
180	176, 179	eqtr3d 2797	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑𝑘) = ((𝑋↑(𝑘 + 1)) / 𝑋))
181	180	oveq2d 7425	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
182	172, 181	eqtr4d 2798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))
183	182	fveq2d 6878	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
184	23	abscld 15559	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘𝑋) ∈ ℝ)
185	184	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ)
186	185	recnd 11294	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℂ)
187	158, 116	sylan 592	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ⁺)
188	187	rpne0d 13124	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ≠ 0)
189	164, 186, 188	divrec2d 12052	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)) = ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
190	169, 183, 189	3eqtr3rd 2804	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
191	190	oveq2d 7425	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
192	165, 191	eqtrd 2795	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
193	157, 192	breqtrrd 5133	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
194	126, 193	sylanl2 694	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
195	147, 194	sylan2br 607	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
196	121, 123, 146, 195	ifbothda 4521	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
197	49	fveq2d 6878	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
198	126, 197	sylan2 605	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
199	30	oveq2d 7425	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
200	126, 199	sylan2 605	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
201	196, 198, 200	3brtr4d 5137	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(𝐻‘𝑘)) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)))
202	1, 3, 40, 55, 113, 119, 201	cvgcmpce 15938	1 ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 {crab 3412 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5648 ∘ ccom 5652 ⟶wf 6524 ‘cfv 6528 (class class class)co 7409 supcsup 9410 ℂcc 11155 ℝcr 11156 0cc0 11157 1c1 11158 + caddc 11160 · cmul 11162 ℝ^*cxr 11299 < clt 11300 ≤ cle 11301 − cmin 11498 -cneg 11499 / cdiv 11928 ℕcn 12290 ℕ₀cn0 12561 ℤcz 12648 ℤ_≥cuz 12920 ℝ⁺crp 13075 seqcseq 14098 ↑cexp 14158 shift cshi 15172 abscabs 15354 ⇝ cli 15604

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7735 ax-inf2 9620 ax-cnex 11213 ax-resscn 11214 ax-1cn 11215 ax-icn 11216 ax-addcl 11217 ax-addrcl 11218 ax-mulcl 11219 ax-mulrcl 11220 ax-mulcom 11221 ax-addass 11222 ax-mulass 11223 ax-distr 11224 ax-i2m1 11225 ax-1ne0 11226 ax-1rid 11227 ax-rnegex 11228 ax-rrecex 11229 ax-cnre 11230 ax-pre-lttri 11231 ax-pre-lttrn 11232 ax-pre-ltadd 11233 ax-pre-mulgt0 11234 ax-pre-sup 11235

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-se 5602 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6294 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-isom 6537 df-riota 7366 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8455 df-er 8696 df-pm 8829 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-inf 9413 df-oi 9482 df-card 9977 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-sub 11500 df-neg 11501 df-div 11929 df-nn 12291 df-2 12360 df-3 12361 df-n0 12562 df-z 12649 df-uz 12921 df-rp 13076 df-ico 13437 df-icc 13438 df-fz 13595 df-fzo 13743 df-fl 13886 df-seq 14099 df-exp 14159 df-hash 14428 df-shft 15173 df-cj 15219 df-re 15220 df-im 15221 df-sqrt 15355 df-abs 15356 df-limsup 15591 df-clim 15608 df-rlim 15609 df-sum 15807

This theorem is used by: pserdvlem2 26704 dvradcnv2 45269

W3C validator