Theorem dmgmdivn0

Description: Lemma for lgamf . (Contributed by Mario Carneiro, 3-Jul-2017)

	Ref	Expression
Hypotheses	dmgmn0.a	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
	dmgmdivn0.a	|- ( ph -> M e. NN )
Assertion	dmgmdivn0	|- ( ph -> ( ( A / M ) + 1 ) =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
2		dmgmdivn0.a	|- ( ph -> M e. NN )
3	1	eldifad	|- ( ph -> A e. CC )
4	2	nncnd	|- ( ph -> M e. CC )
5	2	nnne0d	|- ( ph -> M =/= 0 )
6	3 4 4 5	divdird	|- ( ph -> ( ( A + M ) / M ) = ( ( A / M ) + ( M / M ) ) )
7	4 5	dividd	|- ( ph -> ( M / M ) = 1 )
8	7	oveq2d	|- ( ph -> ( ( A / M ) + ( M / M ) ) = ( ( A / M ) + 1 ) )
9	6 8	eqtrd	|- ( ph -> ( ( A + M ) / M ) = ( ( A / M ) + 1 ) )
10	3 4	addcld	|- ( ph -> ( A + M ) e. CC )
11	2	nnnn0d	|- ( ph -> M e. NN0 )
12		dmgmaddn0	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ M e. NN0 ) -> ( A + M ) =/= 0 )
13	1 11 12	syl2anc	|- ( ph -> ( A + M ) =/= 0 )
14	10 4 13 5	divne0d	|- ( ph -> ( ( A + M ) / M ) =/= 0 )
15	9 14	eqnetrrd	|- ( ph -> ( ( A / M ) + 1 ) =/= 0 )