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

Proof

Step Hyp Ref Expression
1 dvradcnv2.g ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
2 dvradcnv2.r ⊢ R = sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
3 dvradcnv2.h ⊢ H = n ∈ ℕ ⟼ n ⁢ A ⁡ n ⁢ X n − 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 → seq 0 − -1 + H = seq 1 + H
13 11 12 ax-mp ⊢ seq 0 − -1 + H = seq 1 + H
14 ovex ⊢ n ⁢ A ⁡ n ⁢ X n − 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 → X n − 1 = X m - -1 - 1
20 17 19 oveq12d ⊢ n = m − -1 → n ⁢ A ⁡ n ⁢ X n − 1 = m − -1 ⁢ A ⁡ m − -1 ⁢ X m - -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 ⊢ φ → H shift -1 = m ∈ ℕ 0 ⟼ m − -1 ⁢ A ⁡ m − -1 ⁢ X m - -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 → X m - -1 - 1 = X m
39 34 38 oveq12d ⊢ φ ∧ m ∈ ℕ 0 → m − -1 ⁢ A ⁡ m − -1 ⁢ X m - -1 - 1 = m + 1 ⁢ A ⁡ m + 1 ⁢ X m
40 39 mpteq2dva ⊢ φ → m ∈ ℕ 0 ⟼ m − -1 ⁢ A ⁡ m − -1 ⁢ X m - -1 - 1 = m ∈ ℕ 0 ⟼ m + 1 ⁢ A ⁡ m + 1 ⁢ X m
41 28 40 eqtrd ⊢ φ → H shift -1 = m ∈ ℕ 0 ⟼ m + 1 ⁢ A ⁡ m + 1 ⁢ X m
42 41 seqeq3d ⊢ φ → seq 0 + H shift -1 = seq 0 + m ∈ ℕ 0 ⟼ m + 1 ⁢ A ⁡ m + 1 ⁢ X m
43 fveq2 ⊢ n = m → A ⁡ n = A ⁡ m
44 oveq2 ⊢ n = m → x n = x m
45 43 44 oveq12d ⊢ n = m → A ⁡ n ⁢ x n = A ⁡ m ⁢ x m
46 45 cbvmptv ⊢ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n = m ∈ ℕ 0 ⟼ A ⁡ m ⁢ x m
47 46 mpteq2i ⊢ x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n = x ∈ ℂ ⟼ m ∈ ℕ 0 ⟼ A ⁡ m ⁢ x m
48 1 47 eqtri ⊢ G = x ∈ ℂ ⟼ m ∈ ℕ 0 ⟼ A ⁡ m ⁢ x m
49 eqid ⊢ m ∈ ℕ 0 ⟼ m + 1 ⁢ A ⁡ m + 1 ⁢ X m = m ∈ ℕ 0 ⟼ m + 1 ⁢ A ⁡ m + 1 ⁢ X m
50 48 2 49 4 5 6 dvradcnv ⊢ φ → seq 0 + m ∈ ℕ 0 ⟼ m + 1 ⁢ A ⁡ m + 1 ⁢ X m ∈ dom ⁡ ⇝
51 42 50 eqeltrd ⊢ φ → seq 0 + H shift -1 ∈ dom ⁡ ⇝
52 climdm ⊢ seq 0 + H shift -1 ∈ dom ⁡ ⇝ ↔ seq 0 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1
53 51 52 sylib ⊢ φ → seq 0 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1
54 0z ⊢ 0 ∈ ℤ
55 neg1z ⊢ − 1 ∈ ℤ
56 nnex ⊢ ℕ ∈ V
57 56 mptex ⊢ n ∈ ℕ ⟼ n ⁢ A ⁡ n ⁢ X n − 1 ∈ V
58 3 57 eqeltri ⊢ H ∈ V
59 58 seqshft ⊢ 0 ∈ ℤ ∧ − 1 ∈ ℤ → seq 0 + H shift -1 = seq 0 − -1 + H shift -1
60 54 55 59 mp2an ⊢ seq 0 + H shift -1 = seq 0 − -1 + H shift -1
61 60 breq1i ⊢ seq 0 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1 ↔ seq 0 − -1 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1
62 seqex ⊢ seq 0 − -1 + H ∈ V
63 climshft ⊢ − 1 ∈ ℤ ∧ seq 0 − -1 + H ∈ V → seq 0 − -1 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1 ↔ seq 0 − -1 + H ⇝ ⇝ ⁡ seq 0 + H shift -1
64 55 62 63 mp2an ⊢ seq 0 − -1 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1 ↔ seq 0 − -1 + H ⇝ ⇝ ⁡ seq 0 + H shift -1
65 61 64 bitri ⊢ seq 0 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1 ↔ seq 0 − -1 + H ⇝ ⇝ ⁡ seq 0 + H shift -1
66 fvex ⊢ ⇝ ⁡ seq 0 + H shift -1 ∈ V
67 62 66 breldm ⊢ seq 0 − -1 + H ⇝ ⇝ ⁡ seq 0 + H shift -1 → seq 0 − -1 + H ∈ dom ⁡ ⇝
68 65 67 sylbi ⊢ seq 0 + H shift -1 ⇝ ⇝ ⁡ seq 0 + H shift -1 → seq 0 − -1 + H ∈ dom ⁡ ⇝
69 53 68 syl ⊢ φ → seq 0 − -1 + H ∈ dom ⁡ ⇝
70 13 69 eqeltrrid ⊢ φ → seq 1 + H ∈ dom ⁡ ⇝