Metamath Proof Explorer


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 ) ) )