Theorem etransclem9

Description: If K divides N but K does not divide M then M + N cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem9.k	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	etransclem9.kn0	⊢ ( 𝜑 → 𝐾 ≠ 0 )
	etransclem9.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	etransclem9.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	etransclem9.km	⊢ ( 𝜑 → ¬ 𝐾 ∥ 𝑀 )
	etransclem9.kn	⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )
Assertion	etransclem9	⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		etransclem9.k	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2		etransclem9.kn0	⊢ ( 𝜑 → 𝐾 ≠ 0 )
3		etransclem9.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		etransclem9.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		etransclem9.km	⊢ ( 𝜑 → ¬ 𝐾 ∥ 𝑀 )
6		etransclem9.kn	⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )
7		dvdsval2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ∥ 𝑀 ↔ ( 𝑀 / 𝐾 ) ∈ ℤ ) )
8	1 2 3 7	syl3anc	⊢ ( 𝜑 → ( 𝐾 ∥ 𝑀 ↔ ( 𝑀 / 𝐾 ) ∈ ℤ ) )
9	5 8	mtbid	⊢ ( 𝜑 → ¬ ( 𝑀 / 𝐾 ) ∈ ℤ )
10		df-neg	⊢ - 𝑁 = ( 0 − 𝑁 )
11	10	a1i	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → - 𝑁 = ( 0 − 𝑁 ) )
12		oveq1	⊢ ( ( 𝑀 + 𝑁 ) = 0 → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = ( 0 − 𝑁 ) )
13	12	eqcomd	⊢ ( ( 𝑀 + 𝑁 ) = 0 → ( 0 − 𝑁 ) = ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( 0 − 𝑁 ) = ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
15	3	zcnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
16	4	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
17	15 16	pncand	⊢ ( 𝜑 → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
19	11 14 18	3eqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → 𝑀 = - 𝑁 )
20	19	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( 𝑀 / 𝐾 ) = ( - 𝑁 / 𝐾 ) )
21		dvdsnegb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 ↔ 𝐾 ∥ - 𝑁 ) )
22	1 4 21	syl2anc	⊢ ( 𝜑 → ( 𝐾 ∥ 𝑁 ↔ 𝐾 ∥ - 𝑁 ) )
23	6 22	mpbid	⊢ ( 𝜑 → 𝐾 ∥ - 𝑁 )
24	4	znegcld	⊢ ( 𝜑 → - 𝑁 ∈ ℤ )
25		dvdsval2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐾 ∥ - 𝑁 ↔ ( - 𝑁 / 𝐾 ) ∈ ℤ ) )
26	1 2 24 25	syl3anc	⊢ ( 𝜑 → ( 𝐾 ∥ - 𝑁 ↔ ( - 𝑁 / 𝐾 ) ∈ ℤ ) )
27	23 26	mpbid	⊢ ( 𝜑 → ( - 𝑁 / 𝐾 ) ∈ ℤ )
28	27	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( - 𝑁 / 𝐾 ) ∈ ℤ )
29	20 28	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( 𝑀 / 𝐾 ) ∈ ℤ )
30	9 29	mtand	⊢ ( 𝜑 → ¬ ( 𝑀 + 𝑁 ) = 0 )
31	30	neqned	⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ≠ 0 )