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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ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 ⇝ )