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 
|- ( ph -> M e. Prime )
nzprmdif.n 
|- ( ph -> N e. Prime )
nzprmdif.ne 
|- ( ph -> M =/= N )
Assertion nzprmdif 
|- ( ph -> ( ( || " { M } ) \ ( || " { N } ) ) = ( ( || " { M } ) \ ( || " { ( M x. N ) } ) ) )

Proof

Step Hyp Ref Expression
1 nzprmdif.m 
 |-  ( ph -> M e. Prime )
2 nzprmdif.n 
 |-  ( ph -> N e. Prime )
3 nzprmdif.ne 
 |-  ( ph -> M =/= N )
4 difin 
 |-  ( ( || " { M } ) \ ( ( || " { M } ) i^i ( || " { N } ) ) ) = ( ( || " { M } ) \ ( || " { N } ) )
5 prmz 
 |-  ( M e. Prime -> M e. ZZ )
6 1 5 syl 
 |-  ( ph -> M e. ZZ )
7 prmz 
 |-  ( N e. Prime -> N e. ZZ )
8 2 7 syl 
 |-  ( ph -> N e. ZZ )
9 6 8 nzin 
 |-  ( ph -> ( ( || " { M } ) i^i ( || " { N } ) ) = ( || " { ( M lcm N ) } ) )
10 9 difeq2d 
 |-  ( ph -> ( ( || " { M } ) \ ( ( || " { M } ) i^i ( || " { N } ) ) ) = ( ( || " { M } ) \ ( || " { ( M lcm N ) } ) ) )
11 4 10 eqtr3id 
 |-  ( ph -> ( ( || " { M } ) \ ( || " { N } ) ) = ( ( || " { M } ) \ ( || " { ( M lcm N ) } ) ) )
12 lcmgcd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) )
13 6 8 12 syl2anc 
 |-  ( ph -> ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) )
14 prmrp 
 |-  ( ( M e. Prime /\ N e. Prime ) -> ( ( M gcd N ) = 1 <-> M =/= N ) )
15 1 2 14 syl2anc 
 |-  ( ph -> ( ( M gcd N ) = 1 <-> M =/= N ) )
16 3 15 mpbird 
 |-  ( ph -> ( M gcd N ) = 1 )
17 16 oveq2d 
 |-  ( ph -> ( ( M lcm N ) x. ( M gcd N ) ) = ( ( M lcm N ) x. 1 ) )
18 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
19 6 8 18 syl2anc 
 |-  ( ph -> ( M lcm N ) e. NN0 )
20 19 nn0cnd 
 |-  ( ph -> ( M lcm N ) e. CC )
21 20 mulid1d 
 |-  ( ph -> ( ( M lcm N ) x. 1 ) = ( M lcm N ) )
22 17 21 eqtrd 
 |-  ( ph -> ( ( M lcm N ) x. ( M gcd N ) ) = ( M lcm N ) )
23 6 zred 
 |-  ( ph -> M e. RR )
24 8 zred 
 |-  ( ph -> N e. RR )
25 23 24 remulcld 
 |-  ( ph -> ( M x. N ) e. RR )
26 prmnn 
 |-  ( M e. Prime -> M e. NN )
27 1 26 syl 
 |-  ( ph -> M e. NN )
28 27 nnnn0d 
 |-  ( ph -> M e. NN0 )
29 28 nn0ge0d 
 |-  ( ph -> 0 <_ M )
30 prmnn 
 |-  ( N e. Prime -> N e. NN )
31 2 30 syl 
 |-  ( ph -> N e. NN )
32 31 nnnn0d 
 |-  ( ph -> N e. NN0 )
33 32 nn0ge0d 
 |-  ( ph -> 0 <_ N )
34 23 24 29 33 mulge0d 
 |-  ( ph -> 0 <_ ( M x. N ) )
35 25 34 absidd 
 |-  ( ph -> ( abs ` ( M x. N ) ) = ( M x. N ) )
36 13 22 35 3eqtr3d 
 |-  ( ph -> ( M lcm N ) = ( M x. N ) )
37 36 sneqd 
 |-  ( ph -> { ( M lcm N ) } = { ( M x. N ) } )
38 37 imaeq2d 
 |-  ( ph -> ( || " { ( M lcm N ) } ) = ( || " { ( M x. N ) } ) )
39 38 difeq2d 
 |-  ( ph -> ( ( || " { M } ) \ ( || " { ( M lcm N ) } ) ) = ( ( || " { M } ) \ ( || " { ( M x. N ) } ) ) )
40 11 39 eqtrd 
 |-  ( ph -> ( ( || " { M } ) \ ( || " { N } ) ) = ( ( || " { M } ) \ ( || " { ( M x. N ) } ) ) )