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	|- ( A e. RR+ -> A e. ( CC \ ( ZZ \ NN ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	|- ( A e. RR+ -> A e. CC )
2		ax-1	|- ( A e. RR+ -> ( A e. RR -> A e. RR+ ) )
3		eqid	|- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
4	3	ellogdm	|- ( A e. ( CC \ ( -oo (,] 0 ) ) <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )
5	1 2 4	sylanbrc	|- ( A e. RR+ -> A e. ( CC \ ( -oo (,] 0 ) ) )
6		dmlogdmgm	|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
7	5 6	syl	|- ( A e. RR+ -> A e. ( CC \ ( ZZ \ NN ) ) )