| 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 |
1 2 3
|
4sqlem5 |
|- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) ) |
| 5 |
4
|
simpld |
|- ( ph -> B e. ZZ ) |
| 6 |
5
|
zred |
|- ( ph -> B e. RR ) |
| 7 |
2
|
nnrpd |
|- ( ph -> M e. RR+ ) |
| 8 |
7
|
rphalfcld |
|- ( ph -> ( M / 2 ) e. RR+ ) |
| 9 |
8
|
rpred |
|- ( ph -> ( M / 2 ) e. RR ) |
| 10 |
1 2 3
|
4sqlem6 |
|- ( ph -> ( -u ( M / 2 ) <_ B /\ B < ( M / 2 ) ) ) |
| 11 |
10
|
simprd |
|- ( ph -> B < ( M / 2 ) ) |
| 12 |
6 9 11
|
ltled |
|- ( ph -> B <_ ( M / 2 ) ) |
| 13 |
10
|
simpld |
|- ( ph -> -u ( M / 2 ) <_ B ) |
| 14 |
9 6 13
|
lenegcon1d |
|- ( ph -> -u B <_ ( M / 2 ) ) |
| 15 |
8
|
rpge0d |
|- ( ph -> 0 <_ ( M / 2 ) ) |
| 16 |
|
lenegsq |
|- ( ( B e. RR /\ ( M / 2 ) e. RR /\ 0 <_ ( M / 2 ) ) -> ( ( B <_ ( M / 2 ) /\ -u B <_ ( M / 2 ) ) <-> ( B ^ 2 ) <_ ( ( M / 2 ) ^ 2 ) ) ) |
| 17 |
6 9 15 16
|
syl3anc |
|- ( ph -> ( ( B <_ ( M / 2 ) /\ -u B <_ ( M / 2 ) ) <-> ( B ^ 2 ) <_ ( ( M / 2 ) ^ 2 ) ) ) |
| 18 |
12 14 17
|
mpbi2and |
|- ( ph -> ( B ^ 2 ) <_ ( ( M / 2 ) ^ 2 ) ) |
| 19 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
| 20 |
19
|
sqvald |
|- ( ph -> ( 2 ^ 2 ) = ( 2 x. 2 ) ) |
| 21 |
20
|
oveq2d |
|- ( ph -> ( ( M ^ 2 ) / ( 2 ^ 2 ) ) = ( ( M ^ 2 ) / ( 2 x. 2 ) ) ) |
| 22 |
2
|
nncnd |
|- ( ph -> M e. CC ) |
| 23 |
|
2ne0 |
|- 2 =/= 0 |
| 24 |
23
|
a1i |
|- ( ph -> 2 =/= 0 ) |
| 25 |
22 19 24
|
sqdivd |
|- ( ph -> ( ( M / 2 ) ^ 2 ) = ( ( M ^ 2 ) / ( 2 ^ 2 ) ) ) |
| 26 |
22
|
sqcld |
|- ( ph -> ( M ^ 2 ) e. CC ) |
| 27 |
26 19 19 24 24
|
divdiv1d |
|- ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) = ( ( M ^ 2 ) / ( 2 x. 2 ) ) ) |
| 28 |
21 25 27
|
3eqtr4d |
|- ( ph -> ( ( M / 2 ) ^ 2 ) = ( ( ( M ^ 2 ) / 2 ) / 2 ) ) |
| 29 |
18 28
|
breqtrd |
|- ( ph -> ( B ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) ) |