Metamath Proof Explorer

Theorem logcnlem5

Description: Lemma for logcn . (Contributed by Mario Carneiro, 18-Feb-2015)

Ref Expression
Hypothesis logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion logcnlem5 ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℝ )

Proof

Step Hyp Ref Expression
1 logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 difss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
3 1 2 eqsstri ⊢ 𝐷 ⊆ ℂ
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) )
6 1 ellogdm ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
7 6 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
8 1 logdmn0 ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
9 7 8 logcld ⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ℂ )
10 9 imcld ⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ )
11 5 10 fmpti ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) : 𝐷 ⟶ ℝ
12 eqid ⊢ if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) = if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) )
13 eqid ⊢ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) )
14 simpl ⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ ℝ+ ) → 𝑦 ∈ 𝐷 )
15 simpr ⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ ℝ+ ) → 𝑧 ∈ ℝ+ )
16 1 12 13 14 15 logcnlem2 ⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ ℝ+ ) → if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) ∈ ℝ+ )
17 simpll ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) ) ) → 𝑦 ∈ 𝐷 )
18 simprl ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) ) ) → 𝑧 ∈ ℝ+ )
19 simplr ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) ) ) → 𝑤 ∈ 𝐷 )
20 simprr ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) ) ) → ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) )
21 1 12 13 17 18 19 20 logcnlem4 ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) ) ) → ( abs ‘ ( ( ℑ ‘ ( log ‘ 𝑦 ) ) − ( ℑ ‘ ( log ‘ 𝑤 ) ) ) ) < 𝑧 )
22 21 expr ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) → ( abs ‘ ( ( ℑ ‘ ( log ‘ 𝑦 ) ) − ( ℑ ‘ ( log ‘ 𝑤 ) ) ) ) < 𝑧 ) )
23 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( ℑ ‘ ( log ‘ 𝑥 ) ) = ( ℑ ‘ ( log ‘ 𝑦 ) ) )
24 fvex ⊢ ( ℑ ‘ ( log ‘ 𝑦 ) ) ∈ V
25 23 5 24 fvmpt ⊢ ( 𝑦 ∈ 𝐷 → ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑦 ) = ( ℑ ‘ ( log ‘ 𝑦 ) ) )
26 25 ad2antrr ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑦 ) = ( ℑ ‘ ( log ‘ 𝑦 ) ) )
27 2fveq3 ⊢ ( 𝑥 = 𝑤 → ( ℑ ‘ ( log ‘ 𝑥 ) ) = ( ℑ ‘ ( log ‘ 𝑤 ) ) )
28 fvex ⊢ ( ℑ ‘ ( log ‘ 𝑤 ) ) ∈ V
29 27 5 28 fvmpt ⊢ ( 𝑤 ∈ 𝐷 → ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑤 ) = ( ℑ ‘ ( log ‘ 𝑤 ) ) )
30 29 ad2antlr ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑤 ) = ( ℑ ‘ ( log ‘ 𝑤 ) ) )
31 26 30 oveq12d ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑦 ) − ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑤 ) ) = ( ( ℑ ‘ ( log ‘ 𝑦 ) ) − ( ℑ ‘ ( log ‘ 𝑤 ) ) ) )
32 31 fveq2d ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( abs ‘ ( ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑦 ) − ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑤 ) ) ) = ( abs ‘ ( ( ℑ ‘ ( log ‘ 𝑦 ) ) − ( ℑ ‘ ( log ‘ 𝑤 ) ) ) ) )
33 32 breq1d ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( abs ‘ ( ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑦 ) − ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑤 ) ) ) < 𝑧 ↔ ( abs ‘ ( ( ℑ ‘ ( log ‘ 𝑦 ) ) − ( ℑ ‘ ( log ‘ 𝑤 ) ) ) ) < 𝑧 ) )
34 22 33 sylibrd ⊢ ( ( ( 𝑦 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( abs ‘ ( 𝑦 − 𝑤 ) ) < if ( if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) ≤ ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) , if ( 𝑦 ∈ ℝ+ , 𝑦 , ( abs ‘ ( ℑ ‘ 𝑦 ) ) ) , ( ( abs ‘ 𝑦 ) · ( 𝑧 / ( 1 + 𝑧 ) ) ) ) → ( abs ‘ ( ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑦 ) − ( ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ‘ 𝑤 ) ) ) < 𝑧 ) )
35 11 16 34 elcncf1ii ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℝ ) )
36 3 4 35 mp2an ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℝ )