Metamath Proof Explorer

Theorem modlt0b

Description: An integer with an absolute value less than a positive integer is 0 modulo the positive integer iff it is 0. (Contributed by AV, 21-Nov-2025)

Ref Expression
Assertion modlt0b 
|- ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( ( X mod N ) = 0 <-> X = 0 ) )

Proof

Step Hyp Ref Expression
1 pm3.22 
 |-  ( ( N e. NN /\ X e. ZZ ) -> ( X e. ZZ /\ N e. NN ) )
2 1 3adant3 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( X e. ZZ /\ N e. NN ) )
3 mod0mul 
 |-  ( ( X e. ZZ /\ N e. NN ) -> ( ( X mod N ) = 0 -> E. z e. ZZ X = ( z x. N ) ) )
4 2 3 syl 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( ( X mod N ) = 0 -> E. z e. ZZ X = ( z x. N ) ) )
5 simpr 
 |-  ( ( ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) /\ z e. ZZ ) /\ X = ( z x. N ) ) -> X = ( z x. N ) )
6 fveq2 
 |-  ( X = ( z x. N ) -> ( abs ` X ) = ( abs ` ( z x. N ) ) )
7 6 adantl 
 |-  ( ( ( N e. NN /\ z e. ZZ ) /\ X = ( z x. N ) ) -> ( abs ` X ) = ( abs ` ( z x. N ) ) )
8 7 breq1d 
 |-  ( ( ( N e. NN /\ z e. ZZ ) /\ X = ( z x. N ) ) -> ( ( abs ` X ) < N <-> ( abs ` ( z x. N ) ) < N ) )
9 zcn 
 |-  ( z e. ZZ -> z e. CC )
10 nncn 
 |-  ( N e. NN -> N e. CC )
11 absmul 
 |-  ( ( z e. CC /\ N e. CC ) -> ( abs ` ( z x. N ) ) = ( ( abs ` z ) x. ( abs ` N ) ) )
12 9 10 11 syl2anr 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( abs ` ( z x. N ) ) = ( ( abs ` z ) x. ( abs ` N ) ) )
13 nnre 
 |-  ( N e. NN -> N e. RR )
14 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
15 14 nn0ge0d 
 |-  ( N e. NN -> 0 <_ N )
16 13 15 absidd 
 |-  ( N e. NN -> ( abs ` N ) = N )
17 16 adantr 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( abs ` N ) = N )
18 17 oveq2d 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( abs ` z ) x. ( abs ` N ) ) = ( ( abs ` z ) x. N ) )
19 12 18 eqtrd 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( abs ` ( z x. N ) ) = ( ( abs ` z ) x. N ) )
20 19 breq1d 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( abs ` ( z x. N ) ) < N <-> ( ( abs ` z ) x. N ) < N ) )
21 9 abscld 
 |-  ( z e. ZZ -> ( abs ` z ) e. RR )
22 21 adantl 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( abs ` z ) e. RR )
23 13 adantr 
 |-  ( ( N e. NN /\ z e. ZZ ) -> N e. RR )
24 nngt0 
 |-  ( N e. NN -> 0 < N )
25 13 24 jca 
 |-  ( N e. NN -> ( N e. RR /\ 0 < N ) )
26 25 adantr 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( N e. RR /\ 0 < N ) )
27 ltmuldiv 
 |-  ( ( ( abs ` z ) e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( abs ` z ) x. N ) < N <-> ( abs ` z ) < ( N / N ) ) )
28 22 23 26 27 syl3anc 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( ( abs ` z ) x. N ) < N <-> ( abs ` z ) < ( N / N ) ) )
29 nnne0 
 |-  ( N e. NN -> N =/= 0 )
30 10 29 dividd 
 |-  ( N e. NN -> ( N / N ) = 1 )
