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