| 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 |
|
4sqlem9.5 |
|- ( ( ph /\ ps ) -> ( B ^ 2 ) = 0 ) |
| 5 |
1 2 3
|
4sqlem5 |
|- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) ) |
| 6 |
5
|
simpld |
|- ( ph -> B e. ZZ ) |
| 7 |
6
|
zcnd |
|- ( ph -> B e. CC ) |
| 8 |
|
sqeq0 |
|- ( B e. CC -> ( ( B ^ 2 ) = 0 <-> B = 0 ) ) |
| 9 |
7 8
|
syl |
|- ( ph -> ( ( B ^ 2 ) = 0 <-> B = 0 ) ) |
| 10 |
9
|
biimpa |
|- ( ( ph /\ ( B ^ 2 ) = 0 ) -> B = 0 ) |
| 11 |
4 10
|
syldan |
|- ( ( ph /\ ps ) -> B = 0 ) |
| 12 |
11
|
oveq2d |
|- ( ( ph /\ ps ) -> ( A - B ) = ( A - 0 ) ) |
| 13 |
1
|
adantr |
|- ( ( ph /\ ps ) -> A e. ZZ ) |
| 14 |
13
|
zcnd |
|- ( ( ph /\ ps ) -> A e. CC ) |
| 15 |
14
|
subid1d |
|- ( ( ph /\ ps ) -> ( A - 0 ) = A ) |
| 16 |
12 15
|
eqtrd |
|- ( ( ph /\ ps ) -> ( A - B ) = A ) |
| 17 |
16
|
oveq1d |
|- ( ( ph /\ ps ) -> ( ( A - B ) / M ) = ( A / M ) ) |
| 18 |
5
|
simprd |
|- ( ph -> ( ( A - B ) / M ) e. ZZ ) |
| 19 |
18
|
adantr |
|- ( ( ph /\ ps ) -> ( ( A - B ) / M ) e. ZZ ) |
| 20 |
17 19
|
eqeltrrd |
|- ( ( ph /\ ps ) -> ( A / M ) e. ZZ ) |
| 21 |
2
|
nnzd |
|- ( ph -> M e. ZZ ) |
| 22 |
2
|
nnne0d |
|- ( ph -> M =/= 0 ) |
| 23 |
|
dvdsval2 |
|- ( ( M e. ZZ /\ M =/= 0 /\ A e. ZZ ) -> ( M || A <-> ( A / M ) e. ZZ ) ) |
| 24 |
21 22 1 23
|
syl3anc |
|- ( ph -> ( M || A <-> ( A / M ) e. ZZ ) ) |
| 25 |
24
|
adantr |
|- ( ( ph /\ ps ) -> ( M || A <-> ( A / M ) e. ZZ ) ) |
| 26 |
20 25
|
mpbird |
|- ( ( ph /\ ps ) -> M || A ) |
| 27 |
|
dvdssq |
|- ( ( M e. ZZ /\ A e. ZZ ) -> ( M || A <-> ( M ^ 2 ) || ( A ^ 2 ) ) ) |
| 28 |
21 13 27
|
syl2an2r |
|- ( ( ph /\ ps ) -> ( M || A <-> ( M ^ 2 ) || ( A ^ 2 ) ) ) |
| 29 |
26 28
|
mpbid |
|- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( A ^ 2 ) ) |