Metamath Proof Explorer

Theorem modaddmodlo

Description: The sum of an integer modulo a positive integer and another integer equals the sum of the two integers modulo the positive integer if the other integer is in the lower part of the range between 0 and the positive integer. (Contributed by AV, 30-Oct-2018)

Ref Expression
Assertion modaddmodlo 
|- ( ( A e. ZZ /\ M e. NN ) -> ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) -> ( B + ( A mod M ) ) = ( ( B + A ) mod M ) ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) -> B e. ZZ )
2 1 zred 
 |-  ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) -> B e. RR )
3 2 adantr 
 |-  ( ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) /\ ( A e. ZZ /\ M e. NN ) ) -> B e. RR )
4 zmodcl 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( A mod M ) e. NN0 )
5 4 nn0red 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( A mod M ) e. RR )
6 5 adantl 
 |-  ( ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) /\ ( A e. ZZ /\ M e. NN ) ) -> ( A mod M ) e. RR )
7 3 6 readdcld 
 |-  ( ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) /\ ( A e. ZZ /\ M e. NN ) ) -> ( B + ( A mod M ) ) e. RR )
8 7 ancoms 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( B + ( A mod M ) ) e. RR )
9 nnrp 
 |-  ( M e. NN -> M e. RR+ )
10 9 ad2antlr 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> M e. RR+ )
11 2 adantl 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> B e. RR )
12 5 adantr 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( A mod M ) e. RR )
13 elfzole1 
 |-  ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) -> 0 <_ B )
14 13 adantl 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> 0 <_ B )
15 4 nn0ge0d 
 |-  ( ( A e. ZZ /\ M e. NN ) -> 0 <_ ( A mod M ) )
16 15 adantr 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> 0 <_ ( A mod M ) )
17 11 12 14 16 addge0d 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> 0 <_ ( B + ( A mod M ) ) )
18 elfzolt2 
 |-  ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) -> B < ( M - ( A mod M ) ) )
19 18 adantl 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> B < ( M - ( A mod M ) ) )
20 nnre 
 |-  ( M e. NN -> M e. RR )
21 20 ad2antlr 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> M e. RR )
22 11 12 21 ltaddsubd 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( ( B + ( A mod M ) ) < M <-> B < ( M - ( A mod M ) ) ) )
23 19 22 mpbird 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( B + ( A mod M ) ) < M )
24 modid 
 |-  ( ( ( ( B + ( A mod M ) ) e. RR /\ M e. RR+ ) /\ ( 0 <_ ( B + ( A mod M ) ) /\ ( B + ( A mod M ) ) < M ) ) -> ( ( B + ( A mod M ) ) mod M ) = ( B + ( A mod M ) ) )
25 8 10 17 23 24 syl22anc 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( ( B + ( A mod M ) ) mod M ) = ( B + ( A mod M ) ) )
26 zre 
 |-  ( A e. ZZ -> A e. RR )
27 26 adantr 
 |-  ( ( A e. ZZ /\ M e. NN ) -> A e. RR )
28 27 adantr 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> A e. RR )
29 modadd2mod 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( B + A ) mod M ) )
30 28 11 10 29 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( B + A ) mod M ) )
31 25 30 eqtr3d 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( 0 ..^ ( M - ( A mod M ) ) ) ) -> ( B + ( A mod M ) ) = ( ( B + A ) mod M ) )
32 31 ex 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( B e. ( 0 ..^ ( M - ( A mod M ) ) ) -> ( B + ( A mod M ) ) = ( ( B + A ) mod M ) ) )