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	⊢ ( 𝜑 → 𝑀 ∈ ℙ )
	nzprmdif.n	⊢ ( 𝜑 → 𝑁 ∈ ℙ )
	nzprmdif.ne	⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
Assertion	nzprmdif	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { 𝑁 } ) ) = ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { ( 𝑀 · 𝑁 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		nzprmdif.m	⊢ ( 𝜑 → 𝑀 ∈ ℙ )
2		nzprmdif.n	⊢ ( 𝜑 → 𝑁 ∈ ℙ )
3		nzprmdif.ne	⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
4		difin	⊢ ( ( ∥ “ { 𝑀 } ) ∖ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) ) = ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { 𝑁 } ) )
5		prmz	⊢ ( 𝑀 ∈ ℙ → 𝑀 ∈ ℤ )
6	1 5	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		prmz	⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℤ )
8	2 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9	6 8	nzin	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) = ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) )
10	9	difeq2d	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∖ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) ) = ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ) )
11	4 10	eqtr3id	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { 𝑁 } ) ) = ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ) )
12		lcmgcd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( abs ‘ ( 𝑀 · 𝑁 ) ) )
13	6 8 12	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( abs ‘ ( 𝑀 · 𝑁 ) ) )
14		prmrp	⊢ ( ( 𝑀 ∈ ℙ ∧ 𝑁 ∈ ℙ ) → ( ( 𝑀 gcd 𝑁 ) = 1 ↔ 𝑀 ≠ 𝑁 ) )
15	1 2 14	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 gcd 𝑁 ) = 1 ↔ 𝑀 ≠ 𝑁 ) )
16	3 15	mpbird	⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
17	16	oveq2d	⊢ ( 𝜑 → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( ( 𝑀 lcm 𝑁 ) · 1 ) )
18		lcmcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
19	6 8 18	syl2anc	⊢ ( 𝜑 → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
20	19	nn0cnd	⊢ ( 𝜑 → ( 𝑀 lcm 𝑁 ) ∈ ℂ )
21	20	mulridd	⊢ ( 𝜑 → ( ( 𝑀 lcm 𝑁 ) · 1 ) = ( 𝑀 lcm 𝑁 ) )
22	17 21	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 lcm 𝑁 ) )
23	6	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
24	8	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
25	23 24	remulcld	⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℝ )
26		prmnn	⊢ ( 𝑀 ∈ ℙ → 𝑀 ∈ ℕ )
27	1 26	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
28	27	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
29	28	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝑀 )
30		prmnn	⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ )
31	2 30	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
32	31	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
33	32	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝑁 )
34	23 24 29 33	mulge0d	⊢ ( 𝜑 → 0 ≤ ( 𝑀 · 𝑁 ) )
35	25 34	absidd	⊢ ( 𝜑 → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( 𝑀 · 𝑁 ) )
36	13 22 35	3eqtr3d	⊢ ( 𝜑 → ( 𝑀 lcm 𝑁 ) = ( 𝑀 · 𝑁 ) )
37	36	sneqd	⊢ ( 𝜑 → { ( 𝑀 lcm 𝑁 ) } = { ( 𝑀 · 𝑁 ) } )
38	37	imaeq2d	⊢ ( 𝜑 → ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) = ( ∥ “ { ( 𝑀 · 𝑁 ) } ) )
39	38	difeq2d	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ) = ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { ( 𝑀 · 𝑁 ) } ) ) )
40	11 39	eqtrd	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { 𝑁 } ) ) = ( ( ∥ “ { 𝑀 } ) ∖ ( ∥ “ { ( 𝑀 · 𝑁 ) } ) ) )