Metamath Proof Explorer

Theorem logcnlem5

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

Ref Expression
Hypothesis logcn.d ⊢D=ℂ∖−∞0
Assertion logcnlem5 ⊢x∈D⟼ℑ⁡log⁡x:D⟶cnℝ

Proof

Step Hyp Ref Expression
1 logcn.d ⊢D=ℂ∖−∞0
2 difss ⊢ℂ∖−∞0⊆ℂ
3 1 2 eqsstri ⊢D⊆ℂ
4 ax-resscn ⊢ℝ⊆ℂ
5 eqid ⊢x∈D⟼ℑ⁡log⁡x=x∈D⟼ℑ⁡log⁡x
6 1 ellogdm ⊢x∈D↔x∈ℂ∧x∈ℝ→x∈ℝ+
7 6 simplbi ⊢x∈D→x∈ℂ
8 1 logdmn0 ⊢x∈D→x≠0
9 7 8 logcld ⊢x∈D→log⁡x∈ℂ
10 9 imcld ⊢x∈D→ℑ⁡log⁡x∈ℝ
11 5 10 fmpti ⊢x∈D⟼ℑ⁡log⁡x:D⟶ℝ
12 eqid ⊢ify∈ℝ+yℑ⁡y=ify∈ℝ+yℑ⁡y
13 eqid ⊢y⁢z1+z=y⁢z1+z
14 simpl ⊢y∈D∧z∈ℝ+→y∈D
15 simpr ⊢y∈D∧z∈ℝ+→z∈ℝ+
16 1 12 13 14 15 logcnlem2 ⊢y∈D∧z∈ℝ+→ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z∈ℝ+
17 simpll ⊢y∈D∧w∈D∧z∈ℝ+∧y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→y∈D
18 simprl ⊢y∈D∧w∈D∧z∈ℝ+∧y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→z∈ℝ+
19 simplr ⊢y∈D∧w∈D∧z∈ℝ+∧y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→w∈D
20 simprr ⊢y∈D∧w∈D∧z∈ℝ+∧y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z
21 1 12 13 17 18 19 20 logcnlem4 ⊢y∈D∧w∈D∧z∈ℝ+∧y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→ℑ⁡log⁡y−ℑ⁡log⁡w<z
22 21 expr ⊢y∈D∧w∈D∧z∈ℝ+→y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→ℑ⁡log⁡y−ℑ⁡log⁡w<z
23 2fveq3 ⊢x=y→ℑ⁡log⁡x=ℑ⁡log⁡y
24 fvex ⊢ℑ⁡log⁡y∈V
25 23 5 24 fvmpt ⊢y∈D→x∈D⟼ℑ⁡log⁡x⁡y=ℑ⁡log⁡y
26 25 ad2antrr ⊢y∈D∧w∈D∧z∈ℝ+→x∈D⟼ℑ⁡log⁡x⁡y=ℑ⁡log⁡y
27 2fveq3 ⊢x=w→ℑ⁡log⁡x=ℑ⁡log⁡w
28 fvex ⊢ℑ⁡log⁡w∈V
29 27 5 28 fvmpt ⊢w∈D→x∈D⟼ℑ⁡log⁡x⁡w=ℑ⁡log⁡w
30 29 ad2antlr ⊢y∈D∧w∈D∧z∈ℝ+→x∈D⟼ℑ⁡log⁡x⁡w=ℑ⁡log⁡w
31 26 30 oveq12d ⊢y∈D∧w∈D∧z∈ℝ+→x∈D⟼ℑ⁡log⁡x⁡y−x∈D⟼ℑ⁡log⁡x⁡w=ℑ⁡log⁡y−ℑ⁡log⁡w
32 31 fveq2d ⊢y∈D∧w∈D∧z∈ℝ+→x∈D⟼ℑ⁡log⁡x⁡y−x∈D⟼ℑ⁡log⁡x⁡w=ℑ⁡log⁡y−ℑ⁡log⁡w
33 32 breq1d ⊢y∈D∧w∈D∧z∈ℝ+→x∈D⟼ℑ⁡log⁡x⁡y−x∈D⟼ℑ⁡log⁡x⁡w<z↔ℑ⁡log⁡y−ℑ⁡log⁡w<z
34 22 33 sylibrd ⊢y∈D∧w∈D∧z∈ℝ+→y−w<ifify∈ℝ+yℑ⁡y≤y⁢z1+zify∈ℝ+yℑ⁡yy⁢z1+z→x∈D⟼ℑ⁡log⁡x⁡y−x∈D⟼ℑ⁡log⁡x⁡w<z
35 11 16 34 elcncf1ii ⊢D⊆ℂ∧ℝ⊆ℂ→x∈D⟼ℑ⁡log⁡x:D⟶cnℝ
36 3 4 35 mp2an ⊢x∈D⟼ℑ⁡log⁡x:D⟶cnℝ