Database
REAL AND COMPLEX NUMBERS
Elementary limits and convergence
Limits
climim
Metamath Proof Explorer
Description: Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of
Gleason p. 172. (Contributed by NM , 7-Jun-2006) (Revised by Mario
Carneiro , 9-Feb-2014)
Ref
Expression
Hypotheses
climcn1lem.1
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climcn1lem.2
⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climcn1lem.4
⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
climcn1lem.5
⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climcn1lem.6
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
climim.7
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion
climim
⊢ ( 𝜑 → 𝐺 ⇝ ( ℑ ‘ 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
climcn1lem.1
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2
climcn1lem.2
⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
3
climcn1lem.4
⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
4
climcn1lem.5
⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5
climcn1lem.6
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
6
climim.7
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑘 ) ) )
7
imf
⊢ ℑ : ℂ ⟶ ℝ
8
ax-resscn
⊢ ℝ ⊆ ℂ
9
fss
⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℑ : ℂ ⟶ ℂ )
10
7 8 9
mp2an
⊢ ℑ : ℂ ⟶ ℂ
11
imcn2
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) < 𝑥 ) )
12
1 2 3 4 5 10 11 6
climcn1lem
⊢ ( 𝜑 → 𝐺 ⇝ ( ℑ ‘ 𝐴 ) )