dvdssqim

Description: Unidirectional form of dvdssq . (Contributed by Scott Fenton, 19-Apr-2014)

		Ref	Expression
	Assertion	dvdssqim	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \to M^{2} ∥ N^{2})$

Step	Hyp	Ref	Expression
1		divides	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \exists k \in ℤ k \cdot M = N)$
2		zsqcl	$⊢ k \in ℤ \to k^{2} \in ℤ$
3		zsqcl	$⊢ M \in ℤ \to M^{2} \in ℤ$
4		dvdsmul2	$⊢ (k^{2} \in ℤ \land M^{2} \in ℤ) \to M^{2} ∥ k^{2} M^{2}$
5	2 3 4	syl2anr	$⊢ (M \in ℤ \land k \in ℤ) \to M^{2} ∥ k^{2} M^{2}$
6		zcn	$⊢ k \in ℤ \to k \in ℂ$
7		zcn	$⊢ M \in ℤ \to M \in ℂ$
8		sqmul	$⊢ (k \in ℂ \land M \in ℂ) \to {k \cdot M}^{2} = k^{2} M^{2}$
9	6 7 8	syl2anr	$⊢ (M \in ℤ \land k \in ℤ) \to {k \cdot M}^{2} = k^{2} M^{2}$
10	5 9	breqtrrd	$⊢ (M \in ℤ \land k \in ℤ) \to M^{2} ∥ {k \cdot M}^{2}$
11		oveq1	$⊢ k \cdot M = N \to {k \cdot M}^{2} = N^{2}$
12	11	breq2d	$⊢ k \cdot M = N \to (M^{2} ∥ {k \cdot M}^{2} \leftrightarrow M^{2} ∥ N^{2})$
13	10 12	syl5ibcom	$⊢ (M \in ℤ \land k \in ℤ) \to (k \cdot M = N \to M^{2} ∥ N^{2})$
14	13	rexlimdva	$⊢ M \in ℤ \to (\exists k \in ℤ k \cdot M = N \to M^{2} ∥ N^{2})$
15	14	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to (\exists k \in ℤ k \cdot M = N \to M^{2} ∥ N^{2})$
16	1 15	sylbid	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \to M^{2} ∥ N^{2})$

Metamath Proof Explorer