Metamath Proof Explorer

Theorem dmlogdmgm

Description: If A is in the continuous domain of the logarithm, then it is in the domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017)

Ref Expression
Assertion dmlogdmgm ⊢ A ∈ ℂ ∖ −∞ 0 → A ∈ ℂ ∖ ℤ ∖ ℕ

Proof

Step Hyp Ref Expression
1 eldifi ⊢ A ∈ ℂ ∖ −∞ 0 → A ∈ ℂ
2 simpr ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → − A ∈ ℕ 0
3 2 nn0ge0d ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → 0 ≤ − A
4 1 adantr ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → A ∈ ℂ
5 2 nn0red ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → − A ∈ ℝ
6 4 5 negrebd ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → A ∈ ℝ
7 eqid ⊢ ℂ ∖ −∞ 0 = ℂ ∖ −∞ 0
8 7 ellogdm ⊢ A ∈ ℂ ∖ −∞ 0 ↔ A ∈ ℂ ∧ A ∈ ℝ → A ∈ ℝ +
9 8 simprbi ⊢ A ∈ ℂ ∖ −∞ 0 → A ∈ ℝ → A ∈ ℝ +
10 9 imp ⊢ A ∈ ℂ ∖ −∞ 0 ∧ A ∈ ℝ → A ∈ ℝ +
11 6 10 syldan ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → A ∈ ℝ +
12 11 rpgt0d ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → 0 < A
13 6 lt0neg2d ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → 0 < A ↔ − A < 0
14 12 13 mpbid ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → − A < 0
15 0red ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → 0 ∈ ℝ
16 5 15 ltnled ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → − A < 0 ↔ ¬ 0 ≤ − A
17 14 16 mpbid ⊢ A ∈ ℂ ∖ −∞ 0 ∧ − A ∈ ℕ 0 → ¬ 0 ≤ − A
18 3 17 pm2.65da ⊢ A ∈ ℂ ∖ −∞ 0 → ¬ − A ∈ ℕ 0
19 eldmgm ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ ↔ A ∈ ℂ ∧ ¬ − A ∈ ℕ 0
20 1 18 19 sylanbrc ⊢ A ∈ ℂ ∖ −∞ 0 → A ∈ ℂ ∖ ℤ ∖ ℕ