| Step |
Hyp |
Ref |
Expression |
| 1 |
|
divides |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. k e. ZZ ( k x. M ) = N ) ) |
| 2 |
|
zsqcl |
|- ( k e. ZZ -> ( k ^ 2 ) e. ZZ ) |
| 3 |
|
zsqcl |
|- ( M e. ZZ -> ( M ^ 2 ) e. ZZ ) |
| 4 |
|
dvdsmul2 |
|- ( ( ( k ^ 2 ) e. ZZ /\ ( M ^ 2 ) e. ZZ ) -> ( M ^ 2 ) || ( ( k ^ 2 ) x. ( M ^ 2 ) ) ) |
| 5 |
2 3 4
|
syl2anr |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( M ^ 2 ) || ( ( k ^ 2 ) x. ( M ^ 2 ) ) ) |
| 6 |
|
zcn |
|- ( k e. ZZ -> k e. CC ) |
| 7 |
|
zcn |
|- ( M e. ZZ -> M e. CC ) |
| 8 |
|
sqmul |
|- ( ( k e. CC /\ M e. CC ) -> ( ( k x. M ) ^ 2 ) = ( ( k ^ 2 ) x. ( M ^ 2 ) ) ) |
| 9 |
6 7 8
|
syl2anr |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( ( k x. M ) ^ 2 ) = ( ( k ^ 2 ) x. ( M ^ 2 ) ) ) |
| 10 |
5 9
|
breqtrrd |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( M ^ 2 ) || ( ( k x. M ) ^ 2 ) ) |
| 11 |
|
oveq1 |
|- ( ( k x. M ) = N -> ( ( k x. M ) ^ 2 ) = ( N ^ 2 ) ) |
| 12 |
11
|
breq2d |
|- ( ( k x. M ) = N -> ( ( M ^ 2 ) || ( ( k x. M ) ^ 2 ) <-> ( M ^ 2 ) || ( N ^ 2 ) ) ) |
| 13 |
10 12
|
syl5ibcom |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( ( k x. M ) = N -> ( M ^ 2 ) || ( N ^ 2 ) ) ) |
| 14 |
13
|
rexlimdva |
|- ( M e. ZZ -> ( E. k e. ZZ ( k x. M ) = N -> ( M ^ 2 ) || ( N ^ 2 ) ) ) |
| 15 |
14
|
adantr |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( E. k e. ZZ ( k x. M ) = N -> ( M ^ 2 ) || ( N ^ 2 ) ) ) |
| 16 |
1 15
|
sylbid |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( M ^ 2 ) || ( N ^ 2 ) ) ) |