Metamath Proof Explorer

Theorem 4sqlem8

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 4sqlem8 
|- ( ph -> M || ( ( A ^ 2 ) - ( B ^ 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 2 nnzd 
 |-  ( ph -> M e. ZZ )
5 1 2 3 4sqlem5 
 |-  ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )
6 5 simpld 
 |-  ( ph -> B e. ZZ )
7 1 6 zsubcld 
 |-  ( ph -> ( A - B ) e. ZZ )
8 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
9 1 8 syl 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
10 zsqcl 
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
11 6 10 syl 
 |-  ( ph -> ( B ^ 2 ) e. ZZ )
12 9 11 zsubcld 
 |-  ( ph -> ( ( A ^ 2 ) - ( B ^ 2 ) ) e. ZZ )
13 5 simprd 
 |-  ( ph -> ( ( A - B ) / M ) e. ZZ )
14 2 nnne0d 
 |-  ( ph -> M =/= 0 )
15 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ ( A - B ) e. ZZ ) -> ( M || ( A - B ) <-> ( ( A - B ) / M ) e. ZZ ) )
16 4 14 7 15 syl3anc 
 |-  ( ph -> ( M || ( A - B ) <-> ( ( A - B ) / M ) e. ZZ ) )
17 13 16 mpbird 
 |-  ( ph -> M || ( A - B ) )
18 1 6 zaddcld 
 |-  ( ph -> ( A + B ) e. ZZ )
19 dvdsmul2 
 |-  ( ( ( A + B ) e. ZZ /\ ( A - B ) e. ZZ ) -> ( A - B ) || ( ( A + B ) x. ( A - B ) ) )
20 18 7 19 syl2anc 
 |-  ( ph -> ( A - B ) || ( ( A + B ) x. ( A - B ) ) )
21 1 zcnd 
 |-  ( ph -> A e. CC )
22 6 zcnd 
 |-  ( ph -> B e. CC )
23 subsq 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) )
24 21 22 23 syl2anc 
 |-  ( ph -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) )
25 20 24 breqtrrd 
 |-  ( ph -> ( A - B ) || ( ( A ^ 2 ) - ( B ^ 2 ) ) )
26 4 7 12 17 25 dvdstrd 
 |-  ( ph -> M || ( ( A ^ 2 ) - ( B ^ 2 ) ) )