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 φ K
coprmdvds2d.2 φ M
coprmdvds2d.3 φ N
coprmdvds2d.4 φ K gcd M = 1
coprmdvds2d.5 φ K N
coprmdvds2d.6 φ M N
Assertion coprmdvds2d φ K M N

Proof

Step Hyp Ref Expression
1 coprmdvds2d.1 φ K
2 coprmdvds2d.2 φ M
3 coprmdvds2d.3 φ N
4 coprmdvds2d.4 φ K gcd M = 1
5 coprmdvds2d.5 φ K N
6 coprmdvds2d.6 φ M N
7 1 2 3 3jca φ K M N
8 7 4 jca φ K M N K gcd M = 1
9 coprmdvds2 K M N K gcd M = 1 K N M N K M N
10 8 9 syl φ K N M N K M N
11 5 6 10 mp2and φ K M N