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→ ℝ )