| 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 |
|
0red |
|- ( ph -> 0 e. RR ) |
| 5 |
1
|
zred |
|- ( ph -> A e. RR ) |
| 6 |
2
|
nnred |
|- ( ph -> M e. RR ) |
| 7 |
6
|
rehalfcld |
|- ( ph -> ( M / 2 ) e. RR ) |
| 8 |
5 7
|
readdcld |
|- ( ph -> ( A + ( M / 2 ) ) e. RR ) |
| 9 |
2
|
nnrpd |
|- ( ph -> M e. RR+ ) |
| 10 |
8 9
|
modcld |
|- ( ph -> ( ( A + ( M / 2 ) ) mod M ) e. RR ) |
| 11 |
|
modge0 |
|- ( ( ( A + ( M / 2 ) ) e. RR /\ M e. RR+ ) -> 0 <_ ( ( A + ( M / 2 ) ) mod M ) ) |
| 12 |
8 9 11
|
syl2anc |
|- ( ph -> 0 <_ ( ( A + ( M / 2 ) ) mod M ) ) |
| 13 |
4 10 7 12
|
lesub1dd |
|- ( ph -> ( 0 - ( M / 2 ) ) <_ ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ) |
| 14 |
|
df-neg |
|- -u ( M / 2 ) = ( 0 - ( M / 2 ) ) |
| 15 |
13 14 3
|
3brtr4g |
|- ( ph -> -u ( M / 2 ) <_ B ) |
| 16 |
|
modlt |
|- ( ( ( A + ( M / 2 ) ) e. RR /\ M e. RR+ ) -> ( ( A + ( M / 2 ) ) mod M ) < M ) |
| 17 |
8 9 16
|
syl2anc |
|- ( ph -> ( ( A + ( M / 2 ) ) mod M ) < M ) |
| 18 |
2
|
nncnd |
|- ( ph -> M e. CC ) |
| 19 |
18
|
2halvesd |
|- ( ph -> ( ( M / 2 ) + ( M / 2 ) ) = M ) |
| 20 |
17 19
|
breqtrrd |
|- ( ph -> ( ( A + ( M / 2 ) ) mod M ) < ( ( M / 2 ) + ( M / 2 ) ) ) |
| 21 |
10 7 7
|
ltsubaddd |
|- ( ph -> ( ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) < ( M / 2 ) <-> ( ( A + ( M / 2 ) ) mod M ) < ( ( M / 2 ) + ( M / 2 ) ) ) ) |
| 22 |
20 21
|
mpbird |
|- ( ph -> ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) < ( M / 2 ) ) |
| 23 |
3 22
|
eqbrtrid |
|- ( ph -> B < ( M / 2 ) ) |
| 24 |
15 23
|
jca |
|- ( ph -> ( -u ( M / 2 ) <_ B /\ B < ( M / 2 ) ) ) |