Metamath Proof Explorer

Theorem rlimrecl

Description: The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016)

Ref Expression
Hypotheses rlimcld2.1 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
rlimcld2.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
rlimrecl.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion rlimrecl ( 𝜑 → 𝐶 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 rlimcld2.1 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
2 rlimcld2.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
3 rlimrecl.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 4 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
6 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ ℝ ) → 𝑦 ∈ ℂ )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → 𝑦 ∈ ℂ )
8 7 imcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ( ℑ ‘ 𝑦 ) ∈ ℝ )
9 8 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ( ℑ ‘ 𝑦 ) ∈ ℂ )
10 eldifn ⊢ ( 𝑦 ∈ ( ℂ ∖ ℝ ) → ¬ 𝑦 ∈ ℝ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ¬ 𝑦 ∈ ℝ )
12 reim0b ⊢ ( 𝑦 ∈ ℂ → ( 𝑦 ∈ ℝ ↔ ( ℑ ‘ 𝑦 ) = 0 ) )
13 7 12 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ( 𝑦 ∈ ℝ ↔ ( ℑ ‘ 𝑦 ) = 0 ) )
14 13 necon3bbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ( ¬ 𝑦 ∈ ℝ ↔ ( ℑ ‘ 𝑦 ) ≠ 0 ) )
15 11 14 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ( ℑ ‘ 𝑦 ) ≠ 0 )
16 9 15 absrpcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) → ( abs ‘ ( ℑ ‘ 𝑦 ) ) ∈ ℝ+ )
17 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → 𝑦 ∈ ℂ )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
19 18 recnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℂ )
20 17 19 subcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝑦 − 𝑧 ) ∈ ℂ )
21 absimle ⊢ ( ( 𝑦 − 𝑧 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( 𝑦 − 𝑧 ) ) ) ≤ ( abs ‘ ( 𝑦 − 𝑧 ) ) )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ ( 𝑦 − 𝑧 ) ) ) ≤ ( abs ‘ ( 𝑦 − 𝑧 ) ) )
23 17 19 imsubd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( ℑ ‘ ( 𝑦 − 𝑧 ) ) = ( ( ℑ ‘ 𝑦 ) − ( ℑ ‘ 𝑧 ) ) )
24 reim0 ⊢ ( 𝑧 ∈ ℝ → ( ℑ ‘ 𝑧 ) = 0 )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( ℑ ‘ 𝑧 ) = 0 )
26 25 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( ( ℑ ‘ 𝑦 ) − ( ℑ ‘ 𝑧 ) ) = ( ( ℑ ‘ 𝑦 ) − 0 ) )
27 9 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( ℑ ‘ 𝑦 ) ∈ ℂ )
28 27 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( ( ℑ ‘ 𝑦 ) − 0 ) = ( ℑ ‘ 𝑦 ) )
29 23 26 28 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( ℑ ‘ 𝑦 ) = ( ℑ ‘ ( 𝑦 − 𝑧 ) ) )
30 29 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑦 ) ) = ( abs ‘ ( ℑ ‘ ( 𝑦 − 𝑧 ) ) ) )
31 19 17 abssubd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
32 22 30 31 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ℝ ) ) ∧ 𝑧 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
33 1 2 5 16 32 3 rlimcld2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )