MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moddvds Structured version   Unicode version

Theorem moddvds 14014
Description: Two ways to say  A  ==  B (  mod  N
). (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 nnrp 11166 . . . . . 6  |-  ( N  e.  NN  ->  N  e.  RR+ )
21adantr 463 . . . . 5  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  N  e.  RR+ )
3 0mod 11947 . . . . 5  |-  ( N  e.  RR+  ->  ( 0  mod  N )  =  0 )
42, 3syl 16 . . . 4  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( 0  mod  N )  =  0 )
54eqeq2d 2406 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( A  -  B
)  mod  N )  =  ( 0  mod 
N )  <->  ( ( A  -  B )  mod  N )  =  0 ) )
6 zre 10803 . . . . . . 7  |-  ( A  e.  ZZ  ->  A  e.  RR )
76ad2antrl 725 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  A  e.  RR )
8 zre 10803 . . . . . . 7  |-  ( B  e.  ZZ  ->  B  e.  RR )
98ad2antll 726 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  B  e.  RR )
109renegcld 9922 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  -u B  e.  RR )
11 modadd1 11953 . . . . . . 7  |-  ( ( ( 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 )
)
12113expia 1196 . . . . . 6  |-  ( ( ( 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 )
) )
137, 9, 10, 2, 12syl22anc 1227 . . . . 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
) ) )
147recnd 9551 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  A  e.  CC )
159recnd 9551 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  B  e.  CC )
1614, 15negsubd 9868 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( A  +  -u B )  =  ( A  -  B
) )
1716oveq1d 6229 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  +  -u B )  mod  N )  =  ( ( A  -  B )  mod  N
) )
1815negidd 9852 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( B  +  -u B )  =  0 )
1918oveq1d 6229 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( B  +  -u B )  mod  N )  =  ( 0  mod  N
) )
2017, 19eqeq12d 2414 . . . . 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 ) ) )
2113, 20sylibd 214 . . . 4  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  mod  N )  =  ( B  mod  N
)  ->  ( ( A  -  B )  mod  N )  =  ( 0  mod  N ) ) )
227, 9resubcld 9923 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( A  -  B )  e.  RR )
23 0red 9526 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  0  e.  RR )
24 modadd1 11953 . . . . . . 7  |-  ( ( ( ( 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 ) )
25243expia 1196 . . . . . 6  |-  ( ( ( ( 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 ) ) )
2622, 23, 9, 2, 25syl22anc 1227 . . . . 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 ) ) )
2714, 15npcand 9866 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  -  B )  +  B )  =  A )
2827oveq1d 6229 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( A  -  B
)  +  B )  mod  N )  =  ( A  mod  N
) )
2915addid2d 9710 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( 0  +  B )  =  B )
3029oveq1d 6229 . . . . . 6  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
0  +  B )  mod  N )  =  ( B  mod  N
) )
3128, 30eqeq12d 2414 . . . . 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 ) ) )
3226, 31sylibd 214 . . . 4  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( (
( A  -  B
)  mod  N )  =  ( 0  mod 
N )  ->  ( A  mod  N )  =  ( B  mod  N
) ) )
3321, 32impbid 191 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  mod  N )  =  ( B  mod  N
)  <->  ( ( A  -  B )  mod 
N )  =  ( 0  mod  N ) ) )
34 zsubcl 10841 . . . 4  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  -  B
)  e.  ZZ )
35 dvdsval3 14011 . . . 4  |-  ( ( N  e.  NN  /\  ( A  -  B
)  e.  ZZ )  ->  ( N  ||  ( A  -  B
)  <->  ( ( A  -  B )  mod 
N )  =  0 ) )
3634, 35sylan2 472 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( N  ||  ( A  -  B
)  <->  ( ( A  -  B )  mod 
N )  =  0 ) )
375, 33, 363bitr4d 285 . 2  |-  ( ( N  e.  NN  /\  ( A  e.  ZZ  /\  B  e.  ZZ ) )  ->  ( ( A  mod  N )  =  ( B  mod  N
)  <->  N  ||  ( A  -  B ) ) )
38373impb 1190 1  |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  B  e.  ZZ )  ->  (
( A  mod  N
)  =  ( B  mod  N )  <->  N  ||  ( A  -  B )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1836   class class class wbr 4380  (class class class)co 6214   RRcr 9420   0cc0 9421    + caddc 9424    - cmin 9736   -ucneg 9737   NNcn 10470   ZZcz 10799   RR+crp 11157    mod cmo 11915    || cdvds 14007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498  ax-pre-sup 9499
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-recs 6978  df-rdg 7012  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-sup 7834  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-div 10142  df-nn 10471  df-n0 10731  df-z 10800  df-uz 11020  df-rp 11158  df-fl 11847  df-mod 11916  df-dvds 14008
This theorem is referenced by:  dvdsmod  14064  sadadd3  14132  sadaddlem  14137  crt  14329  eulerthlem2  14333  prmdiv  14336  prmdiveq  14337  odzcllem  14340  odzdvds  14343  odzphi  14344  modprm1div  14345  pockthlem  14444  4sqlem11  14494  4sqlem12  14495  mndodcong  16702  dfod2  16722  sylow3lem6  16788  znf1o  18700  wilthlem1  23478  wilthlem2  23479  wilthlem3  23480  ppiub  23615  lgslem1  23707  lgsmod  23732  lgsdirprm  23740  lgsqrlem1  23752  lgsqrlem2  23753  lgsqr  23757  lgsdchrval  23758  lgseisenlem2  23761  lgseisenlem3  23762  lgseisenlem4  23763  m1lgs  23773  dvdsabsmod0OLD  31130
  Copyright terms: Public domain W3C validator