Metamath Proof Explorer


Theorem dvdsmod

Description: Any number K whose mod base N is divisible by a divisor P of the base is also divisible by P . This means that primes will also be relatively prime to the base when reduced mod N for any base. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion dvdsmod PNKPNPKmodNPK

Proof

Step Hyp Ref Expression
1 simpl3 PNKPNK
2 1 zred PNKPNK
3 simpl2 PNKPNN
4 3 nnrpd PNKPNN+
5 modval KN+KmodN=KNKN
6 2 4 5 syl2anc PNKPNKmodN=KNKN
7 6 breq2d PNKPNPKmodNPKNKN
8 simpl1 PNKPNP
9 8 nnzd PNKPNP
10 3 nnzd PNKPNN
11 2 3 nndivred PNKPNKN
12 11 flcld PNKPNKN
13 simpr PNKPNPN
14 9 10 12 13 dvdsmultr1d PNKPNPNKN
15 10 12 zmulcld PNKPNNKN
16 15 zcnd PNKPNNKN
17 16 subid1d PNKPNNKN0=NKN
18 14 17 breqtrrd PNKPNPNKN0
19 0zd PNKPN0
20 moddvds PNKN0NKNmodP=0modPPNKN0
21 8 15 19 20 syl3anc PNKPNNKNmodP=0modPPNKN0
22 18 21 mpbird PNKPNNKNmodP=0modP
23 22 eqeq2d PNKPNKmodP=NKNmodPKmodP=0modP
24 moddvds PKNKNKmodP=NKNmodPPKNKN
25 8 1 15 24 syl3anc PNKPNKmodP=NKNmodPPKNKN
26 moddvds PK0KmodP=0modPPK0
27 8 1 19 26 syl3anc PNKPNKmodP=0modPPK0
28 23 25 27 3bitr3d PNKPNPKNKNPK0
29 1 zcnd PNKPNK
30 29 subid1d PNKPNK0=K
31 30 breq2d PNKPNPK0PK
32 7 28 31 3bitrd PNKPNPKmodNPK