This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem radcnvlem3

Description: Lemma for radcnvlt1 , radcnvle . If X is a point closer to zero than Y and the power series converges at Y , then it converges at X . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
psergf.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
radcnvlem2.y ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
radcnvlem2.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑌 ) )
radcnvlem2.c ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑌 ) ) ∈ dom ⇝ )
Assertion radcnvlem3 ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
3 psergf.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4 radcnvlem2.y ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
5 radcnvlem2.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑌 ) )
6 radcnvlem2.c ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑌 ) ) ∈ dom ⇝ )
7 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
9 1 2 3 psergf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )
10 fvco3 ⊢ ( ( ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) )
11 9 10 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) )
12 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ∈ ℂ )
13 1 2 3 4 5 6 radcnvlem2 ⊢ ( 𝜑 → seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ )
14 7 8 11 12 13 abscvgcvg ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )