Metamath Proof Explorer

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 ⊢G=x∈ℂ⟼n∈ℕ0⟼A⁡n⁢xn
dvradcnv2.r ⊢R=supr∈ℝ|seq0+G⁡r∈dom⁡⇝ℝ*<
dvradcnv2.h ⊢H=n∈ℕ⟼n⁢A⁡n⁢Xn−1
dvradcnv2.a ⊢φ→A:ℕ0⟶ℂ
dvradcnv2.x ⊢φ→X∈ℂ
dvradcnv2.l ⊢φ→X<R
Assertion dvradcnv2 ⊢φ→seq1+H∈dom⁡⇝

Proof

Step Hyp Ref Expression
1 dvradcnv2.g ⊢G=x∈ℂ⟼n∈ℕ0⟼A⁡n⁢xn
2 dvradcnv2.r ⊢R=supr∈ℝ|seq0+G⁡r∈dom⁡⇝ℝ*<
3 dvradcnv2.h ⊢H=n∈ℕ⟼n⁢A⁡n⁢Xn−1
4 dvradcnv2.a ⊢φ→A:ℕ0⟶ℂ
5 dvradcnv2.x ⊢φ→X∈ℂ
6 dvradcnv2.l ⊢φ→X<R
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→seq0−-1+H=seq1+H
13 11 12 ax-mp ⊢seq0−-1+H=seq1+H
14 ovex ⊢n⁢A⁡n⁢Xn−1∈V
15 id ⊢n=m−-1→n=m−-1
16 fveq2 ⊢n=m−-1→A⁡n=A⁡m−-1
17 15 16 oveq12d ⊢n=m−-1→n⁢A⁡n=m−-1⁢A⁡m−-1
18 oveq1 ⊢n=m−-1→n−1=m--1-1
19 18 oveq2d ⊢n=m−-1→Xn−1=Xm--1-1
20 17 19 oveq12d ⊢n=m−-1→n⁢A⁡n⁢Xn−1=m−-1⁢A⁡m−-1⁢Xm--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 ⊢φ→Hshift-1=m∈ℕ0⟼m−-1⁢A⁡m−-1⁢Xm--1-1
29 nn0cn ⊢m∈ℕ0→m∈ℂ
30 29 adantl ⊢φ∧m∈ℕ0→m∈ℂ
31 1cnd ⊢φ∧m∈ℕ0→1∈ℂ
32 30 31 subnegd ⊢φ∧m∈ℕ0→m−-1=m+1
33 32 fveq2d ⊢φ∧m∈ℕ0→A⁡m−-1=A⁡m+1
34 32 33 oveq12d ⊢φ∧m∈ℕ0→m−-1⁢A⁡m−-1=m+1⁢A⁡m+1
35 32 oveq1d ⊢φ∧m∈ℕ0→m--1-1=m+1-1
36 30 31 pncand ⊢φ∧m∈ℕ0→m+1-1=m
37 35 36 eqtrd ⊢φ∧m∈ℕ0→m--1-1=m
38 37 oveq2d ⊢φ∧m∈ℕ0→Xm--1-1=Xm
39 34 38 oveq12d ⊢φ∧m∈ℕ0→m−-1⁢A⁡m−-1⁢Xm--1-1=m+1⁢A⁡m+1⁢Xm
40 39 mpteq2dva ⊢φ→m∈ℕ0⟼m−-1⁢A⁡m−-1⁢Xm--1-1=m∈ℕ0⟼m+1⁢A⁡m+1⁢Xm
41 28 40 eqtrd ⊢φ→Hshift-1=m∈ℕ0⟼m+1⁢A⁡m+1⁢Xm
42 41 seqeq3d ⊢φ→seq0+Hshift-1=seq0+m∈ℕ0⟼m+1⁢A⁡m+1⁢Xm
43 fveq2 ⊢n=m→A⁡n=A⁡m
44 oveq2 ⊢n=m→xn=xm
45 43 44 oveq12d ⊢n=m→A⁡n⁢xn=A⁡m⁢xm
46 45 cbvmptv ⊢n∈ℕ0⟼A⁡n⁢xn=m∈ℕ0⟼A⁡m⁢xm
47 46 mpteq2i ⊢x∈ℂ⟼n∈ℕ0⟼A⁡n⁢xn=x∈ℂ⟼m∈ℕ0⟼A⁡m⁢xm
48 1 47 eqtri ⊢G=x∈ℂ⟼m∈ℕ0⟼A⁡m⁢xm
49 eqid ⊢m∈ℕ0⟼m+1⁢A⁡m+1⁢Xm=m∈ℕ0⟼m+1⁢A⁡m+1⁢Xm
50 48 2 49 4 5 6 dvradcnv ⊢φ→seq0+m∈ℕ0⟼m+1⁢A⁡m+1⁢Xm∈dom⁡⇝
51 42 50 eqeltrd ⊢φ→seq0+Hshift-1∈dom⁡⇝
52 climdm ⊢seq0+Hshift-1∈dom⁡⇝↔seq0+Hshift-1⇝⇝⁡seq0+Hshift-1
53 51 52 sylib ⊢φ→seq0+Hshift-1⇝⇝⁡seq0+Hshift-1
54 0z ⊢0∈ℤ
55 neg1z ⊢−1∈ℤ
56 nnex ⊢ℕ∈V
57 56 mptex ⊢n∈ℕ⟼n⁢A⁡n⁢Xn−1∈V
58 3 57 eqeltri ⊢H∈V
59 58 seqshft ⊢0∈ℤ∧−1∈ℤ→seq0+Hshift-1=seq0−-1+Hshift-1
60 54 55 59 mp2an ⊢seq0+Hshift-1=seq0−-1+Hshift-1
61 60 breq1i ⊢seq0+Hshift-1⇝⇝⁡seq0+Hshift-1↔seq0−-1+Hshift-1⇝⇝⁡seq0+Hshift-1
62 seqex ⊢seq0−-1+H∈V
63 climshft ⊢−1∈ℤ∧seq0−-1+H∈V→seq0−-1+Hshift-1⇝⇝⁡seq0+Hshift-1↔seq0−-1+H⇝⇝⁡seq0+Hshift-1
64 55 62 63 mp2an ⊢seq0−-1+Hshift-1⇝⇝⁡seq0+Hshift-1↔seq0−-1+H⇝⇝⁡seq0+Hshift-1
65 61 64 bitri ⊢seq0+Hshift-1⇝⇝⁡seq0+Hshift-1↔seq0−-1+H⇝⇝⁡seq0+Hshift-1
66 fvex ⊢⇝⁡seq0+Hshift-1∈V
67 62 66 breldm ⊢seq0−-1+H⇝⇝⁡seq0+Hshift-1→seq0−-1+H∈dom⁡⇝
68 65 67 sylbi ⊢seq0+Hshift-1⇝⇝⁡seq0+Hshift-1→seq0−-1+H∈dom⁡⇝
69 53 68 syl ⊢φ→seq0−-1+H∈dom⁡⇝
70 13 69 eqeltrrid ⊢φ→seq1+H∈dom⁡⇝