Metamath Proof Explorer

Theorem difmodm1lt

Description: The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd A and N = 2 , since ( ( A mod N ) - ( ( A - 1 ) mod N ) ) would be ( 1 - 0 ) = 1 which is not less than ( N - 1 ) = 1 . (Contributed by AV, 6-Jun-2012)

Ref Expression
Assertion difmodm1lt 
|- ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( A mod N ) = 1 )
2 zre 
 |-  ( A e. ZZ -> A e. RR )
3 2 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> A e. RR )
4 nnre 
 |-  ( N e. NN -> N e. RR )
5 4 3ad2ant2 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> N e. RR )
6 1lt2 
 |-  1 < 2
7 1red 
 |-  ( N e. NN -> 1 e. RR )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( N e. NN -> 2 e. RR )
10 7 9 4 3jca 
 |-  ( N e. NN -> ( 1 e. RR /\ 2 e. RR /\ N e. RR ) )
11 lttr 
 |-  ( ( 1 e. RR /\ 2 e. RR /\ N e. RR ) -> ( ( 1 < 2 /\ 2 < N ) -> 1 < N ) )
12 10 11 syl 
 |-  ( N e. NN -> ( ( 1 < 2 /\ 2 < N ) -> 1 < N ) )
13 6 12 mpani 
 |-  ( N e. NN -> ( 2 < N -> 1 < N ) )
14 13 a1i 
 |-  ( A e. ZZ -> ( N e. NN -> ( 2 < N -> 1 < N ) ) )
15 14 3imp 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 1 < N )
16 3 5 15 3jca 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A e. RR /\ N e. RR /\ 1 < N ) )
17 16 adantl 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( A e. RR /\ N e. RR /\ 1 < N ) )
18 m1mod0mod1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( ( A - 1 ) mod N ) = 0 <-> ( A mod N ) = 1 ) )
19 17 18 syl 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( ( A - 1 ) mod N ) = 0 <-> ( A mod N ) = 1 ) )
20 1 19 mpbird 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A - 1 ) mod N ) = 0 )
21 1 20 oveq12d 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) = ( 1 - 0 ) )
22 df-2 
 |-  2 = ( 1 + 1 )
23 22 breq1i 
 |-  ( 2 < N <-> ( 1 + 1 ) < N )
24 23 biimpi 
 |-  ( 2 < N -> ( 1 + 1 ) < N )
25 24 adantl 
 |-  ( ( N e. NN /\ 2 < N ) -> ( 1 + 1 ) < N )
26 1red 
 |-  ( ( N e. NN /\ 2 < N ) -> 1 e. RR )
27 4 adantr 
 |-  ( ( N e. NN /\ 2 < N ) -> N e. RR )
28 26 26 27 ltaddsub2d 
 |-  ( ( N e. NN /\ 2 < N ) -> ( ( 1 + 1 ) < N <-> 1 < ( N - 1 ) ) )
29 25 28 mpbid 
 |-  ( ( N e. NN /\ 2 < N ) -> 1 < ( N - 1 ) )
30 1m0e1 
 |-  ( 1 - 0 ) = 1
31 30 breq1i 
 |-  ( ( 1 - 0 ) < ( N - 1 ) <-> 1 < ( N - 1 ) )
32 29 31 sylibr 
 |-  ( ( N e. NN /\ 2 < N ) -> ( 1 - 0 ) < ( N - 1 ) )
33 32 3adant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( 1 - 0 ) < ( N - 1 ) )
34 33 adantl 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( 1 - 0 ) < ( N - 1 ) )
35 21 34 eqbrtrd 
 |-  ( ( ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )
36 zmodfz 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A mod N ) e. ( 0 ... ( N - 1 ) ) )
37 36 3adant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A mod N ) e. ( 0 ... ( N - 1 ) ) )
38 elfzle2 
 |-  ( ( A mod N ) e. ( 0 ... ( N - 1 ) ) -> ( A mod N ) <_ ( N - 1 ) )
39 37 38 syl 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A mod N ) <_ ( N - 1 ) )
40 39 adantl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( A mod N ) <_ ( N - 1 ) )
41 nnrp 
 |-  ( N e. NN -> N e. RR+ )
42 41 3ad2ant2 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> N e. RR+ )
43 3 42 modcld 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A mod N ) e. RR )
44 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
45 4 44 syl 
 |-  ( N e. NN -> ( N - 1 ) e. RR )
46 45 3ad2ant2 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( N - 1 ) e. RR )
47 peano2zm 
 |-  ( A e. ZZ -> ( A - 1 ) e. ZZ )
