Theorem dvdssqim

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

	Ref	Expression
Assertion	dvdssqim	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		divides	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 ) )
2		zsqcl	⊢ ( 𝑘 ∈ ℤ → ( 𝑘 ↑ 2 ) ∈ ℤ )
3		zsqcl	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ↑ 2 ) ∈ ℤ )
4		dvdsmul2	⊢ ( ( ( 𝑘 ↑ 2 ) ∈ ℤ ∧ ( 𝑀 ↑ 2 ) ∈ ℤ ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝑘 ↑ 2 ) · ( 𝑀 ↑ 2 ) ) )
5	2 3 4	syl2anr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝑘 ↑ 2 ) · ( 𝑀 ↑ 2 ) ) )
6		zcn	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
7		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8		sqmul	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑘 · 𝑀 ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( 𝑀 ↑ 2 ) ) )
9	6 7 8	syl2anr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · 𝑀 ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( 𝑀 ↑ 2 ) ) )
10	5 9	breqtrrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝑘 · 𝑀 ) ↑ 2 ) )
11		oveq1	⊢ ( ( 𝑘 · 𝑀 ) = 𝑁 → ( ( 𝑘 · 𝑀 ) ↑ 2 ) = ( 𝑁 ↑ 2 ) )
12	11	breq2d	⊢ ( ( 𝑘 · 𝑀 ) = 𝑁 → ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝑘 · 𝑀 ) ↑ 2 ) ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
13	10 12	syl5ibcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · 𝑀 ) = 𝑁 → ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
14	13	rexlimdva	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 → ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
15	14	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 → ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
16	1 15	sylbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )