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 φK0
etransclem9.m φM
etransclem9.n φN
etransclem9.km φ¬KM
etransclem9.kn φKN
Assertion etransclem9 φM+N0

Proof

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