Theorem dvradcnv2

Description: The radius of convergence of the (formal) derivative H of the power series G is (at least) as large as the radius of convergence of G . This version of dvradcnv uses a shifted version of H to match the sum form of ( CC _D F ) in pserdv2 (and shows how to use uzmptshftfval to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		dvradcnv2.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		dvradcnv2.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
3		dvradcnv2.h	⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 · ( 𝐴 ‘ 𝑛 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) )
4		dvradcnv2.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
5		dvradcnv2.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6		dvradcnv2.l	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
7		0cn	⊢ 0 ∈ ℂ
8		ax-1cn	⊢ 1 ∈ ℂ
9	7 8	subnegi	⊢ ( 0 − - 1 ) = ( 0 + 1 )
10		0p1e1	⊢ ( 0 + 1 ) = 1
11	9 10	eqtri	⊢ ( 0 − - 1 ) = 1
12		seqeq1	⊢ ( ( 0 − - 1 ) = 1 → seq ( 0 − - 1 ) ( + , 𝐻 ) = seq 1 ( + , 𝐻 ) )
13	11 12	ax-mp	⊢ seq ( 0 − - 1 ) ( + , 𝐻 ) = seq 1 ( + , 𝐻 )
14		ovex	⊢ ( ( 𝑛 · ( 𝐴 ‘ 𝑛 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ∈ V
15		id	⊢ ( 𝑛 = ( 𝑚 − - 1 ) → 𝑛 = ( 𝑚 − - 1 ) )
16		fveq2	⊢ ( 𝑛 = ( 𝑚 − - 1 ) → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ ( 𝑚 − - 1 ) ) )
17	15 16	oveq12d	⊢ ( 𝑛 = ( 𝑚 − - 1 ) → ( 𝑛 · ( 𝐴 ‘ 𝑛 ) ) = ( ( 𝑚 − - 1 ) · ( 𝐴 ‘ ( 𝑚 − - 1 ) ) ) )
18		oveq1	⊢ ( 𝑛 = ( 𝑚 − - 1 ) → ( 𝑛 − 1 ) = ( ( 𝑚 − - 1 ) − 1 ) )
19	18	oveq2d	⊢ ( 𝑛 = ( 𝑚 − - 1 ) → ( 𝑋 ↑ ( 𝑛 − 1 ) ) = ( 𝑋 ↑ ( ( 𝑚 − - 1 ) − 1 ) ) )
20	17 19	oveq12d	⊢ ( 𝑛 = ( 𝑚 − - 1 ) → ( ( 𝑛 · ( 𝐴 ‘ 𝑛 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) = ( ( ( 𝑚 − - 1 ) · ( 𝐴 ‘ ( 𝑚 − - 1 ) ) ) · ( 𝑋 ↑ ( ( 𝑚 − - 1 ) − 1 ) ) ) )
21		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
22		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
23		1pneg1e0	⊢ ( 1 + - 1 ) = 0
24	23	fveq2i	⊢ ( ℤ≥ ‘ ( 1 + - 1 ) ) = ( ℤ≥ ‘ 0 )
25	22 24	eqtr4i	⊢ ℕ0 = ( ℤ≥ ‘ ( 1 + - 1 ) )
26		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
27	26	znegcld	⊢ ( 𝜑 → - 1 ∈ ℤ )
28	3 14 20 21 25 26 27	uzmptshftfval	⊢ ( 𝜑 → ( 𝐻 shift - 1 ) = ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 − - 1 ) · ( 𝐴 ‘ ( 𝑚 − - 1 ) ) ) · ( 𝑋 ↑ ( ( 𝑚 − - 1 ) − 1 ) ) ) ) )
29		nn0cn	⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
31		1cnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 1 ∈ ℂ )
32	30 31	subnegd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 − - 1 ) = ( 𝑚 + 1 ) )
33	32	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑚 − - 1 ) ) = ( 𝐴 ‘ ( 𝑚 + 1 ) ) )
34	32 33	oveq12d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 − - 1 ) · ( 𝐴 ‘ ( 𝑚 − - 1 ) ) ) = ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) )
35	32	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 − - 1 ) − 1 ) = ( ( 𝑚 + 1 ) − 1 ) )
36	30 31	pncand	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
37	35 36	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 − - 1 ) − 1 ) = 𝑚 )
38	37	oveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑋 ↑ ( ( 𝑚 − - 1 ) − 1 ) ) = ( 𝑋 ↑ 𝑚 ) )
39	34 38	oveq12d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝑚 − - 1 ) · ( 𝐴 ‘ ( 𝑚 − - 1 ) ) ) · ( 𝑋 ↑ ( ( 𝑚 − - 1 ) − 1 ) ) ) = ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) )
40	39	mpteq2dva	⊢ ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 − - 1 ) · ( 𝐴 ‘ ( 𝑚 − - 1 ) ) ) · ( 𝑋 ↑ ( ( 𝑚 − - 1 ) − 1 ) ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) ) )
41	28 40	eqtrd	⊢ ( 𝜑 → ( 𝐻 shift - 1 ) = ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) ) )
42	41	seqeq3d	⊢ ( 𝜑 → seq 0 ( + , ( 𝐻 shift - 1 ) ) = seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) ) ) )
43		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑚 ) )
44		oveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑚 ) )
45	43 44	oveq12d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) )
46	45	cbvmptv	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) )
47	46	mpteq2i	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) )
48	1 47	eqtri	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) )
49		eqid	⊢ ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) )
50	48 2 49 4 5 6	dvradcnv	⊢ ( 𝜑 → seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) · ( 𝑋 ↑ 𝑚 ) ) ) ) ∈ dom ⇝ )
51	42 50	eqeltrd	⊢ ( 𝜑 → seq 0 ( + , ( 𝐻 shift - 1 ) ) ∈ dom ⇝ )
52		climdm	⊢ ( seq 0 ( + , ( 𝐻 shift - 1 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐻 shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) )
53	51 52	sylib	⊢ ( 𝜑 → seq 0 ( + , ( 𝐻 shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) )
54		0z	⊢ 0 ∈ ℤ
55		neg1z	⊢ - 1 ∈ ℤ
56		nnex	⊢ ℕ ∈ V
57	56	mptex	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 · ( 𝐴 ‘ 𝑛 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) ∈ V
58	3 57	eqeltri	⊢ 𝐻 ∈ V
59	58	seqshft	⊢ ( ( 0 ∈ ℤ ∧ - 1 ∈ ℤ ) → seq 0 ( + , ( 𝐻 shift - 1 ) ) = ( seq ( 0 − - 1 ) ( + , 𝐻 ) shift - 1 ) )
60	54 55 59	mp2an	⊢ seq 0 ( + , ( 𝐻 shift - 1 ) ) = ( seq ( 0 − - 1 ) ( + , 𝐻 ) shift - 1 )
61	60	breq1i	⊢ ( seq 0 ( + , ( 𝐻 shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) ↔ ( seq ( 0 − - 1 ) ( + , 𝐻 ) shift - 1 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) )
62		seqex	⊢ seq ( 0 − - 1 ) ( + , 𝐻 ) ∈ V
63		climshft	⊢ ( ( - 1 ∈ ℤ ∧ seq ( 0 − - 1 ) ( + , 𝐻 ) ∈ V ) → ( ( seq ( 0 − - 1 ) ( + , 𝐻 ) shift - 1 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) ↔ seq ( 0 − - 1 ) ( + , 𝐻 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) ) )
64	55 62 63	mp2an	⊢ ( ( seq ( 0 − - 1 ) ( + , 𝐻 ) shift - 1 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) ↔ seq ( 0 − - 1 ) ( + , 𝐻 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) )
65	61 64	bitri	⊢ ( seq 0 ( + , ( 𝐻 shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) ↔ seq ( 0 − - 1 ) ( + , 𝐻 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) )
66		fvex	⊢ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) ∈ V
67	62 66	breldm	⊢ ( seq ( 0 − - 1 ) ( + , 𝐻 ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) → seq ( 0 − - 1 ) ( + , 𝐻 ) ∈ dom ⇝ )
68	65 67	sylbi	⊢ ( seq 0 ( + , ( 𝐻 shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝐻 shift - 1 ) ) ) → seq ( 0 − - 1 ) ( + , 𝐻 ) ∈ dom ⇝ )
69	53 68	syl	⊢ ( 𝜑 → seq ( 0 − - 1 ) ( + , 𝐻 ) ∈ dom ⇝ )
70	13 69	eqeltrrid	⊢ ( 𝜑 → seq 1 ( + , 𝐻 ) ∈ dom ⇝ )