48 47 zred 
 |-  ( A e. ZZ -> ( A - 1 ) e. RR )
49 48 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A - 1 ) e. RR )
50 49 42 modcld 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A - 1 ) mod N ) e. RR )
51 43 46 50 3jca 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) e. RR /\ ( N - 1 ) e. RR /\ ( ( A - 1 ) mod N ) e. RR ) )
52 51 adantl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A mod N ) e. RR /\ ( N - 1 ) e. RR /\ ( ( A - 1 ) mod N ) e. RR ) )
53 lesub1 
 |-  ( ( ( A mod N ) e. RR /\ ( N - 1 ) e. RR /\ ( ( A - 1 ) mod N ) e. RR ) -> ( ( A mod N ) <_ ( N - 1 ) <-> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) <_ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) ) )
54 52 53 syl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A mod N ) <_ ( N - 1 ) <-> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) <_ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) ) )
55 40 54 mpbid 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) <_ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) )
56 49 42 jca 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A - 1 ) e. RR /\ N e. RR+ ) )
57 56 adantl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A - 1 ) e. RR /\ N e. RR+ ) )
58 modge0 
 |-  ( ( ( A - 1 ) e. RR /\ N e. RR+ ) -> 0 <_ ( ( A - 1 ) mod N ) )
59 57 58 syl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> 0 <_ ( ( A - 1 ) mod N ) )
60 16 18 syl 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( ( A - 1 ) mod N ) = 0 <-> ( A mod N ) = 1 ) )
61 60 bicomd 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) = 1 <-> ( ( A - 1 ) mod N ) = 0 ) )
62 61 notbid 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( -. ( A mod N ) = 1 <-> -. ( ( A - 1 ) mod N ) = 0 ) )
63 62 biimpac 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -. ( ( A - 1 ) mod N ) = 0 )
64 63 neqned 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A - 1 ) mod N ) =/= 0 )
65 59 64 jca 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( 0 <_ ( ( A - 1 ) mod N ) /\ ( ( A - 1 ) mod N ) =/= 0 ) )
66 0red 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 0 e. RR )
67 66 50 jca 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( 0 e. RR /\ ( ( A - 1 ) mod N ) e. RR ) )
68 67 adantl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( 0 e. RR /\ ( ( A - 1 ) mod N ) e. RR ) )
69 ltlen 
 |-  ( ( 0 e. RR /\ ( ( A - 1 ) mod N ) e. RR ) -> ( 0 < ( ( A - 1 ) mod N ) <-> ( 0 <_ ( ( A - 1 ) mod N ) /\ ( ( A - 1 ) mod N ) =/= 0 ) ) )
70 68 69 syl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( 0 < ( ( A - 1 ) mod N ) <-> ( 0 <_ ( ( A - 1 ) mod N ) /\ ( ( A - 1 ) mod N ) =/= 0 ) ) )
71 65 70 mpbird 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> 0 < ( ( A - 1 ) mod N ) )
72 50 46 jca 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( ( A - 1 ) mod N ) e. RR /\ ( N - 1 ) e. RR ) )
73 72 adantl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( ( A - 1 ) mod N ) e. RR /\ ( N - 1 ) e. RR ) )
74 ltsubpos 
 |-  ( ( ( ( A - 1 ) mod N ) e. RR /\ ( N - 1 ) e. RR ) -> ( 0 < ( ( A - 1 ) mod N ) <-> ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) ) )
75 73 74 syl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( 0 < ( ( A - 1 ) mod N ) <-> ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) ) )
76 71 75 mpbid 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )
77 43 50 resubcld 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) e. RR )
78 46 50 resubcld 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) e. RR )
79 77 78 46 3jca 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( ( A mod N ) - ( ( A - 1 ) mod N ) ) e. RR /\ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) e. RR /\ ( N - 1 ) e. RR ) )
80 79 adantl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( ( A mod N ) - ( ( A - 1 ) mod N ) ) e. RR /\ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) e. RR /\ ( N - 1 ) e. RR ) )
81 lelttr 
 |-  ( ( ( ( A mod N ) - ( ( A - 1 ) mod N ) ) e. RR /\ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) e. RR /\ ( N - 1 ) e. RR ) -> ( ( ( ( A mod N ) - ( ( A - 1 ) mod N ) ) <_ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) /\ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) ) )
82 80 81 syl 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( ( ( A mod N ) - ( ( A - 1 ) mod N ) ) <_ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) /\ ( ( N - 1 ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) ) )
83 55 76 82 mp2and 
 |-  ( ( -. ( A mod N ) = 1 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )
84 35 83 pm2.61ian 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )