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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 𝐴 mod 𝑁 ) − ( ( 𝐴 − 1 ) mod 𝑁 ) ) < ( 𝑁 − 1 ) )

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℤ )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝐴 − 1 ) ∈ ℤ )
3 2 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝐴 − 1 ) ∈ ℝ )
4 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
5 4 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 𝑁 ∈ ℝ+ )
6 3 5 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ∈ ℝ )
7 6 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ∈ ℂ )
8 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 𝐴 ∈ ℝ )
10 9 5 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℝ )
11 10 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℂ )
12 7 11 negsubdi2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → - ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = ( ( 𝐴 mod 𝑁 ) − ( ( 𝐴 − 1 ) mod 𝑁 ) ) )
13 m1modmmod ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) )
14 13 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) )
15 14 negeqd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → - ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) )
16 12 15 eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 𝐴 mod 𝑁 ) − ( ( 𝐴 − 1 ) mod 𝑁 ) ) = - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) )
17 iftrue ⊢ ( ( 𝐴 mod 𝑁 ) = 0 → if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = ( 𝑁 − 1 ) )
18 17 adantr ⊢ ( ( ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = ( 𝑁 − 1 ) )
19 18 negeqd ⊢ ( ( ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = - ( 𝑁 − 1 ) )
20 1red ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 1 ∈ ℝ )
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 2 ∈ ℝ )
23 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
24 23 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 𝑁 ∈ ℝ )
25 1lt2 ⊢ 1 < 2
26 25 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 1 < 2 )
27 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 2 < 𝑁 )
28 20 22 24 26 27 lttrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 1 < 𝑁 )
29 difrp ⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 1 < 𝑁 ↔ ( 𝑁 − 1 ) ∈ ℝ+ ) )
30 20 24 29 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 1 < 𝑁 ↔ ( 𝑁 − 1 ) ∈ ℝ+ ) )
31 28 30 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝑁 − 1 ) ∈ ℝ+ )
32 neglt ⊢ ( ( 𝑁 − 1 ) ∈ ℝ+ → - ( 𝑁 − 1 ) < ( 𝑁 − 1 ) )
33 31 32 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → - ( 𝑁 − 1 ) < ( 𝑁 − 1 ) )
34 33 adantl ⊢ ( ( ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → - ( 𝑁 − 1 ) < ( 𝑁 − 1 ) )
35 19 34 eqbrtrd ⊢ ( ( ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) < ( 𝑁 − 1 ) )
36 iffalse ⊢ ( ¬ ( 𝐴 mod 𝑁 ) = 0 → if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = - 1 )
37 36 adantr ⊢ ( ( ¬ ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = - 1 )
38 37 negeqd ⊢ ( ( ¬ ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = - - 1 )
39 negneg1e1 ⊢ - - 1 = 1
40 df-2 ⊢ 2 = ( 1 + 1 )
41 40 breq1i ⊢ ( 2 < 𝑁 ↔ ( 1 + 1 ) < 𝑁 )
42 41 biimpi ⊢ ( 2 < 𝑁 → ( 1 + 1 ) < 𝑁 )
43 42 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 1 + 1 ) < 𝑁 )
44 20 20 24 ltaddsub2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 1 + 1 ) < 𝑁 ↔ 1 < ( 𝑁 − 1 ) ) )
45 43 44 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 1 < ( 𝑁 − 1 ) )
46 39 45 eqbrtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → - - 1 < ( 𝑁 − 1 ) )
47 46 adantl ⊢ ( ( ¬ ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → - - 1 < ( 𝑁 − 1 ) )
48 38 47 eqbrtrd ⊢ ( ( ¬ ( 𝐴 mod 𝑁 ) = 0 ∧ ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) ) → - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) < ( 𝑁 − 1 ) )
49 35 48 pm2.61ian ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → - if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) < ( 𝑁 − 1 ) )
50 16 49 eqbrtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 𝐴 mod 𝑁 ) − ( ( 𝐴 − 1 ) mod 𝑁 ) ) < ( 𝑁 − 1 ) )