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 
|- ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( ( A - B ) mod N ) = ( ( N + A ) - B ) )

Proof

Step Hyp Ref Expression
1 elfzoel2 
 |-  ( A e. ( 0 ..^ B ) -> B e. ZZ )
2 1 zcnd 
 |-  ( A e. ( 0 ..^ B ) -> B e. CC )
3 elfzoelz 
 |-  ( A e. ( 0 ..^ B ) -> A e. ZZ )
4 3 zcnd 
 |-  ( A e. ( 0 ..^ B ) -> A e. CC )
5 2 4 jca 
 |-  ( A e. ( 0 ..^ B ) -> ( B e. CC /\ A e. CC ) )
6 5 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( B e. CC /\ A e. CC ) )
7 negsubdi2 
 |-  ( ( B e. CC /\ A e. CC ) -> -u ( B - A ) = ( A - B ) )
8 6 7 syl 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> -u ( B - A ) = ( A - B ) )
9 8 eqcomd 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( A - B ) = -u ( B - A ) )
10 9 oveq1d 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( ( A - B ) mod N ) = ( -u ( B - A ) mod N ) )
11 1 3 zsubcld 
 |-  ( A e. ( 0 ..^ B ) -> ( B - A ) e. ZZ )
12 11 zred 
 |-  ( A e. ( 0 ..^ B ) -> ( B - A ) e. RR )
13 12 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( B - A ) e. RR )
14 nnrp 
 |-  ( N e. NN -> N e. RR+ )
15 14 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> N e. RR+ )
16 negmod 
 |-  ( ( ( B - A ) e. RR /\ N e. RR+ ) -> ( -u ( B - A ) mod N ) = ( ( N - ( B - A ) ) mod N ) )
17 13 15 16 syl2anc 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( -u ( B - A ) mod N ) = ( ( N - ( B - A ) ) mod N ) )
18 10 17 eqtrd 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( ( A - B ) mod N ) = ( ( N - ( B - A ) ) mod N ) )
19 nnz 
 |-  ( N e. NN -> N e. ZZ )
20 19 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> N e. ZZ )
21 11 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( B - A ) e. ZZ )
22 20 21 zsubcld 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( N - ( B - A ) ) e. ZZ )
23 22 zred 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( N - ( B - A ) ) e. RR )
24 1 zred 
 |-  ( A e. ( 0 ..^ B ) -> B e. RR )
25 24 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> B e. RR )
26 nnre 
 |-  ( N e. NN -> N e. RR )
27 26 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> N e. RR )
28 elfzo0suble 
 |-  ( A e. ( 0 ..^ B ) -> ( B - A ) <_ B )
29 28 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( B - A ) <_ B )
30 simp3 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> B < N )
31 leltletr 
 |-  ( ( ( B - A ) e. RR /\ B e. RR /\ N e. RR ) -> ( ( ( B - A ) <_ B /\ B < N ) -> ( B - A ) <_ N ) )
32 31 imp 
 |-  ( ( ( ( B - A ) e. RR /\ B e. RR /\ N e. RR ) /\ ( ( B - A ) <_ B /\ B < N ) ) -> ( B - A ) <_ N )
33 13 25 27 29 30 32 syl32anc 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( B - A ) <_ N )
34 27 13 subge0d 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( 0 <_ ( N - ( B - A ) ) <-> ( B - A ) <_ N ) )
35 33 34 mpbird 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> 0 <_ ( N - ( B - A ) ) )
36 elfzo0 
 |-  ( A e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. NN /\ A < B ) )
37 nn0re 
 |-  ( A e. NN0 -> A e. RR )
38 nnre 
 |-  ( B e. NN -> B e. RR )
39 posdif 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )
40 37 38 39 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A < B <-> 0 < ( B - A ) ) )
41 40 biimp3a 
 |-  ( ( A e. NN0 /\ B e. NN /\ A < B ) -> 0 < ( B - A ) )
42 36 41 sylbi 
 |-  ( A e. ( 0 ..^ B ) -> 0 < ( B - A ) )
43 42 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> 0 < ( B - A ) )
44 13 27 ltsubposd 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( 0 < ( B - A ) <-> ( N - ( B - A ) ) < N ) )
45 43 44 mpbid 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( N - ( B - A ) ) < N )
46 modid 
 |-  ( ( ( ( N - ( B - A ) ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( N - ( B - A ) ) /\ ( N - ( B - A ) ) < N ) ) -> ( ( N - ( B - A ) ) mod N ) = ( N - ( B - A ) ) )
47 23 15 35 45 46 syl22anc 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( ( N - ( B - A ) ) mod N ) = ( N - ( B - A ) ) )
48 nncn 
 |-  ( N e. NN -> N e. CC )
49 48 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> N e. CC )
50 2 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> B e. CC )
51 4 3ad2ant2 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> A e. CC )
52 49 50 51 subsub3d 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( N - ( B - A ) ) = ( ( N + A ) - B ) )
53 18 47 52 3eqtrd 
 |-  ( ( N e. NN /\ A e. ( 0 ..^ B ) /\ B < N ) -> ( ( A - B ) mod N ) = ( ( N + A ) - B ) )