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	$$⊢\phi \to K\in \mathbb{Z}$$
	etransclem9.kn0	$$⊢\phi \to K\ne 0$$
	etransclem9.m	$$⊢\phi \to M\in \mathbb{Z}$$
	etransclem9.n	$$⊢\phi \to N\in \mathbb{Z}$$
	etransclem9.km	$$⊢\phi \to \neg K\parallel M$$
	etransclem9.kn	$$⊢\phi \to K\parallel N$$
Assertion	etransclem9	$$⊢\phi \to M+N\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		etransclem9.k	$$⊢\phi \to K\in \mathbb{Z}$$
2		etransclem9.kn0	$$⊢\phi \to K\ne 0$$
3		etransclem9.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		etransclem9.n	$$⊢\phi \to N\in \mathbb{Z}$$
5		etransclem9.km	$$⊢\phi \to \neg K\parallel M$$
6		etransclem9.kn	$$⊢\phi \to K\parallel N$$
7		dvdsval2	$$⊢\left(K\in \mathbb{Z}\wedge K\ne 0\wedge M\in \mathbb{Z}\right)\to \left(K\parallel M\leftrightarrow \frac{M}{K}\in \mathbb{Z}\right)$$
8	1 2 3 7	syl3anc	$$⊢\phi \to \left(K\parallel M\leftrightarrow \frac{M}{K}\in \mathbb{Z}\right)$$
9	5 8	mtbid	$$⊢\phi \to \neg \frac{M}{K}\in \mathbb{Z}$$
10		df-neg	$$⊢-N=0-N$$
11	10	a1i	$$⊢\left(\phi \wedge M+N=0\right)\to -N=0-N$$
12		oveq1	$$⊢M+N=0\to M+N-N=0-N$$
13	12	eqcomd	$$⊢M+N=0\to 0-N=M+N-N$$
14	13	adantl	$$⊢\left(\phi \wedge M+N=0\right)\to 0-N=M+N-N$$
15	3	zcnd	$$⊢\phi \to M\in ℂ$$
16	4	zcnd	$$⊢\phi \to N\in ℂ$$
17	15 16	pncand	$$⊢\phi \to M+N-N=M$$
18	17	adantr	$$⊢\left(\phi \wedge M+N=0\right)\to M+N-N=M$$
19	11 14 18	3eqtrrd	$$⊢\left(\phi \wedge M+N=0\right)\to M=-N$$
20	19	oveq1d	$$⊢\left(\phi \wedge M+N=0\right)\to \frac{M}{K}=\frac{-N}{K}$$
21		dvdsnegb	$$⊢\left(K\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(K\parallel N\leftrightarrow K\parallel \mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)$$
22	1 4 21	syl2anc	$$⊢\phi \to \left(K\parallel N\leftrightarrow K\parallel \mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)$$
23	6 22	mpbid	$$⊢\phi \to K\parallel \mathrm{-<mi\; mathcolor="\#808">N</mi>}$$
24	4	znegcld	$$⊢\phi \to -N\in \mathbb{Z}$$
25		dvdsval2	$$⊢\left(K\in \mathbb{Z}\wedge K\ne 0\wedge -N\in \mathbb{Z}\right)\to \left(K\parallel \mathrm{-<mi\; mathcolor="\#808">N</mi>}\leftrightarrow \frac{-N}{K}\in \mathbb{Z}\right)$$
26	1 2 24 25	syl3anc	$$⊢\phi \to \left(K\parallel \mathrm{-<mi\; mathcolor="\#808">N</mi>}\leftrightarrow \frac{-N}{K}\in \mathbb{Z}\right)$$
27	23 26	mpbid	$$⊢\phi \to \frac{-N}{K}\in \mathbb{Z}$$
28	27	adantr	$$⊢\left(\phi \wedge M+N=0\right)\to \frac{-N}{K}\in \mathbb{Z}$$
29	20 28	eqeltrd	$$⊢\left(\phi \wedge M+N=0\right)\to \frac{M}{K}\in \mathbb{Z}$$
30	9 29	mtand	$$⊢\phi \to \neg M+N=0$$
31	30	neqned	$$⊢\phi \to M+N\ne 0$$