This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsn1add

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

Ref Expression
Assertion dvdsn1add 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( -. K || M /\ K || N ) -> -. K || ( M + N ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
2 zaddcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
3 2 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
4 simp3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
5 1 3 4 3jca 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ ( M + N ) e. ZZ /\ N e. ZZ ) )
6 5 ad2antrr 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> ( K e. ZZ /\ ( M + N ) e. ZZ /\ N e. ZZ ) )
7 pm3.22 
 |-  ( ( K || N /\ K || ( M + N ) ) -> ( K || ( M + N ) /\ K || N ) )
8 7 adantll 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> ( K || ( M + N ) /\ K || N ) )
9 dvds2sub 
 |-  ( ( K e. ZZ /\ ( M + N ) e. ZZ /\ N e. ZZ ) -> ( ( K || ( M + N ) /\ K || N ) -> K || ( ( M + N ) - N ) ) )
10 6 8 9 sylc 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> K || ( ( M + N ) - N ) )
11 zcn 
 |-  ( M e. ZZ -> M e. CC )
12 11 3ad2ant2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. CC )
13 12 ad2antrr 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> M e. CC )
14 4 zcnd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N e. CC )
15 14 ad2antrr 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> N e. CC )
16 13 15 pncand 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> ( ( M + N ) - N ) = M )
17 10 16 breqtrd 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || N ) /\ K || ( M + N ) ) -> K || M )
18 17 adantlrl 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( -. K || M /\ K || N ) ) /\ K || ( M + N ) ) -> K || M )
19 simplrl 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( -. K || M /\ K || N ) ) /\ K || ( M + N ) ) -> -. K || M )
20 18 19 pm2.65da 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( -. K || M /\ K || N ) ) -> -. K || ( M + N ) )
21 20 ex 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( -. K || M /\ K || N ) -> -. K || ( M + N ) ) )