ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  moddvds Unicode version

Theorem moddvds 11765
Description: Two ways to say  A  ==  B (mod  N), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
Assertion
Ref Expression
moddvds  |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  B  e.  ZZ )  ->  (
( A  mod  N
)  =  ( B  mod  N )  <->  N  ||  ( A  -  B )
) )

Proof of Theorem moddvds
StepHypRef Expression
1 nnq 9596 . . . . . 6  |-  ( N  e.  NN  ->  N  e.  QQ )
21adantr 274 . . . . 5  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  N  e.  QQ )
3 nngt0 8907 . . . . . 6  |-  ( N  e.  NN  ->  0  <  N )
43adantr 274 . . . . 5  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  0  <  N )
5 q0mod 10315 . . . . 5  |-  ( ( N  e.  QQ  /\  0  <  N )  -> 
( 0  mod  N
)  =  0 )
62, 4, 5syl2anc 409 . . . 4  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( 0  mod  N )  =  0 )
76eqeq2d 2183 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( A  -  B
)  mod  N )  =  ( 0  mod 
N )  <->  ( ( A  -  B )  mod  N )  =  0 ) )
8 zq 9589 . . . . . . . . 9  |-  ( A  e.  ZZ  ->  A  e.  QQ )
98ad2antrl 488 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  A  e.  QQ )
109adantr 274 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( A  mod  N )  =  ( B  mod  N
) )  ->  A  e.  QQ )
11 zq 9589 . . . . . . . . 9  |-  ( B  e.  ZZ  ->  B  e.  QQ )
1211ad2antll 489 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  B  e.  QQ )
1312adantr 274 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( A  mod  N )  =  ( B  mod  N
) )  ->  B  e.  QQ )
14 qnegcl 9599 . . . . . . . 8  |-  ( B  e.  QQ  ->  -u B  e.  QQ )
1513, 14syl 14 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( A  mod  N )  =  ( B  mod  N
) )  ->  -u B  e.  QQ )
162adantr 274 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( A  mod  N )  =  ( B  mod  N
) )  ->  N  e.  QQ )
174adantr 274 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( A  mod  N )  =  ( B  mod  N
) )  ->  0  <  N )
18 simpr 109 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( A  mod  N )  =  ( B  mod  N
) )  ->  ( A  mod  N )  =  ( B  mod  N
) )
1910, 13, 15, 16, 17, 18modqadd1 10321 . . . . . 6  |-  ( ( ( 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 )
)
2019ex 114 . . . . 5  |-  ( ( 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
) ) )
21 simprl 527 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  A  e.  ZZ )
2221zcnd 9339 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  A  e.  CC )
23 simprr 528 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  B  e.  ZZ )
2423zcnd 9339 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  B  e.  CC )
2522, 24negsubd 8240 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( A  +  -u B )  =  ( A  -  B
) )
2625oveq1d 5872 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  +  -u B )  mod  N )  =  ( ( A  -  B )  mod  N
) )
2724negidd 8224 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( B  +  -u B )  =  0 )
2827oveq1d 5872 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( B  +  -u B )  mod  N )  =  ( 0  mod  N
) )
2926, 28eqeq12d 2186 . . . . 5  |-  ( ( 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 ) ) )
3020, 29sylibd 148 . . . 4  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  mod  N )  =  ( B  mod  N
)  ->  ( ( A  -  B )  mod  N )  =  ( 0  mod  N ) ) )
319adantr 274 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  A  e.  QQ )
3212adantr 274 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  B  e.  QQ )
33 qsubcl 9601 . . . . . . . 8  |-  ( ( A  e.  QQ  /\  B  e.  QQ )  ->  ( A  -  B
)  e.  QQ )
3431, 32, 33syl2anc 409 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  ( A  -  B )  e.  QQ )
35 0z 9227 . . . . . . . 8  |-  0  e.  ZZ
36 zq 9589 . . . . . . . 8  |-  ( 0  e.  ZZ  ->  0  e.  QQ )
3735, 36mp1i 10 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  0  e.  QQ )
382adantr 274 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  N  e.  QQ )
394adantr 274 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  0  <  N )
40 simpr 109 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  /\  ( ( A  -  B )  mod  N )  =  ( 0  mod  N
) )  ->  (
( A  -  B
)  mod  N )  =  ( 0  mod 
N ) )
4134, 37, 32, 38, 39, 40modqadd1 10321 . . . . . 6  |-  ( ( ( 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 ) )
4241ex 114 . . . . 5  |-  ( ( 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 ) ) )
4322, 24npcand 8238 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  -  B )  +  B )  =  A )
4443oveq1d 5872 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( A  -  B
)  +  B )  mod  N )  =  ( A  mod  N
) )
4524addid2d 8073 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( 0  +  B )  =  B )
4645oveq1d 5872 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
0  +  B )  mod  N )  =  ( B  mod  N
) )
4744, 46eqeq12d 2186 . . . . 5  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( ( A  -  B )  +  B
)  mod  N )  =  ( ( 0  +  B )  mod 
N )  <->  ( A  mod  N )  =  ( B  mod  N ) ) )
4842, 47sylibd 148 . . . 4  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( A  -  B
)  mod  N )  =  ( 0  mod 
N )  ->  ( A  mod  N )  =  ( B  mod  N
) ) )
4930, 48impbid 128 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  mod  N )  =  ( B  mod  N
)  <->  ( ( A  -  B )  mod 
N )  =  ( 0  mod  N ) ) )
50 zsubcl 9257 . . . 4  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  -  B
)  e.  ZZ )
51 dvdsval3 11757 . . . 4  |-  ( ( N  e.  NN  /\  ( A  -  B
)  e.  ZZ )  ->  ( N  ||  ( A  -  B
)  <->  ( ( A  -  B )  mod 
N )  =  0 ) )
5250, 51sylan2 284 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( N  ||  ( A  -  B
)  <->  ( ( A  -  B )  mod 
N )  =  0 ) )
537, 49, 523bitr4d 219 . 2  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  mod  N )  =  ( B  mod  N
)  <->  N  ||  ( A  -  B ) ) )
54533impb 1195 1  |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  B  e.  ZZ )  ->  (
( A  mod  N
)  =  ( B  mod  N )  <->  N  ||  ( A  -  B )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    /\ w3a 974    = wceq 1349    e. wcel 2142   class class class wbr 3990  (class class class)co 5857   0cc0 7778    + caddc 7781    < clt 7958    - cmin 8094   -ucneg 8095   NNcn 8882   ZZcz 9216   QQcq 9582    mod cmo 10282    || cdvds 11753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-cnex 7869  ax-resscn 7870  ax-1cn 7871  ax-1re 7872  ax-icn 7873  ax-addcl 7874  ax-addrcl 7875  ax-mulcl 7876  ax-mulrcl 7877  ax-addcom 7878  ax-mulcom 7879  ax-addass 7880  ax-mulass 7881  ax-distr 7882  ax-i2m1 7883  ax-0lt1 7884  ax-1rid 7885  ax-0id 7886  ax-rnegex 7887  ax-precex 7888  ax-cnre 7889  ax-pre-ltirr 7890  ax-pre-ltwlin 7891  ax-pre-lttrn 7892  ax-pre-apti 7893  ax-pre-ltadd 7894  ax-pre-mulgt0 7895  ax-pre-mulext 7896  ax-arch 7897
This theorem depends on definitions:  df-bi 116  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-nel 2437  df-ral 2454  df-rex 2455  df-reu 2456  df-rmo 2457  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-po 4282  df-iso 4283  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-fv 5208  df-riota 5813  df-ov 5860  df-oprab 5861  df-mpo 5862  df-1st 6123  df-2nd 6124  df-pnf 7960  df-mnf 7961  df-xr 7962  df-ltxr 7963  df-le 7964  df-sub 8096  df-neg 8097  df-reap 8498  df-ap 8505  df-div 8594  df-inn 8883  df-n0 9140  df-z 9217  df-q 9583  df-rp 9615  df-fl 10230  df-mod 10283  df-dvds 11754
This theorem is referenced by:  modm1div  11766  summodnegmod  11788  modmulconst  11789  addmodlteqALT  11823  dvdsmod  11826  congr  12058  cncongr1  12061  cncongr2  12062  crth  12182  eulerthlemh  12189  eulerthlemth  12190  prmdiv  12193  prmdiveq  12194  odzcllem  12200  odzdvds  12203  odzphi  12204  pockthlem  12312  lgslem1  13780  lgsmod  13806  lgsdirprm  13814
  Copyright terms: Public domain W3C validator