Metamath Proof Explorer


Theorem coprmdvds2d

Description: If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses coprmdvds2d.1
|- ( ph -> K e. ZZ )
coprmdvds2d.2
|- ( ph -> M e. ZZ )
coprmdvds2d.3
|- ( ph -> N e. ZZ )
coprmdvds2d.4
|- ( ph -> ( K gcd M ) = 1 )
coprmdvds2d.5
|- ( ph -> K || N )
coprmdvds2d.6
|- ( ph -> M || N )
Assertion coprmdvds2d
|- ( ph -> ( K x. M ) || N )

Proof

Step Hyp Ref Expression
1 coprmdvds2d.1
 |-  ( ph -> K e. ZZ )
2 coprmdvds2d.2
 |-  ( ph -> M e. ZZ )
3 coprmdvds2d.3
 |-  ( ph -> N e. ZZ )
4 coprmdvds2d.4
 |-  ( ph -> ( K gcd M ) = 1 )
5 coprmdvds2d.5
 |-  ( ph -> K || N )
6 coprmdvds2d.6
 |-  ( ph -> M || N )
7 1 2 3 3jca
 |-  ( ph -> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
8 7 4 jca
 |-  ( ph -> ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) )
9 coprmdvds2
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( ( K || N /\ M || N ) -> ( K x. M ) || N ) )
10 8 9 syl
 |-  ( ph -> ( ( K || N /\ M || N ) -> ( K x. M ) || N ) )
11 5 6 10 mp2and
 |-  ( ph -> ( K x. M ) || N )