Theorem dmgmdivn0

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

	Ref	Expression
Hypotheses	dmgmn0.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
	dmgmdivn0.a	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
Assertion	dmgmdivn0	⊢ ( 𝜑 → ( ( 𝐴 / 𝑀 ) + 1 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
2		dmgmdivn0.a	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3	1	eldifad	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4	2	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
5	2	nnne0d	⊢ ( 𝜑 → 𝑀 ≠ 0 )
6	3 4 4 5	divdird	⊢ ( 𝜑 → ( ( 𝐴 + 𝑀 ) / 𝑀 ) = ( ( 𝐴 / 𝑀 ) + ( 𝑀 / 𝑀 ) ) )
7	4 5	dividd	⊢ ( 𝜑 → ( 𝑀 / 𝑀 ) = 1 )
8	7	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 / 𝑀 ) + ( 𝑀 / 𝑀 ) ) = ( ( 𝐴 / 𝑀 ) + 1 ) )
9	6 8	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 + 𝑀 ) / 𝑀 ) = ( ( 𝐴 / 𝑀 ) + 1 ) )
10	3 4	addcld	⊢ ( 𝜑 → ( 𝐴 + 𝑀 ) ∈ ℂ )
11	2	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
12		dmgmaddn0	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 + 𝑀 ) ≠ 0 )
13	1 11 12	syl2anc	⊢ ( 𝜑 → ( 𝐴 + 𝑀 ) ≠ 0 )
14	10 4 13 5	divne0d	⊢ ( 𝜑 → ( ( 𝐴 + 𝑀 ) / 𝑀 ) ≠ 0 )
15	9 14	eqnetrrd	⊢ ( 𝜑 → ( ( 𝐴 / 𝑀 ) + 1 ) ≠ 0 )