| Step |
Hyp |
Ref |
Expression |
| 1 |
|
4sqlem5.2 |
|- ( ph -> A e. ZZ ) |
| 2 |
|
4sqlem5.3 |
|- ( ph -> M e. NN ) |
| 3 |
|
4sqlem5.4 |
|- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) |
| 4 |
2
|
nnzd |
|- ( ph -> M e. ZZ ) |
| 5 |
1 2 3
|
4sqlem5 |
|- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) ) |
| 6 |
5
|
simpld |
|- ( ph -> B e. ZZ ) |
| 7 |
1 6
|
zsubcld |
|- ( ph -> ( A - B ) e. ZZ ) |
| 8 |
|
zsqcl |
|- ( A e. ZZ -> ( A ^ 2 ) e. ZZ ) |
| 9 |
1 8
|
syl |
|- ( ph -> ( A ^ 2 ) e. ZZ ) |
| 10 |
|
zsqcl |
|- ( B e. ZZ -> ( B ^ 2 ) e. ZZ ) |
| 11 |
6 10
|
syl |
|- ( ph -> ( B ^ 2 ) e. ZZ ) |
| 12 |
9 11
|
zsubcld |
|- ( ph -> ( ( A ^ 2 ) - ( B ^ 2 ) ) e. ZZ ) |
| 13 |
5
|
simprd |
|- ( ph -> ( ( A - B ) / M ) e. ZZ ) |
| 14 |
2
|
nnne0d |
|- ( ph -> M =/= 0 ) |
| 15 |
|
dvdsval2 |
|- ( ( M e. ZZ /\ M =/= 0 /\ ( A - B ) e. ZZ ) -> ( M || ( A - B ) <-> ( ( A - B ) / M ) e. ZZ ) ) |
| 16 |
4 14 7 15
|
syl3anc |
|- ( ph -> ( M || ( A - B ) <-> ( ( A - B ) / M ) e. ZZ ) ) |
| 17 |
13 16
|
mpbird |
|- ( ph -> M || ( A - B ) ) |
| 18 |
1 6
|
zaddcld |
|- ( ph -> ( A + B ) e. ZZ ) |
| 19 |
|
dvdsmul2 |
|- ( ( ( A + B ) e. ZZ /\ ( A - B ) e. ZZ ) -> ( A - B ) || ( ( A + B ) x. ( A - B ) ) ) |
| 20 |
18 7 19
|
syl2anc |
|- ( ph -> ( A - B ) || ( ( A + B ) x. ( A - B ) ) ) |
| 21 |
1
|
zcnd |
|- ( ph -> A e. CC ) |
| 22 |
6
|
zcnd |
|- ( ph -> B e. CC ) |
| 23 |
|
subsq |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) ) |
| 24 |
21 22 23
|
syl2anc |
|- ( ph -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) ) |
| 25 |
20 24
|
breqtrrd |
|- ( ph -> ( A - B ) || ( ( A ^ 2 ) - ( B ^ 2 ) ) ) |
| 26 |
4 7 12 17 25
|
dvdstrd |
|- ( ph -> M || ( ( A ^ 2 ) - ( B ^ 2 ) ) ) |