Metamath Proof Explorer

Theorem submodlt

Description: The difference of an element of a half-open range of nonnegative integers and the upper bound of this range modulo an integer greater than the upper bound. (Contributed by AV, 1-Sep-2025)

Ref Expression
Assertion submodlt ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( ( 𝑁 + 𝐴 ) − 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elfzoel2 ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐵 ∈ ℤ )
2 1 zcnd ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐵 ∈ ℂ )
3 elfzoelz ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐴 ∈ ℤ )
4 3 zcnd ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐴 ∈ ℂ )
5 2 4 jca ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
6 5 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
7 negsubdi2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → - ( 𝐵 − 𝐴 ) = ( 𝐴 − 𝐵 ) )
8 6 7 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → - ( 𝐵 − 𝐴 ) = ( 𝐴 − 𝐵 ) )
9 8 eqcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝐴 − 𝐵 ) = - ( 𝐵 − 𝐴 ) )
10 9 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( - ( 𝐵 − 𝐴 ) mod 𝑁 ) )
11 1 3 zsubcld ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
12 11 zred ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
13 12 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
14 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
15 14 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝑁 ∈ ℝ+ )
16 negmod ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( - ( 𝐵 − 𝐴 ) mod 𝑁 ) = ( ( 𝑁 − ( 𝐵 − 𝐴 ) ) mod 𝑁 ) )
17 13 15 16 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( - ( 𝐵 − 𝐴 ) mod 𝑁 ) = ( ( 𝑁 − ( 𝐵 − 𝐴 ) ) mod 𝑁 ) )
18 10 17 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( ( 𝑁 − ( 𝐵 − 𝐴 ) ) mod 𝑁 ) )
19 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
20 19 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝑁 ∈ ℤ )
21 11 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
22 20 21 zsubcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝑁 − ( 𝐵 − 𝐴 ) ) ∈ ℤ )
23 22 zred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝑁 − ( 𝐵 − 𝐴 ) ) ∈ ℝ )
24 1 zred ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐵 ∈ ℝ )
25 24 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝐵 ∈ ℝ )
26 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
27 26 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝑁 ∈ ℝ )
28 elfzo0suble ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( 𝐵 − 𝐴 ) ≤ 𝐵 )
29 28 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝐵 − 𝐴 ) ≤ 𝐵 )
30 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝐵 < 𝑁 )
31 leltletr ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝐵 − 𝐴 ) ≤ 𝐵 ∧ 𝐵 < 𝑁 ) → ( 𝐵 − 𝐴 ) ≤ 𝑁 ) )
32 31 imp ⊢ ( ( ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ ( ( 𝐵 − 𝐴 ) ≤ 𝐵 ∧ 𝐵 < 𝑁 ) ) → ( 𝐵 − 𝐴 ) ≤ 𝑁 )
33 13 25 27 29 30 32 syl32anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝐵 − 𝐴 ) ≤ 𝑁 )
34 27 13 subge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 0 ≤ ( 𝑁 − ( 𝐵 − 𝐴 ) ) ↔ ( 𝐵 − 𝐴 ) ≤ 𝑁 ) )
35 33 34 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 0 ≤ ( 𝑁 − ( 𝐵 − 𝐴 ) ) )
36 elfzo0 ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) )
37 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
38 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
39 posdif ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
40 37 38 39 syl2an ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
41 40 biimp3a ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → 0 < ( 𝐵 − 𝐴 ) )
42 36 41 sylbi ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 0 < ( 𝐵 − 𝐴 ) )
43 42 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 0 < ( 𝐵 − 𝐴 ) )
44 13 27 ltsubposd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 0 < ( 𝐵 − 𝐴 ) ↔ ( 𝑁 − ( 𝐵 − 𝐴 ) ) < 𝑁 ) )
45 43 44 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝑁 − ( 𝐵 − 𝐴 ) ) < 𝑁 )
46 modid ⊢ ( ( ( ( 𝑁 − ( 𝐵 − 𝐴 ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑁 − ( 𝐵 − 𝐴 ) ) ∧ ( 𝑁 − ( 𝐵 − 𝐴 ) ) < 𝑁 ) ) → ( ( 𝑁 − ( 𝐵 − 𝐴 ) ) mod 𝑁 ) = ( 𝑁 − ( 𝐵 − 𝐴 ) ) )
47 23 15 35 45 46 syl22anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( ( 𝑁 − ( 𝐵 − 𝐴 ) ) mod 𝑁 ) = ( 𝑁 − ( 𝐵 − 𝐴 ) ) )
48 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
49 48 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝑁 ∈ ℂ )
50 2 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝐵 ∈ ℂ )
51 4 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → 𝐴 ∈ ℂ )
52 49 50 51 subsub3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( 𝑁 − ( 𝐵 − 𝐴 ) ) = ( ( 𝑁 + 𝐴 ) − 𝐵 ) )
53 18 47 52 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ 𝐵 < 𝑁 ) → ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( ( 𝑁 + 𝐴 ) − 𝐵 ) )