Theorem rpdmgm

Description: A positive real number is in the domain of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	rpdmgm	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
2		ax-1	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) )
3		eqid	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
4	3	ellogdm	⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )
5	1 2 4	sylanbrc	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
6		dmlogdmgm	⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
7	5 6	syl	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )