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 
|- ( ph -> K e. ZZ )
etransclem9.kn0 
|- ( ph -> K =/= 0 )
etransclem9.m 
|- ( ph -> M e. ZZ )
etransclem9.n 
|- ( ph -> N e. ZZ )
etransclem9.km 
|- ( ph -> -. K || M )
etransclem9.kn 
|- ( ph -> K || N )
Assertion etransclem9 
|- ( ph -> ( M + N ) =/= 0 )

Proof

Step Hyp Ref Expression
1 etransclem9.k 
 |-  ( ph -> K e. ZZ )
2 etransclem9.kn0 
 |-  ( ph -> K =/= 0 )
3 etransclem9.m 
 |-  ( ph -> M e. ZZ )
4 etransclem9.n 
 |-  ( ph -> N e. ZZ )
5 etransclem9.km 
 |-  ( ph -> -. K || M )
6 etransclem9.kn 
 |-  ( ph -> K || N )
7 dvdsval2 
 |-  ( ( K e. ZZ /\ K =/= 0 /\ M e. ZZ ) -> ( K || M <-> ( M / K ) e. ZZ ) )
8 1 2 3 7 syl3anc 
 |-  ( ph -> ( K || M <-> ( M / K ) e. ZZ ) )
9 5 8 mtbid 
 |-  ( ph -> -. ( M / K ) e. ZZ )
10 df-neg 
 |-  -u N = ( 0 - N )
11 10 a1i 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> -u 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 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> ( 0 - N ) = ( ( M + N ) - N ) )
15 3 zcnd 
 |-  ( ph -> M e. CC )
16 4 zcnd 
 |-  ( ph -> N e. CC )
17 15 16 pncand 
 |-  ( ph -> ( ( M + N ) - N ) = M )
18 17 adantr 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> ( ( M + N ) - N ) = M )
19 11 14 18 3eqtrrd 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> M = -u N )
20 19 oveq1d 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> ( M / K ) = ( -u N / K ) )
21 dvdsnegb 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K || N <-> K || -u N ) )
22 1 4 21 syl2anc 
 |-  ( ph -> ( K || N <-> K || -u N ) )
23 6 22 mpbid 
 |-  ( ph -> K || -u N )
24 4 znegcld 
 |-  ( ph -> -u N e. ZZ )
25 dvdsval2 
 |-  ( ( K e. ZZ /\ K =/= 0 /\ -u N e. ZZ ) -> ( K || -u N <-> ( -u N / K ) e. ZZ ) )
26 1 2 24 25 syl3anc 
 |-  ( ph -> ( K || -u N <-> ( -u N / K ) e. ZZ ) )
27 23 26 mpbid 
 |-  ( ph -> ( -u N / K ) e. ZZ )
28 27 adantr 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> ( -u N / K ) e. ZZ )
29 20 28 eqeltrd 
 |-  ( ( ph /\ ( M + N ) = 0 ) -> ( M / K ) e. ZZ )
30 9 29 mtand 
 |-  ( ph -> -. ( M + N ) = 0 )
31 30 neqned 
 |-  ( ph -> ( M + N ) =/= 0 )