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 ⊢ if y ∈ ℝ + y ℑ ⁡ y = if y ∈ ℝ + y ℑ ⁡ y
13 eqid ⊢ y ⁢ z 1 + z = y ⁢ z 1 + z
14 simpl ⊢ y ∈ D ∧ z ∈ ℝ + → y ∈ D
15 simpr ⊢ y ∈ D ∧ z ∈ ℝ + → z ∈ ℝ +
16 1 12 13 14 15 logcnlem2 ⊢ y ∈ D ∧ z ∈ ℝ + → if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z ∈ ℝ +
17 simpll ⊢ y ∈ D ∧ w ∈ D ∧ z ∈ ℝ + ∧ y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z → y ∈ D
18 simprl ⊢ y ∈ D ∧ w ∈ D ∧ z ∈ ℝ + ∧ y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z → z ∈ ℝ +
19 simplr ⊢ y ∈ D ∧ w ∈ D ∧ z ∈ ℝ + ∧ y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z → w ∈ D
20 simprr ⊢ y ∈ D ∧ w ∈ D ∧ z ∈ ℝ + ∧ y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z → y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z
21 1 12 13 17 18 19 20 logcnlem4 ⊢ y ∈ D ∧ w ∈ D ∧ z ∈ ℝ + ∧ y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + z → ℑ ⁡ log ⁡ y − ℑ ⁡ log ⁡ w < z
22 21 expr ⊢ y ∈ D ∧ w ∈ D ∧ z ∈ ℝ + → y − w < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + 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 < if if y ∈ ℝ + y ℑ ⁡ y ≤ y ⁢ z 1 + z if y ∈ ℝ + y ℑ ⁡ y y ⁢ z 1 + 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 ℝ