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 
|- ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( P || ( K mod N ) <-> P || K ) )

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> K e. ZZ )
2 1 zred 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> K e. RR )
3 simpl2 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> N e. NN )
4 3 nnrpd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> N e. RR+ )
5 modval 
 |-  ( ( K e. RR /\ N e. RR+ ) -> ( K mod N ) = ( K - ( N x. ( |_ ` ( K / N ) ) ) ) )
6 2 4 5 syl2anc 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( K mod N ) = ( K - ( N x. ( |_ ` ( K / N ) ) ) ) )
7 6 breq2d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( P || ( K mod N ) <-> P || ( K - ( N x. ( |_ ` ( K / N ) ) ) ) ) )
8 simpl1 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> P e. NN )
9 8 nnzd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> P e. ZZ )
10 3 nnzd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> N e. ZZ )
11 2 3 nndivred 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( K / N ) e. RR )
12 11 flcld 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( |_ ` ( K / N ) ) e. ZZ )
13 simpr 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> P || N )
14 9 10 12 13 dvdsmultr1d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> P || ( N x. ( |_ ` ( K / N ) ) ) )
15 10 12 zmulcld 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( N x. ( |_ ` ( K / N ) ) ) e. ZZ )
16 15 zcnd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( N x. ( |_ ` ( K / N ) ) ) e. CC )
17 16 subid1d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( ( N x. ( |_ ` ( K / N ) ) ) - 0 ) = ( N x. ( |_ ` ( K / N ) ) ) )
18 14 17 breqtrrd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> P || ( ( N x. ( |_ ` ( K / N ) ) ) - 0 ) )
19 0zd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> 0 e. ZZ )
20 moddvds 
 |-  ( ( P e. NN /\ ( N x. ( |_ ` ( K / N ) ) ) e. ZZ /\ 0 e. ZZ ) -> ( ( ( N x. ( |_ ` ( K / N ) ) ) mod P ) = ( 0 mod P ) <-> P || ( ( N x. ( |_ ` ( K / N ) ) ) - 0 ) ) )
21 8 15 19 20 syl3anc 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( ( ( N x. ( |_ ` ( K / N ) ) ) mod P ) = ( 0 mod P ) <-> P || ( ( N x. ( |_ ` ( K / N ) ) ) - 0 ) ) )
22 18 21 mpbird 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( ( N x. ( |_ ` ( K / N ) ) ) mod P ) = ( 0 mod P ) )
23 22 eqeq2d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( ( K mod P ) = ( ( N x. ( |_ ` ( K / N ) ) ) mod P ) <-> ( K mod P ) = ( 0 mod P ) ) )
24 moddvds 
 |-  ( ( P e. NN /\ K e. ZZ /\ ( N x. ( |_ ` ( K / N ) ) ) e. ZZ ) -> ( ( K mod P ) = ( ( N x. ( |_ ` ( K / N ) ) ) mod P ) <-> P || ( K - ( N x. ( |_ ` ( K / N ) ) ) ) ) )
25 8 1 15 24 syl3anc 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( ( K mod P ) = ( ( N x. ( |_ ` ( K / N ) ) ) mod P ) <-> P || ( K - ( N x. ( |_ ` ( K / N ) ) ) ) ) )
26 moddvds 
 |-  ( ( P e. NN /\ K e. ZZ /\ 0 e. ZZ ) -> ( ( K mod P ) = ( 0 mod P ) <-> P || ( K - 0 ) ) )
27 8 1 19 26 syl3anc 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( ( K mod P ) = ( 0 mod P ) <-> P || ( K - 0 ) ) )
28 23 25 27 3bitr3d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( P || ( K - ( N x. ( |_ ` ( K / N ) ) ) ) <-> P || ( K - 0 ) ) )
29 1 zcnd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> K e. CC )
30 29 subid1d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( K - 0 ) = K )
31 30 breq2d 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( P || ( K - 0 ) <-> P || K ) )
32 7 28 31 3bitrd 
 |-  ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( P || ( K mod N ) <-> P || K ) )