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) (Proof shortened by SN, 27-Nov-2025)

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 peano2zm 
 |-  ( A e. ZZ -> ( A - 1 ) e. ZZ )
2 1 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A - 1 ) e. ZZ )
3 2 zred 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A - 1 ) e. RR )
4 nnrp 
 |-  ( N e. NN -> N e. RR+ )
5 4 3ad2ant2 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> N e. RR+ )
6 3 5 modcld 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A - 1 ) mod N ) e. RR )
7 6 recnd 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A - 1 ) mod N ) e. CC )
8 zre 
 |-  ( A e. ZZ -> A e. RR )
9 8 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> A e. RR )
10 9 5 modcld 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A mod N ) e. RR )
11 10 recnd 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( A mod N ) e. CC )
12 7 11 negsubdi2d 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> -u ( ( ( A - 1 ) mod N ) - ( A mod N ) ) = ( ( A mod N ) - ( ( A - 1 ) mod N ) ) )
13 m1modmmod 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) mod N ) - ( A mod N ) ) = if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) )
14 13 3adant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( ( A - 1 ) mod N ) - ( A mod N ) ) = if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) )
15 14 negeqd 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> -u ( ( ( A - 1 ) mod N ) - ( A mod N ) ) = -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) )
16 12 15 eqtr3d 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) = -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) )
17 iftrue 
 |-  ( ( A mod N ) = 0 -> if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) = ( N - 1 ) )
18 17 adantr 
 |-  ( ( ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) = ( N - 1 ) )
19 18 negeqd 
 |-  ( ( ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) = -u ( N - 1 ) )
20 1red 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 1 e. RR )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 2 e. RR )
23 nnre 
 |-  ( N e. NN -> N e. RR )
24 23 3ad2ant2 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> N e. RR )
25 1lt2 
 |-  1 < 2
26 25 a1i 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 1 < 2 )
27 simp3 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 2 < N )
28 20 22 24 26 27 lttrd 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 1 < N )
29 difrp 
 |-  ( ( 1 e. RR /\ N e. RR ) -> ( 1 < N <-> ( N - 1 ) e. RR+ ) )
30 20 24 29 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( 1 < N <-> ( N - 1 ) e. RR+ ) )
31 28 30 mpbid 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( N - 1 ) e. RR+ )
32 neglt 
 |-  ( ( N - 1 ) e. RR+ -> -u ( N - 1 ) < ( N - 1 ) )
33 31 32 syl 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> -u ( N - 1 ) < ( N - 1 ) )
34 33 adantl 
 |-  ( ( ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -u ( N - 1 ) < ( N - 1 ) )
35 19 34 eqbrtrd 
 |-  ( ( ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) < ( N - 1 ) )
36 iffalse 
 |-  ( -. ( A mod N ) = 0 -> if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) = -u 1 )
37 36 adantr 
 |-  ( ( -. ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) = -u 1 )
38 37 negeqd 
 |-  ( ( -. ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) = -u -u 1 )
39 negneg1e1 
 |-  -u -u 1 = 1
40 df-2 
 |-  2 = ( 1 + 1 )
41 40 breq1i 
 |-  ( 2 < N <-> ( 1 + 1 ) < N )
42 41 biimpi 
 |-  ( 2 < N -> ( 1 + 1 ) < N )
43 42 3ad2ant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( 1 + 1 ) < N )
44 20 20 24 ltaddsub2d 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( 1 + 1 ) < N <-> 1 < ( N - 1 ) ) )
45 43 44 mpbid 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> 1 < ( N - 1 ) )
46 39 45 eqbrtrid 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> -u -u 1 < ( N - 1 ) )
47 46 adantl 
 |-  ( ( -. ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -u -u 1 < ( N - 1 ) )
48 38 47 eqbrtrd 
 |-  ( ( -. ( A mod N ) = 0 /\ ( A e. ZZ /\ N e. NN /\ 2 < N ) ) -> -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) < ( N - 1 ) )
49 35 48 pm2.61ian 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> -u if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) < ( N - 1 ) )
50 16 49 eqbrtrd 
 |-  ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )