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 ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )

Proof

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