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	$$⊢\phi \to M\in \mathbb{P}$$
	nzprmdif.n	$$⊢\phi \to N\in \mathbb{P}$$
	nzprmdif.ne	$$⊢\phi \to M\ne N$$
Assertion	nzprmdif	$$⊢\phi \to \parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{N\right\}\right]=\parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		nzprmdif.m	$$⊢\phi \to M\in \mathbb{P}$$
2		nzprmdif.n	$$⊢\phi \to N\in \mathbb{P}$$
3		nzprmdif.ne	$$⊢\phi \to M\ne N$$
4		difin	$$⊢\parallel \left[\left\{M\right\}\right]\setminus \left(\parallel \left[\left\{M\right\}\right]\cap \parallel \left[\left\{N\right\}\right]\right)=\parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{N\right\}\right]$$
5		prmz	$$⊢M\in \mathbb{P}\to M\in \mathbb{Z}$$
6	1 5	syl	$$⊢\phi \to M\in \mathbb{Z}$$
7		prmz	$$⊢N\in \mathbb{P}\to N\in \mathbb{Z}$$
8	2 7	syl	$$⊢\phi \to N\in \mathbb{Z}$$
9	6 8	nzin	$$⊢\phi \to \parallel \left[\left\{M\right\}\right]\cap \parallel \left[\left\{N\right\}\right]=\parallel \left[\left\{M\mathrm{lcm}N\right\}\right]$$
10	9	difeq2d	$$⊢\phi \to \parallel \left[\left\{M\right\}\right]\setminus \left(\parallel \left[\left\{M\right\}\right]\cap \parallel \left[\left\{N\right\}\right]\right)=\parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{M\mathrm{lcm}N\right\}\right]$$
11	4 10	eqtr3id	$$⊢\phi \to \parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{N\right\}\right]=\parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{M\mathrm{lcm}N\right\}\right]$$
12		lcmgcd	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M\mathrm{lcm}N\right)\left(M\gcd N\right)=\left|\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|$$
13	6 8 12	syl2anc	$$⊢\phi \to \left(M\mathrm{lcm}N\right)\left(M\gcd N\right)=\left|\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|$$
14		prmrp	$$⊢\left(M\in \mathbb{P}\wedge N\in \mathbb{P}\right)\to \left(M\gcd N=1\leftrightarrow M\ne N\right)$$
15	1 2 14	syl2anc	$$⊢\phi \to \left(M\gcd N=1\leftrightarrow M\ne N\right)$$
16	3 15	mpbird	$$⊢\phi \to M\gcd N=1$$
17	16	oveq2d	$$⊢\phi \to \left(M\mathrm{lcm}N\right)\left(M\gcd N\right)=\left(M\mathrm{lcm}N\right)\cdot 1$$
18		lcmcl	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\mathrm{lcm}N\in {\mathbb{N}}_0$$
19	6 8 18	syl2anc	$$⊢\phi \to M\mathrm{lcm}N\in {\mathbb{N}}_0$$
20	19	nn0cnd	$$⊢\phi \to M\mathrm{lcm}N\in ℂ$$
21	20	mulid1d	$$⊢\phi \to \left(M\mathrm{lcm}N\right)\cdot 1=M\mathrm{lcm}N$$
22	17 21	eqtrd	$$⊢\phi \to \left(M\mathrm{lcm}N\right)\left(M\gcd N\right)=M\mathrm{lcm}N$$
23	6	zred	$$⊢\phi \to M\in ℝ$$
24	8	zred	$$⊢\phi \to N\in ℝ$$
25	23 24	remulcld	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
26		prmnn	$$⊢M\in \mathbb{P}\to M\in \mathbb{N}$$
27	1 26	syl	$$⊢\phi \to M\in \mathbb{N}$$
28	27	nnnn0d	$$⊢\phi \to M\in {\mathbb{N}}_0$$
29	28	nn0ge0d	$$⊢\phi \to 0\le M$$
30		prmnn	$$⊢N\in \mathbb{P}\to N\in \mathbb{N}$$
31	2 30	syl	$$⊢\phi \to N\in \mathbb{N}$$
32	31	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
33	32	nn0ge0d	$$⊢\phi \to 0\le N$$
34	23 24 29 33	mulge0d	$$⊢\phi \to 0\le \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
35	25 34	absidd	$$⊢\phi \to \left|\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
36	13 22 35	3eqtr3d	$$⊢\phi \to M\mathrm{lcm}N=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
37	36	sneqd	$$⊢\phi \to \left\{M\mathrm{lcm}N\right\}=\left\{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right\}$$
38	37	imaeq2d	$$⊢\phi \to \parallel \left[\left\{M\mathrm{lcm}N\right\}\right]=\parallel \left[\left\{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right\}\right]$$
39	38	difeq2d	$$⊢\phi \to \parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{M\mathrm{lcm}N\right\}\right]=\parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right\}\right]$$
40	11 39	eqtrd	$$⊢\phi \to \parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{N\right\}\right]=\parallel \left[\left\{M\right\}\right]\setminus \parallel \left[\left\{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right\}\right]$$