dvdssqlem

		Ref	Expression
	Assertion	dvdssqlem	$⊢ (M \in ℕ \land N \in ℕ) \to (M ∥ N \leftrightarrow M^{2} ∥ N^{2})$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ M \in ℕ \to M \in ℤ$
2		nnz	$⊢ N \in ℕ \to N \in ℤ$
3		dvdssqim	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \to M^{2} ∥ N^{2})$
4	1 2 3	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to (M ∥ N \to M^{2} ∥ N^{2})$
5		sqgcd	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} = M^{2} \gcd N^{2}$
6	5	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to {(M \gcd N)}^{2} = M^{2} \gcd N^{2}$
7		nnsqcl	$⊢ M \in ℕ \to M^{2} \in ℕ$
8		nnsqcl	$⊢ N \in ℕ \to N^{2} \in ℕ$
9		gcdeq	$⊢ (M^{2} \in ℕ \land N^{2} \in ℕ) \to (M^{2} \gcd N^{2} = M^{2} \leftrightarrow M^{2} ∥ N^{2})$
10	7 8 9	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to (M^{2} \gcd N^{2} = M^{2} \leftrightarrow M^{2} ∥ N^{2})$
11	10	biimpar	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to M^{2} \gcd N^{2} = M^{2}$
12	6 11	eqtrd	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to {(M \gcd N)}^{2} = M^{2}$
13		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
14	1 2 13	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℕ_{0}$
15	14	nn0red	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℝ$
16	14	nn0ge0d	$⊢ (M \in ℕ \land N \in ℕ) \to 0 \leq M \gcd N$
17		nnre	$⊢ M \in ℕ \to M \in ℝ$
18	17	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℝ$
19		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
20	19	nn0ge0d	$⊢ M \in ℕ \to 0 \leq M$
21	20	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to 0 \leq M$
22		sq11	$⊢ ((M \gcd N \in ℝ \land 0 \leq M \gcd N) \land (M \in ℝ \land 0 \leq M)) \to ({(M \gcd N)}^{2} = M^{2} \leftrightarrow M \gcd N = M)$
23	15 16 18 21 22	syl22anc	$⊢ (M \in ℕ \land N \in ℕ) \to ({(M \gcd N)}^{2} = M^{2} \leftrightarrow M \gcd N = M)$
24	23	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to ({(M \gcd N)}^{2} = M^{2} \leftrightarrow M \gcd N = M)$
25	12 24	mpbid	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to M \gcd N = M$
26		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
27	1 2 26	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
28	27	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
29	28	simprd	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to (M \gcd N) ∥ N$
30	25 29	eqbrtrrd	$⊢ ((M \in ℕ \land N \in ℕ) \land M^{2} ∥ N^{2}) \to M ∥ N$
31	30	ex	$⊢ (M \in ℕ \land N \in ℕ) \to (M^{2} ∥ N^{2} \to M ∥ N)$
32	4 31	impbid	$⊢ (M \in ℕ \land N \in ℕ) \to (M ∥ N \leftrightarrow M^{2} ∥ N^{2})$

Metamath Proof Explorer

Theorem dvdssqlem

Proof