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 e. ( CC \ ( -oo (,] 0 ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldifi	|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> A e. CC )
2		simpr	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> -u A e. NN0 )
3	2	nn0ge0d	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> 0 <_ -u A )
4	1	adantr	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> A e. CC )
5	2	nn0red	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> -u A e. RR )
6	4 5	negrebd	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> A e. RR )
7		eqid	|- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
8	7	ellogdm	|- ( A e. ( CC \ ( -oo (,] 0 ) ) <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )
9	8	simprbi	|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( A e. RR -> A e. RR+ ) )
10	9	imp	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ A e. RR ) -> A e. RR+ )
11	6 10	syldan	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> A e. RR+ )
12	11	rpgt0d	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> 0 < A )
13	6	lt0neg2d	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> ( 0 < A <-> -u A < 0 ) )
14	12 13	mpbid	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> -u A < 0 )
15		0red	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> 0 e. RR )
16	5 15	ltnled	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> ( -u A < 0 <-> -. 0 <_ -u A ) )
17	14 16	mpbid	|- ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ -u A e. NN0 ) -> -. 0 <_ -u A )
18	3 17	pm2.65da	|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> -. -u A e. NN0 )
19		eldmgm	|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) )
20	1 18 19	sylanbrc	|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )