Theorem dmgmdivn0

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

	Ref	Expression
Hypotheses	dmgmn0.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
	dmgmdivn0.a	$$⊢\phi \to M\in \mathbb{N}$$
Assertion	dmgmdivn0	$$⊢\phi \to \left(\frac{A}{M}\right)+1\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
2		dmgmdivn0.a	$$⊢\phi \to M\in \mathbb{N}$$
3	1	eldifad	$$⊢\phi \to A\in ℂ$$
4	2	nncnd	$$⊢\phi \to M\in ℂ$$
5	2	nnne0d	$$⊢\phi \to M\ne 0$$
6	3 4 4 5	divdird	$$⊢\phi \to \frac{A+M}{M}=\left(\frac{A}{M}\right)+\left(\frac{M}{M}\right)$$
7	4 5	dividd	$$⊢\phi \to \frac{M}{M}=1$$
8	7	oveq2d	$$⊢\phi \to \left(\frac{A}{M}\right)+\left(\frac{M}{M}\right)=\left(\frac{A}{M}\right)+1$$
9	6 8	eqtrd	$$⊢\phi \to \frac{A+M}{M}=\left(\frac{A}{M}\right)+1$$
10	3 4	addcld	$$⊢\phi \to A+M\in ℂ$$
11	2	nnnn0d	$$⊢\phi \to M\in {\mathbb{N}}_0$$
12		dmgmaddn0	$$⊢\left(A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\wedge M\in {\mathbb{N}}_0\right)\to A+M\ne 0$$
13	1 11 12	syl2anc	$$⊢\phi \to A+M\ne 0$$
14	10 4 13 5	divne0d	$$⊢\phi \to \frac{A+M}{M}\ne 0$$
15	9 14	eqnetrrd	$$⊢\phi \to \left(\frac{A}{M}\right)+1\ne 0$$