Metamath Proof Explorer


Theorem dvds2add

Description: If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 3simpa
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ M e. ZZ ) )
2 3simpb
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ N e. ZZ ) )
3 zaddcl
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
4 3 anim2i
 |-  ( ( K e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( K e. ZZ /\ ( M + N ) e. ZZ ) )
5 4 3impb
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ ( M + N ) e. ZZ ) )
6 zaddcl
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
7 6 adantl
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x + y ) e. ZZ )
8 zcn
 |-  ( x e. ZZ -> x e. CC )
9 zcn
 |-  ( y e. ZZ -> y e. CC )
10 zcn
 |-  ( K e. ZZ -> K e. CC )
11 adddir
 |-  ( ( x e. CC /\ y e. CC /\ K e. CC ) -> ( ( x + y ) x. K ) = ( ( x x. K ) + ( y x. K ) ) )
12 8 9 10 11 syl3an
 |-  ( ( x e. ZZ /\ y e. ZZ /\ K e. ZZ ) -> ( ( x + y ) x. K ) = ( ( x x. K ) + ( y x. K ) ) )
13 12 3comr
 |-  ( ( K e. ZZ /\ x e. ZZ /\ y e. ZZ ) -> ( ( x + y ) x. K ) = ( ( x x. K ) + ( y x. K ) ) )
14 13 3expb
 |-  ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x + y ) x. K ) = ( ( x x. K ) + ( y x. K ) ) )
15 oveq12
 |-  ( ( ( x x. K ) = M /\ ( y x. K ) = N ) -> ( ( x x. K ) + ( y x. K ) ) = ( M + N ) )
16 14 15 sylan9eq
 |-  ( ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( ( x x. K ) = M /\ ( y x. K ) = N ) ) -> ( ( x + y ) x. K ) = ( M + N ) )
17 16 ex
 |-  ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. K ) = M /\ ( y x. K ) = N ) -> ( ( x + y ) x. K ) = ( M + N ) ) )
18 17 3ad2antl1
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. K ) = M /\ ( y x. K ) = N ) -> ( ( x + y ) x. K ) = ( M + N ) ) )
19 1 2 5 7 18 dvds2lem
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M + N ) ) )