31 30 adantr 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( N / N ) = 1 )
32 31 breq2d 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( abs ` z ) < ( N / N ) <-> ( abs ` z ) < 1 ) )
33 28 32 bitrd 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( ( abs ` z ) x. N ) < N <-> ( abs ` z ) < 1 ) )
34 zabs0b 
 |-  ( z e. ZZ -> ( ( abs ` z ) < 1 <-> z = 0 ) )
35 34 adantl 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( abs ` z ) < 1 <-> z = 0 ) )
36 oveq1 
 |-  ( z = 0 -> ( z x. N ) = ( 0 x. N ) )
37 10 mul02d 
 |-  ( N e. NN -> ( 0 x. N ) = 0 )
38 36 37 sylan9eqr 
 |-  ( ( N e. NN /\ z = 0 ) -> ( z x. N ) = 0 )
39 38 ex 
 |-  ( N e. NN -> ( z = 0 -> ( z x. N ) = 0 ) )
40 39 adantr 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( z = 0 -> ( z x. N ) = 0 ) )
41 35 40 sylbid 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( abs ` z ) < 1 -> ( z x. N ) = 0 ) )
42 33 41 sylbid 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( ( abs ` z ) x. N ) < N -> ( z x. N ) = 0 ) )
43 20 42 sylbid 
 |-  ( ( N e. NN /\ z e. ZZ ) -> ( ( abs ` ( z x. N ) ) < N -> ( z x. N ) = 0 ) )
44 43 adantr 
 |-  ( ( ( N e. NN /\ z e. ZZ ) /\ X = ( z x. N ) ) -> ( ( abs ` ( z x. N ) ) < N -> ( z x. N ) = 0 ) )
45 8 44 sylbid 
 |-  ( ( ( N e. NN /\ z e. ZZ ) /\ X = ( z x. N ) ) -> ( ( abs ` X ) < N -> ( z x. N ) = 0 ) )
46 45 expl 
 |-  ( N e. NN -> ( ( z e. ZZ /\ X = ( z x. N ) ) -> ( ( abs ` X ) < N -> ( z x. N ) = 0 ) ) )
47 46 adantr 
 |-  ( ( N e. NN /\ X e. ZZ ) -> ( ( z e. ZZ /\ X = ( z x. N ) ) -> ( ( abs ` X ) < N -> ( z x. N ) = 0 ) ) )
48 47 com23 
 |-  ( ( N e. NN /\ X e. ZZ ) -> ( ( abs ` X ) < N -> ( ( z e. ZZ /\ X = ( z x. N ) ) -> ( z x. N ) = 0 ) ) )
49 48 3impia 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( ( z e. ZZ /\ X = ( z x. N ) ) -> ( z x. N ) = 0 ) )
50 49 impl 
 |-  ( ( ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) /\ z e. ZZ ) /\ X = ( z x. N ) ) -> ( z x. N ) = 0 )
51 5 50 eqtrd 
 |-  ( ( ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) /\ z e. ZZ ) /\ X = ( z x. N ) ) -> X = 0 )
52 51 ex 
 |-  ( ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) /\ z e. ZZ ) -> ( X = ( z x. N ) -> X = 0 ) )
53 52 rexlimdva 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( E. z e. ZZ X = ( z x. N ) -> X = 0 ) )
54 4 53 syld 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( ( X mod N ) = 0 -> X = 0 ) )
55 oveq1 
 |-  ( X = 0 -> ( X mod N ) = ( 0 mod N ) )
56 nnrp 
 |-  ( N e. NN -> N e. RR+ )
57 0mod 
 |-  ( N e. RR+ -> ( 0 mod N ) = 0 )
58 56 57 syl 
 |-  ( N e. NN -> ( 0 mod N ) = 0 )
59 58 3ad2ant1 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( 0 mod N ) = 0 )
60 55 59 sylan9eqr 
 |-  ( ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) /\ X = 0 ) -> ( X mod N ) = 0 )
61 60 ex 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( X = 0 -> ( X mod N ) = 0 ) )
62 54 61 impbid 
 |-  ( ( N e. NN /\ X e. ZZ /\ ( abs ` X ) < N ) -> ( ( X mod N ) = 0 <-> X = 0 ) )