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 25817

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 12814	. 2 ⊢ ℕ₀ = (ℤ_≥‘0)
2		1nn0 12438	. . 3 ⊢ 1 ∈ ℕ₀
3	2	a1i 11	. 2 ⊢ (𝜑 → 1 ∈ ℕ₀)
4		ax-1cn 11118	. . . . 5 ⊢ 1 ∈ ℂ
5		nn0cn 12432	. . . . . 6 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℂ)
6	5	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
7		nn0ex 12428	. . . . . . 7 ⊢ ℕ₀ ∈ V
8	7	mptex 7178	. . . . . 6 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) ∈ V
9	8	shftval4 14974	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
10	4, 6, 9	sylancr 587	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
11		addcom 11350	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (1 + 𝑘) = (𝑘 + 1))
12	4, 6, 11	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (1 + 𝑘) = (𝑘 + 1))
13	12	fveq2d 6851	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)))
14		peano2nn0 12462	. . . . . . 7 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
15	14	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℕ₀)
16		id 22	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
17		2fveq3 6852	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))
18	16, 17	oveq12d 7380	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
19		eqid 2731	. . . . . . 7 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))
20		ovex 7395	. . . . . . 7 ⊢ ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) ∈ V
21	18, 19, 20	fvmpt 6953	. . . . . 6 ⊢ ((𝑘 + 1) ∈ ℕ₀ → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
22	15, 21	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))))
23		dvradcnv.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℂ)
24		dvradcnv.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
25	24	pserval2 25807	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
26	23, 14, 25	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))
27	26	fveq2d 6851	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐺‘𝑋)‘(𝑘 + 1))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
28	27	oveq2d 7378	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
29	22, 28	eqtrd 2771	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
30	10, 13, 29	3eqtrd 2775	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
31	15	nn0red 12483	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℝ)
32		dvradcnv.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
33		ffvelcdm 7037	. . . . . . 7 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
34	32, 14, 33	syl2an 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
35		expcl 13995	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ₀) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
36	23, 14, 35	syl2an 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
37	34, 36	mulcld 11184	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
38	37	abscld 15333	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
39	31, 38	remulcld 11194	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℝ)
40	30, 39	eqeltrd 2832	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℝ)
41		oveq1 7369	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
42	41	fveq2d 6851	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑘 + 1)))
43	41, 42	oveq12d 7380	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
44		oveq2 7370	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑋↑𝑛) = (𝑋↑𝑘))
45	43, 44	oveq12d 7380	. . . . 5 ⊢ (𝑛 = 𝑘 → (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
46		dvradcnv.h	. . . . 5 ⊢ 𝐻 = (𝑛 ∈ ℕ₀ ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))
47		ovex 7395	. . . . 5 ⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ V
48	45, 46, 47	fvmpt 6953	. . . 4 ⊢ (𝑘 ∈ ℕ₀ → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
49	48	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))
50	15	nn0cnd 12484	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℂ)
51	50, 34	mulcld 11184	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ ℂ)
52		expcl 13995	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑋↑𝑘) ∈ ℂ)
53	23, 52	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑋↑𝑘) ∈ ℂ)
54	51, 53	mulcld 11184	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ ℂ)
55	49, 54	eqeltrd 2832	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐻‘𝑘) ∈ ℂ)
56		dvradcnv.r	. . . . . . . 8 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )
57		dvradcnv.l	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝑋) < 𝑅)
58		id 22	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
59		2fveq3 6852	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘𝑘)))
60	58, 59	oveq12d 7380	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
61	60	cbvmptv 5223	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑘 ∈ ℕ₀ ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))
62	24, 32, 56, 23, 57, 61	radcnvlt1 25814	. . . . . . 7 ⊢ (𝜑 → (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))
63	62	simpld 495	. . . . . 6 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ )
64		climdm 15448	. . . . . 6 ⊢ (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
65	63, 64	sylib 217	. . . . 5 ⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
66		0z 12519	. . . . . 6 ⊢ 0 ∈ ℤ
67		neg1z 12548	. . . . . 6 ⊢ -1 ∈ ℤ
68	8	isershft 15560	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ -1 ∈ ℤ) → (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))))
69	66, 67, 68	mp2an 690	. . . . 5 ⊢ (seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
70	65, 69	sylib 217	. . . 4 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))
71		seqex 13918	. . . . 5 ⊢ seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ V
72		fvex 6860	. . . . 5 ⊢ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ∈ V
73	71, 72	breldm 5869	. . . 4 ⊢ (seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝ ‘seq0( + , (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) → seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
74	70, 73	syl 17	. . 3 ⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
75		eqid 2731	. . . 4 ⊢ (ℤ_≥‘(0 + -1)) = (ℤ_≥‘(0 + -1))
76		neg1cn 12276	. . . . . . . 8 ⊢ -1 ∈ ℂ
77	76	addlidi 11352	. . . . . . 7 ⊢ (0 + -1) = -1
78		0le1 11687	. . . . . . . 8 ⊢ 0 ≤ 1
79		1re 11164	. . . . . . . . 9 ⊢ 1 ∈ ℝ
80		le0neg2 11673	. . . . . . . . 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 5131	. . . . . 6 ⊢ (0 + -1) ≤ 0
84	77, 67	eqeltri 2828	. . . . . . 7 ⊢ (0 + -1) ∈ ℤ
85	84	eluz1i 12780	. . . . . 6 ⊢ (0 ∈ (ℤ_≥‘(0 + -1)) ↔ (0 ∈ ℤ ∧ (0 + -1) ≤ 0))
86	66, 83, 85	mpbir2an 709	. . . . 5 ⊢ 0 ∈ (ℤ_≥‘(0 + -1))
87	86	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘(0 + -1)))
88		eluzelcn 12784	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → 𝑘 ∈ ℂ)
89	88	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → 𝑘 ∈ ℂ)
90	4, 89, 9	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)))
91		nn0re 12431	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℝ)
92	91	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℝ)
93	24, 32, 23	psergf 25808	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑋):ℕ₀⟶ℂ)
94	93	ffvelcdmda 7040	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((𝐺‘𝑋)‘𝑖) ∈ ℂ)
95	94	abscld 15333	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (abs‘((𝐺‘𝑋)‘𝑖)) ∈ ℝ)
96	92, 95	remulcld 11194	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℝ)
97	96	recnd 11192	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℂ)
98	97	fmpttd 7068	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ₀⟶ℂ)
99	4, 88, 11	sylancr 587	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (1 + 𝑘) = (𝑘 + 1))
100		eluzp1p1 12800	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (𝑘 + 1) ∈ (ℤ_≥‘((0 + -1) + 1)))
101	77	oveq1i 7372	. . . . . . . . . . 11 ⊢ ((0 + -1) + 1) = (-1 + 1)
102		1pneg1e0 12281	. . . . . . . . . . . 12 ⊢ (1 + -1) = 0
103	4, 76, 102	addcomli 11356	. . . . . . . . . . 11 ⊢ (-1 + 1) = 0
104	101, 103	eqtri 2759	. . . . . . . . . 10 ⊢ ((0 + -1) + 1) = 0
105	104	fveq2i 6850	. . . . . . . . 9 ⊢ (ℤ_≥‘((0 + -1) + 1)) = (ℤ_≥‘0)
106	1, 105	eqtr4i 2762	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘((0 + -1) + 1))
107	100, 106	eleqtrrdi 2843	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (𝑘 + 1) ∈ ℕ₀)
108	99, 107	eqeltrd 2832	. . . . . 6 ⊢ (𝑘 ∈ (ℤ_≥‘(0 + -1)) → (1 + 𝑘) ∈ ℕ₀)
109		ffvelcdm 7037	. . . . . 6 ⊢ (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ₀⟶ℂ ∧ (1 + 𝑘) ∈ ℕ₀) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
110	98, 108, 109	syl2an 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ)
111	90, 110	eqeltrd 2832	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(0 + -1))) → (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℂ)
112	75, 87, 111	iserex 15553	. . 3 ⊢ (𝜑 → (seq(0 + -1)( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ↔ seq0( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ))
113	74, 112	mpbid 231	. 2 ⊢ (𝜑 → seq0( + , ((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ )
114		1red 11165	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0) → 1 ∈ ℝ)
115		neqne 2947	. . . . 5 ⊢ (¬ 𝑋 = 0 → 𝑋 ≠ 0)
116		absrpcl 15185	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ⁺)
117	23, 115, 116	syl2an 596	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (abs‘𝑋) ∈ ℝ⁺)
118	117	rprecred 12977	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (1 / (abs‘𝑋)) ∈ ℝ)
119	114, 118	ifclda 4526	. 2 ⊢ (𝜑 → if(𝑋 = 0, 1, (1 / (abs‘𝑋))) ∈ ℝ)
120		oveq1 7369	. . . . 5 ⊢ (1 = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
121	120	breq2d 5122	. . . 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 7369	. . . . 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 5122	. . . 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 12816	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
125		nnnn0 12429	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
126	124, 125	sylbir 234	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℕ₀)
127	15	nn0ge0d 12485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ (𝑘 + 1))
128	37	absge0d 15341	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))
129	31, 38, 127, 128	mulge0d 11741	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 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 7369	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝑋↑𝑘) = (0↑𝑘))
133		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → 𝑘 ∈ (ℤ_≥‘1))
134	133, 124	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → 𝑘 ∈ ℕ)
135	134	0expd 14054	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (0↑𝑘) = 0)
136	132, 135	sylan9eqr 2793	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (𝑋↑𝑘) = 0)
137	136	oveq2d 7378	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0))
138	51	mul01d 11363	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 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 2771	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = 0)
142	141	abs00bd 15188	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = 0)
143	39	recnd 11192	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℂ)
144	143	mullidd 11182	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (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 5142	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑋 = 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
148		df-ne 2940	. . . . 5 ⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0)
149	54	abscld 15333	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ∈ ℝ)
150	50, 34, 53	mulassd 11187	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
151	150	fveq2d 6851	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
152	34, 53	mulcld 11184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) ∈ ℂ)
153	50, 152	absmuld 15351	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
154	31, 127	absidd 15319	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑘 + 1)) = (𝑘 + 1))
155	154	oveq1d 7377	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
156	151, 153, 155	3eqtrd 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
157	149, 156	eqled 11267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
158	157	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
159	23	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑋 ∈ ℂ)
160	116	rpreccld 12976	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ⁺)
161	159, 160	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℝ⁺)
162	161	rpcnd 12968	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (1 / (abs‘𝑋)) ∈ ℂ)
163	50	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℂ)
164	38	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ)
165	164	recnd 11192	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℂ)
166	162, 163, 165	mul12d 11373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
167	37	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ)
168	23	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑋 ∈ ℂ)
169		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0)
170	167, 168, 169	absdivd 15352	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)))
171	34	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
172	36	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑(𝑘 + 1)) ∈ ℂ)
173	171, 172, 168, 169	divassd 11975	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
174	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → 𝑘 ∈ ℂ)
175		pncan 11416	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
176	174, 4, 175	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) − 1) = 𝑘)
177	176	oveq2d 7378	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = (𝑋↑𝑘))
178	15	nn0zd 12534	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℤ)
179	178	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈ ℤ)
180	168, 169, 179	expm1d 14071	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = ((𝑋↑(𝑘 + 1)) / 𝑋))
181	177, 180	eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (𝑋↑𝑘) = ((𝑋↑(𝑘 + 1)) / 𝑋))
182	181	oveq2d 7378	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋)))
183	173, 182	eqtr4d 2774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))
184	183	fveq2d 6851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
185	23	abscld 15333	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘𝑋) ∈ ℝ)
186	185	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ)
187	186	recnd 11192	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℂ)
188	159, 116	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈ ℝ⁺)
189	188	rpne0d 12971	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ≠ 0)
190	165, 187, 189	divrec2d 11944	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)) = ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))
191	170, 184, 190	3eqtr3rd 2780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))
192	191	oveq2d 7378	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
193	166, 192	eqtrd 2771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))))
194	158, 193	breqtrrd 5138	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑋 ≠ 0) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
195	126, 194	sylanl2 679	. . . . 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 4529	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
198	49	fveq2d 6851	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
199	126, 198	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))))
200	30	oveq2d 7378	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
201	126, 200	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))
202	197, 199, 201	3brtr4d 5142	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (abs‘(𝐻‘𝑘)) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ₀ ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)))
203	1, 3, 40, 55, 113, 119, 202	cvgcmpce 15714	1 ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2939 {crab 3405 ifcif 4491 class class class wbr 5110 ↦ cmpt 5193 dom cdm 5638 ∘ ccom 5642 ⟶wf 6497 ‘cfv 6501 (class class class)co 7362 supcsup 9385 ℂcc 11058 ℝcr 11059 0cc0 11060 1c1 11061 + caddc 11063 · cmul 11065 ℝ^*cxr 11197 < clt 11198 ≤ cle 11199 − cmin 11394 -cneg 11395 / cdiv 11821 ℕcn 12162 ℕ₀cn0 12422 ℤcz 12508 ℤ_≥cuz 12772 ℝ⁺crp 12924 seqcseq 13916 ↑cexp 13977 shift cshi 14963 abscabs 15131 ⇝ cli 15378

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5247 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-inf2 9586 ax-cnex 11116 ax-resscn 11117 ax-1cn 11118 ax-icn 11119 ax-addcl 11120 ax-addrcl 11121 ax-mulcl 11122 ax-mulrcl 11123 ax-mulcom 11124 ax-addass 11125 ax-mulass 11126 ax-distr 11127 ax-i2m1 11128 ax-1ne0 11129 ax-1rid 11130 ax-rnegex 11131 ax-rrecex 11132 ax-cnre 11133 ax-pre-lttri 11134 ax-pre-lttrn 11135 ax-pre-ltadd 11136 ax-pre-mulgt0 11137 ax-pre-sup 11138

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-int 4913 df-iun 4961 df-br 5111 df-opab 5173 df-mpt 5194 df-tr 5228 df-id 5536 df-eprel 5542 df-po 5550 df-so 5551 df-fr 5593 df-se 5594 df-we 5595 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6258 df-ord 6325 df-on 6326 df-lim 6327 df-suc 6328 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-isom 6510 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7808 df-1st 7926 df-2nd 7927 df-frecs 8217 df-wrecs 8248 df-recs 8322 df-rdg 8361 df-1o 8417 df-er 8655 df-pm 8775 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-sup 9387 df-inf 9388 df-oi 9455 df-card 9884 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204 df-sub 11396 df-neg 11397 df-div 11822 df-nn 12163 df-2 12225 df-3 12226 df-n0 12423 df-z 12509 df-uz 12773 df-rp 12925 df-ico 13280 df-icc 13281 df-fz 13435 df-fzo 13578 df-fl 13707 df-seq 13917 df-exp 13978 df-hash 14241 df-shft 14964 df-cj 14996 df-re 14997 df-im 14998 df-sqrt 15132 df-abs 15133 df-limsup 15365 df-clim 15382 df-rlim 15383 df-sum 15583

This theorem is referenced by: pserdvlem2 25824 dvradcnv2 42749

W3C validator