Metamath Proof Explorer

Theorem 4sqlem6

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 15-Jul-2014)

Ref Expression
Hypotheses 4sqlem5.2 
|- ( ph -> A e. ZZ )
4sqlem5.3 
|- ( ph -> M e. NN )
4sqlem5.4 
|- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
Assertion 4sqlem6 
|- ( ph -> ( -u ( M / 2 ) <_ B /\ B < ( M / 2 ) ) )

Proof

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 ) ) )