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

Proof

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