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 ⇝ )