Metamath Proof Explorer


Theorem nzprmdif

Description: Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypotheses nzprmdif.m φ M
nzprmdif.n φ N
nzprmdif.ne φ M N
Assertion nzprmdif φ M N = M M N

Proof

Step Hyp Ref Expression
1 nzprmdif.m φ M
2 nzprmdif.n φ N
3 nzprmdif.ne φ M N
4 difin M M N = M N
5 prmz M M
6 1 5 syl φ M
7 prmz N N
8 2 7 syl φ N
9 6 8 nzin φ M N = M lcm N
10 9 difeq2d φ M M N = M M lcm N
11 4 10 eqtr3id φ M N = M M lcm N
12 lcmgcd M N M lcm N M gcd N = M N
13 6 8 12 syl2anc φ M lcm N M gcd N = M N
14 prmrp M N M gcd N = 1 M N
15 1 2 14 syl2anc φ M gcd N = 1 M N
16 3 15 mpbird φ M gcd N = 1
17 16 oveq2d φ M lcm N M gcd N = M lcm N 1
18 lcmcl M N M lcm N 0
19 6 8 18 syl2anc φ M lcm N 0
20 19 nn0cnd φ M lcm N
21 20 mulid1d φ M lcm N 1 = M lcm N
22 17 21 eqtrd φ M lcm N M gcd N = M lcm N
23 6 zred φ M
24 8 zred φ N
25 23 24 remulcld φ M N
26 prmnn M M
27 1 26 syl φ M
28 27 nnnn0d φ M 0
29 28 nn0ge0d φ 0 M
30 prmnn N N
31 2 30 syl φ N
32 31 nnnn0d φ N 0
33 32 nn0ge0d φ 0 N
34 23 24 29 33 mulge0d φ 0 M N
35 25 34 absidd φ M N = M N
36 13 22 35 3eqtr3d φ M lcm N = M N
37 36 sneqd φ M lcm N = M N
38 37 imaeq2d φ M lcm N = M N
39 38 difeq2d φ M M lcm N = M M N
40 11 39 eqtrd φ M N = M M N