Metamath Proof Explorer


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 φ K
etransclem9.kn0 φ K 0
etransclem9.m φ M
etransclem9.n φ N
etransclem9.km φ ¬ K M
etransclem9.kn φ K N
Assertion etransclem9 φ M + N 0

Proof

Step Hyp Ref Expression
1 etransclem9.k φ K
2 etransclem9.kn0 φ K 0
3 etransclem9.m φ M
4 etransclem9.n φ N
5 etransclem9.km φ ¬ K M
6 etransclem9.kn φ K N
7 dvdsval2 K K 0 M K M M K
8 1 2 3 7 syl3anc φ K M M K
9 5 8 mtbid φ ¬ M K
10 df-neg N = 0 N
11 10 a1i φ M + N = 0 N = 0 N
12 oveq1 M + N = 0 M + N - N = 0 N
13 12 eqcomd M + N = 0 0 N = M + N - N
14 13 adantl φ M + N = 0 0 N = M + N - N
15 3 zcnd φ M
16 4 zcnd φ N
17 15 16 pncand φ M + N - N = M
18 17 adantr φ M + N = 0 M + N - N = M
19 11 14 18 3eqtrrd φ M + N = 0 M = N
20 19 oveq1d φ M + N = 0 M K = N K
21 dvdsnegb K N K N K -N
22 1 4 21 syl2anc φ K N K -N
23 6 22 mpbid φ K -N
24 4 znegcld φ N
25 dvdsval2 K K 0 N K -N N K
26 1 2 24 25 syl3anc φ K -N N K
27 23 26 mpbid φ N K
28 27 adantr φ M + N = 0 N K
29 20 28 eqeltrd φ M + N = 0 M K
30 9 29 mtand φ ¬ M + N = 0
31 30 neqned φ M + N 0