This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem moddvds

Description: Two ways to say A == B (mod N ), see also definition in ApostolNT p. 106. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion moddvds 
|- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )

Proof

Step Hyp Ref Expression
1 nnrp 
 |-  ( N e. NN -> N e. RR+ )
2 1 adantr 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> N e. RR+ )
3 0mod 
 |-  ( N e. RR+ -> ( 0 mod N ) = 0 )
4 2 3 syl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( 0 mod N ) = 0 )
5 4 eqeq2d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( ( A - B ) mod N ) = ( 0 mod N ) <-> ( ( A - B ) mod N ) = 0 ) )
6 zre 
 |-  ( A e. ZZ -> A e. RR )
7 6 ad2antrl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> A e. RR )
8 zre 
 |-  ( B e. ZZ -> B e. RR )
9 8 ad2antll 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> B e. RR )
10 9 renegcld 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> -u B e. RR )
11 modadd1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( -u B e. RR /\ N e. RR+ ) /\ ( A mod N ) = ( B mod N ) ) -> ( ( A + -u B ) mod N ) = ( ( B + -u B ) mod N ) )
12 11 3expia 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( -u B e. RR /\ N e. RR+ ) ) -> ( ( A mod N ) = ( B mod N ) -> ( ( A + -u B ) mod N ) = ( ( B + -u B ) mod N ) ) )
13 7 9 10 2 12 syl22anc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( A mod N ) = ( B mod N ) -> ( ( A + -u B ) mod N ) = ( ( B + -u B ) mod N ) ) )
14 7 recnd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> A e. CC )
15 9 recnd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> B e. CC )
16 14 15 negsubd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A + -u B ) = ( A - B ) )
17 16 oveq1d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( A + -u B ) mod N ) = ( ( A - B ) mod N ) )
18 15 negidd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( B + -u B ) = 0 )
19 18 oveq1d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( B + -u B ) mod N ) = ( 0 mod N ) )
20 17 19 eqeq12d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( ( A + -u B ) mod N ) = ( ( B + -u B ) mod N ) <-> ( ( A - B ) mod N ) = ( 0 mod N ) ) )
21 13 20 sylibd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( A mod N ) = ( B mod N ) -> ( ( A - B ) mod N ) = ( 0 mod N ) ) )
22 7 9 resubcld 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A - B ) e. RR )
23 0red 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> 0 e. RR )
24 modadd1 
 |-  ( ( ( ( A - B ) e. RR /\ 0 e. RR ) /\ ( B e. RR /\ N e. RR+ ) /\ ( ( A - B ) mod N ) = ( 0 mod N ) ) -> ( ( ( A - B ) + B ) mod N ) = ( ( 0 + B ) mod N ) )
25 24 3expia 
 |-  ( ( ( ( A - B ) e. RR /\ 0 e. RR ) /\ ( B e. RR /\ N e. RR+ ) ) -> ( ( ( A - B ) mod N ) = ( 0 mod N ) -> ( ( ( A - B ) + B ) mod N ) = ( ( 0 + B ) mod N ) ) )
26 22 23 9 2 25 syl22anc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( ( A - B ) mod N ) = ( 0 mod N ) -> ( ( ( A - B ) + B ) mod N ) = ( ( 0 + B ) mod N ) ) )
27 14 15 npcand 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( A - B ) + B ) = A )
28 27 oveq1d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( ( A - B ) + B ) mod N ) = ( A mod N ) )
29 15 addlidd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( 0 + B ) = B )
30 29 oveq1d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( 0 + B ) mod N ) = ( B mod N ) )
31 28 30 eqeq12d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( ( ( A - B ) + B ) mod N ) = ( ( 0 + B ) mod N ) <-> ( A mod N ) = ( B mod N ) ) )
32 26 31 sylibd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( ( A - B ) mod N ) = ( 0 mod N ) -> ( A mod N ) = ( B mod N ) ) )
33 21 32 impbid 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( A mod N ) = ( B mod N ) <-> ( ( A - B ) mod N ) = ( 0 mod N ) ) )
34 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
35 dvdsval3 
 |-  ( ( N e. NN /\ ( A - B ) e. ZZ ) -> ( N || ( A - B ) <-> ( ( A - B ) mod N ) = 0 ) )
36 34 35 sylan2 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( N || ( A - B ) <-> ( ( A - B ) mod N ) = 0 ) )
37 5 33 36 3bitr4d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )
38 37 3impb 
 |-  ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )