This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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