Metamath Proof Explorer

Theorem 4sqlem5

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 4sqlem5 
|- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )

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 1 zcnd 
 |-  ( ph -> A e. CC )
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 10 recnd 
 |-  ( ph -> ( ( A + ( M / 2 ) ) mod M ) e. CC )
12 7 recnd 
 |-  ( ph -> ( M / 2 ) e. CC )
13 11 12 subcld 
 |-  ( ph -> ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) e. CC )
14 3 13 eqeltrid 
 |-  ( ph -> B e. CC )
15 4 14 nncand 
 |-  ( ph -> ( A - ( A - B ) ) = B )
16 4 14 subcld 
 |-  ( ph -> ( A - B ) e. CC )
17 6 recnd 
 |-  ( ph -> M e. CC )
18 2 nnne0d 
 |-  ( ph -> M =/= 0 )
19 16 17 18 divcan1d 
 |-  ( ph -> ( ( ( A - B ) / M ) x. M ) = ( A - B ) )
20 3 oveq2i 
 |-  ( A - B ) = ( A - ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) )
21 4 11 12 subsub3d 
 |-  ( ph -> ( A - ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ) = ( ( A + ( M / 2 ) ) - ( ( A + ( M / 2 ) ) mod M ) ) )
22 20 21 eqtrid 
 |-  ( ph -> ( A - B ) = ( ( A + ( M / 2 ) ) - ( ( A + ( M / 2 ) ) mod M ) ) )
23 22 oveq1d 
 |-  ( ph -> ( ( A - B ) / M ) = ( ( ( A + ( M / 2 ) ) - ( ( A + ( M / 2 ) ) mod M ) ) / M ) )
24 moddifz 
 |-  ( ( ( A + ( M / 2 ) ) e. RR /\ M e. RR+ ) -> ( ( ( A + ( M / 2 ) ) - ( ( A + ( M / 2 ) ) mod M ) ) / M ) e. ZZ )
25 8 9 24 syl2anc 
 |-  ( ph -> ( ( ( A + ( M / 2 ) ) - ( ( A + ( M / 2 ) ) mod M ) ) / M ) e. ZZ )
26 23 25 eqeltrd 
 |-  ( ph -> ( ( A - B ) / M ) e. ZZ )
27 2 nnzd 
 |-  ( ph -> M e. ZZ )
28 26 27 zmulcld 
 |-  ( ph -> ( ( ( A - B ) / M ) x. M ) e. ZZ )
29 19 28 eqeltrrd 
 |-  ( ph -> ( A - B ) e. ZZ )
30 1 29 zsubcld 
 |-  ( ph -> ( A - ( A - B ) ) e. ZZ )
31 15 30 eqeltrrd 
 |-  ( ph -> B e. ZZ )
32 31 26 jca 
 |-  ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )