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∈ℂ∖ℤ∖ℕ