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 26595

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 12906	. 2 ⊢ ℕ₀ = (ℤ_≥‘0)
2		1nn0 12526	. . 3 ⊢ 1 ∈ ℕ₀
3	2	a1i 11	. 2 ⊢ (𝜑 → 1 ∈ ℕ₀)
4		ax-1cn 11164	. . . . 5 ⊢ 1 ∈ ℂ
5		nn0cn 12520	. . . . . 6 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℂ)
6	5	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
7		nn0ex 12516	. . . . . . 7 ⊢ ℕ₀ ∈ V
8	7	mptex 7221	. . . . . 6 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) ∈ V
9	8	shftval4 15121	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
10	4, 6, 9	sylancr 598	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
11		addcom 11402	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + 𝑘) = (𝑘 + 1))
12	4, 6, 11	sylancr 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (1 + 𝑘) = (𝑘 + 1))
13	12	fveq2d 6885	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)))
14		peano2nn0 12550	. . . . . . 7 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
15	14	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℕ₀)
16		id 23	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
17		2fveq3 6886	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))
18	16, 17	oveq12d 7430	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
19		eqid 2762	. . . . . . 7 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))
20		ovex 7445	. . . . . . 7 ⊢ ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) ∈ V
21	18, 19, 20	fvmpt 6989	. . . . . 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 26585	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
26	23, 14, 25	syl2an 607	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
27	26	fveq2d 6885	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐺‘𝑋)‘(𝑘 + 1))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
28	27	oveq2d 7428	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
29	22, 28	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
30	10, 13, 29	3eqtrd 2801	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
31	15	nn0red 12572	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℝ)
32		dvradcnv.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
33		ffvelcdm 7076	. . . . . . 7 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
34	32, 14, 33	syl2an 607	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
35		expcl 14122	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
36	23, 14, 35	syl2an 607	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
37	34, 36	mulcld 11235	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
38	37	abscld 15497	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
39	31, 38	remulcld 11245	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℝ)
40	30, 39	eqeltrd 2862	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℝ)
41		oveq1 7419	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
42	41	fveq2d 6885	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑘 + 1)))
43	41, 42	oveq12d 7430	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
44		oveq2 7420	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑋↑𝑛) = (𝑋↑𝑘))
45	43, 44	oveq12d 7430	. . . . 5 ⊢ (𝑛 = 𝑘 → (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
46		dvradcnv.h	. . . . 5 ⊢ 𝐻 = (𝑛 ∈ ℕ₀ ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
47		ovex 7445	. . . . 5 ⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ V
48	45, 46, 47	fvmpt 6989	. . . 4 ⊢ (𝑘 ∈ ℕ₀ → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
49	48	adantl 486	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
50	15	nn0cnd 12573	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℂ)
51	50, 34	mulcld 11235	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ ℂ)
52		expcl 14122	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑋↑𝑘) ∈ ℂ)
53	23, 52	sylan 591	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑋↑𝑘) ∈ ℂ)
54	51, 53	mulcld 11235	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ ℂ)
55	49, 54	eqeltrd 2862	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐻‘𝑘) ∈ ℂ)
56		dvradcnv.r	. . . . . . . 8 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )
57		dvradcnv.l	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝑋) < 𝑅)
58		id 23	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
59		2fveq3 6886	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘𝑘)))
60	58, 59	oveq12d 7430	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
61	60	cbvmptv 5214	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑘 ∈ ℕ₀ ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
62	24, 32, 56, 23, 57, 61	radcnvlt1 26592	. . . . . . 7 ⊢ (𝜑 → (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))
63	62	simpld 499	. . . . . 6 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ )
64		climdm 15612	. . . . . 6 ⊢ (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
65	63, 64	sylib 221	. . . . 5 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
66		0z 12608	. . . . . 6 ⊢ 0 ∈ ℤ
67		neg1z 12636	. . . . . 6 ⊢ -1 ∈ ℤ
68	8	isershft 15722	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ -1 ∈ ℤ) → (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))))
69	66, 67, 68	mp2an 704	. . . . 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 14046	. . . . 5 ⊢ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ V
72		fvex 6894	. . . . 5 ⊢ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ∈ V
73	71, 72	breldm 5897	. . . 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 2762	. . . 4 ⊢ (ℤ_≥‘(0 + -1)) = (ℤ_≥‘(0 + -1))
76		neg1cn 12209	. . . . . . . 8 ⊢ -1 ∈ ℂ
77	76	addlidi 11404	. . . . . . 7 ⊢ (0 + -1) = -1
78		0le1 11743	. . . . . . . 8 ⊢ 0 ≤ 1
79		1re 11214	. . . . . . . . 9 ⊢ 1 ∈ ℝ
80		le0neg2 11729	. . . . . . . . 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 5131	. . . . . 6 ⊢ (0 + -1) ≤ 0
84	77, 67	eqeltri 2858	. . . . . . 7 ⊢ (0 + -1) ∈ ℤ
85	84	eluz1i 12876	. . . . . 6 ⊢ (0 ∈ (ℤ_≥‘(0 + -1)) ↔ (0 ∈ ℤ ∧ (0 + -1) ≤ 0))
86	66, 83, 85	mpbir2an 723	. . . . 5 ⊢ 0 ∈ (ℤ_≥‘(0 + -1))
87	86	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘(0 + -1)))
88		eluzelcn 12880	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → 𝑘 ∈ ℂ)
89	88	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → 𝑘 ∈ ℂ)
90	4, 89, 9	sylancr 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
91		nn0re 12519	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℝ)
92	91	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℝ)
93	24, 32, 23	psergf 26586	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑋):ℕ₀⟶ℂ)
94	93	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((𝐺‘𝑋)‘𝑖) ∈ ℂ)
95	94	abscld 15497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (abs‘((𝐺‘𝑋)‘𝑖)) ∈ ℝ)
96	92, 95	remulcld 11245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℝ)
97	96	recnd 11243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℂ)
98	97	fmpttd 7110	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ₀⟶ℂ)
99	4, 88, 11	sylancr 598	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (1 + 𝑘) = (𝑘 + 1))
100		eluzp1p1 12896	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (𝑘 + 1) ∈ (ℤ_≥‘((0 + -1) + 1)))
101	77	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((0 + -1) + 1) = (-1 + 1)
102		1pneg1e0 12364	. . . . . . . . . . . 12 ⊢ (1 + -1) = 0
103	4, 76, 102	addcomli 11408	. . . . . . . . . . 11 ⊢ (-1 + 1) = 0
104	101, 103	eqtri 2785	. . . . . . . . . 10 ⊢ ((0 + -1) + 1) = 0
105	104	fveq2i 6884	. . . . . . . . 9 ⊢ (ℤ_≥‘((0 + -1) + 1)) = (ℤ_≥‘0)
106	1, 105	eqtr4i 2788	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘((0 + -1) + 1))
107	100, 106	eleqtrrdi 2873	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (𝑘 + 1) ∈ ℕ₀)
108	99, 107	eqeltrd 2862	. . . . . 6 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (1 + 𝑘) ∈ ℕ₀)
109		ffvelcdm 7076	. . . . . 6 ⊢ (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ₀⟶ℂ ∧ (1 + 𝑘) ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
110	98, 108, 109	syl2an 607	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
111	90, 110	eqeltrd 2862	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℂ)
112	75, 87, 111	iserex 15715	. . 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 11215	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0) → 1 ∈ ℝ)
115		neqne 2965	. . . . 5 ⊢ (¬ 𝑋 = 0 → 𝑋 ≠ 0)
116		absrpcl 15346	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ⁺)
117	23, 115, 116	syl2an 607	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (abs‘𝑋) ∈ ℝ⁺)
118	117	rprecred 13077	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (1 / (abs‘𝑋)) ∈ ℝ)
119	114, 118	ifclda 4522	. 2 ⊢ (𝜑 → if(𝑋 = 0, 1, (1 / (abs‘𝑋))) ∈ ℝ)
120		oveq1 7419	. . . . 5 ⊢ (1 = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
121	120	breq2d 5120	. . . 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 7419	. . . . 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 5120	. . . 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 12908	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
125		nnnn0 12517	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
126	124, 125	sylbir 238	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℕ₀)
127	15	nn0ge0d 12574	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ (𝑘 + 1))
128	37	absge0d 15505	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
129	31, 38, 127, 128	mulge0d 11797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
130	126, 129	sylan2 604	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
131	130	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → 0 ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
132		oveq1 7419	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝑋↑𝑘) = (0↑𝑘))
133	124	bilanri 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → 𝑘 ∈ ℕ)
134	133	0expd 14182	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (0↑𝑘) = 0)
135	132, 134	sylan9eqr 2819	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (𝑋↑𝑘) = 0)
136	135	oveq2d 7428	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0))
137	51	mul01d 11415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
138	126, 137	sylan2 604	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
139	138	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0)
140	136, 139	eqtrd 2797	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = 0)
141	140	abs00bd 15349	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = 0)
142	39	recnd 11243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℂ)
143	142	mullidd 11233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
144	126, 143	sylan2 604	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
145	144	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
146	131, 141, 145	3brtr4d 5142	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
147		df-ne 2958	. . . . 5 ⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0)
148	54	abscld 15497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ∈ ℝ)
149	50, 34, 53	mulassd 11238	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
150	149	fveq2d 6885	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
151	34, 53	mulcld 11235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) ∈ ℂ)
152	50, 151	absmuld 15515	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
153	31, 127	absidd 15481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑘 + 1)) = (𝑘 + 1))
154	153	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
155	150, 152, 154	3eqtrd 2801	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
156	148, 155	eqled 11319	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
157	156	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
158	23	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑋 ∈ ℂ)
159	116	rpreccld 13076	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ⁺)
160	158, 159	sylan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ⁺)
161	160	rpcnd 13068	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℂ)
162	50	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℂ)
163	38	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
164	163	recnd 11243	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℂ)
165	161, 162, 164	mul12d 11425	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
166	37	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
167	23	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑋 ∈ ℂ)
168		simpr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0)
169	166, 167, 168	absdivd 15516	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)))
170	34	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
171	36	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
172	170, 171, 167, 168	divassd 12032	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
173	6	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑘 ∈ ℂ)
174		pncan 11469	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
175	173, 4, 174	sylancl 597	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) − 1) = 𝑘)
176	175	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = (𝑋↑𝑘))
177	15	nn0zd 12622	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℤ)
178	177	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℤ)
179	167, 168, 178	expm1d 14199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = ((𝑋↑(𝑘 + 1)) / 𝑋))
180	176, 179	eqtr3d 2799	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑𝑘) = ((𝑋↑(𝑘 + 1)) / 𝑋))
181	180	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
182	172, 181	eqtr4d 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))
183	182	fveq2d 6885	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
184	23	abscld 15497	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘𝑋) ∈ ℝ)
185	184	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ)
186	185	recnd 11243	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℂ)
187	158, 116	sylan 591	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ⁺)
188	187	rpne0d 13071	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ≠ 0)
189	164, 186, 188	divrec2d 12001	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)) = ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
190	169, 183, 189	3eqtr3rd 2806	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
191	190	oveq2d 7428	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
192	165, 191	eqtrd 2797	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
193	157, 192	breqtrrd 5138	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
194	126, 193	sylanl2 693	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
195	147, 194	sylan2br 606	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
196	121, 123, 146, 195	ifbothda 4525	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
197	49	fveq2d 6885	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
198	126, 197	sylan2 604	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
199	30	oveq2d 7428	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
200	126, 199	sylan2 604	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
201	196, 198, 200	3brtr4d 5142	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(𝐻‘𝑘)) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)))
202	1, 3, 40, 55, 113, 119, 201	cvgcmpce 15877	1 ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 {crab 3415 ifcif 4486 class class class wbr 5108 ↦ cmpt 5191 dom cdm 5660 ∘ ccom 5664 ⟶wf 6532 ‘cfv 6536 (class class class)co 7412 supcsup 9398 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 ℝ^*cxr 11248 < clt 11249 ≤ cle 11250 − cmin 11447 -cneg 11448 / cdiv 11877 ℕcn 12239 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12868 ℝ⁺crp 13022 seqcseq 14044 ↑cexp 14104 shift cshi 15110 abscabs 15292 ⇝ cli 15542

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-er 8692 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9400 df-inf 9401 df-oi 9470 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-n0 12511 df-z 12598 df-uz 12869 df-rp 13023 df-ico 13384 df-icc 13385 df-fz 13542 df-fzo 13690 df-fl 13832 df-seq 14045 df-exp 14105 df-hash 14374 df-shft 15111 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-limsup 15529 df-clim 15546 df-rlim 15547 df-sum 15745

This theorem is used by: pserdvlem2 26602 dvradcnv2 45085

W3C validator