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

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 ) ) )