Metamath Proof Explorer

Theorem modaddmodup

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

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

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( B e. ( ( M - ( A mod M ) ) ..^ M ) -> B e. ZZ )
2 1 zred 
 |-  ( B e. ( ( M - ( A mod M ) ) ..^ M ) -> B e. RR )
3 2 adantr 
 |-  ( ( B e. ( ( M - ( A mod M ) ) ..^ 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. ( ( M - ( A mod M ) ) ..^ M ) /\ ( A e. ZZ /\ M e. NN ) ) -> ( A mod M ) e. RR )
7 3 6 readdcld 
 |-  ( ( B e. ( ( M - ( A mod M ) ) ..^ M ) /\ ( A e. ZZ /\ M e. NN ) ) -> ( B + ( A mod M ) ) e. RR )
8 7 ancoms 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ 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. ( ( M - ( A mod M ) ) ..^ M ) ) -> M e. RR+ )
11 elfzo2 
 |-  ( B e. ( ( M - ( A mod M ) ) ..^ M ) <-> ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) /\ M e. ZZ /\ B < M ) )
12 eluz2 
 |-  ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) <-> ( ( M - ( A mod M ) ) e. ZZ /\ B e. ZZ /\ ( M - ( A mod M ) ) <_ B ) )
13 nnre 
 |-  ( M e. NN -> M e. RR )
14 13 adantl 
 |-  ( ( A e. ZZ /\ M e. NN ) -> M e. RR )
15 14 adantl 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> M e. RR )
16 5 adantl 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> ( A mod M ) e. RR )
17 zre 
 |-  ( B e. ZZ -> B e. RR )
18 17 adantr 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> B e. RR )
19 15 16 18 lesubaddd 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> ( ( M - ( A mod M ) ) <_ B <-> M <_ ( B + ( A mod M ) ) ) )
20 19 biimpd 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> ( ( M - ( A mod M ) ) <_ B -> M <_ ( B + ( A mod M ) ) ) )
21 20 impancom 
 |-  ( ( B e. ZZ /\ ( M - ( A mod M ) ) <_ B ) -> ( ( A e. ZZ /\ M e. NN ) -> M <_ ( B + ( A mod M ) ) ) )
22 21 3adant1 
 |-  ( ( ( M - ( A mod M ) ) e. ZZ /\ B e. ZZ /\ ( M - ( A mod M ) ) <_ B ) -> ( ( A e. ZZ /\ M e. NN ) -> M <_ ( B + ( A mod M ) ) ) )
23 12 22 sylbi 
 |-  ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) -> ( ( A e. ZZ /\ M e. NN ) -> M <_ ( B + ( A mod M ) ) ) )
24 23 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) /\ M e. ZZ /\ B < M ) -> ( ( A e. ZZ /\ M e. NN ) -> M <_ ( B + ( A mod M ) ) ) )
25 11 24 sylbi 
 |-  ( B e. ( ( M - ( A mod M ) ) ..^ M ) -> ( ( A e. ZZ /\ M e. NN ) -> M <_ ( B + ( A mod M ) ) ) )
26 25 impcom 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> M <_ ( B + ( A mod M ) ) )
27 eluzelz 
 |-  ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) -> B e. ZZ )
28 17 5 anim12i 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> ( B e. RR /\ ( A mod M ) e. RR ) )
29 13 13 jca 
 |-  ( M e. NN -> ( M e. RR /\ M e. RR ) )
30 29 adantl 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( M e. RR /\ M e. RR ) )
31 30 adantl 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> ( M e. RR /\ M e. RR ) )
32 28 31 jca 
 |-  ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) -> ( ( B e. RR /\ ( A mod M ) e. RR ) /\ ( M e. RR /\ M e. RR ) ) )
33 32 adantr 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> ( ( B e. RR /\ ( A mod M ) e. RR ) /\ ( M e. RR /\ M e. RR ) ) )
34 simpr 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> B < M )
35 zre 
 |-  ( A e. ZZ -> A e. RR )
36 modlt 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) < M )
37 35 9 36 syl2an 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( A mod M ) < M )
38 5 14 37 ltled 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( A mod M ) <_ M )
39 38 ad2antlr 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> ( A mod M ) <_ M )
40 34 39 jca 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> ( B < M /\ ( A mod M ) <_ M ) )
41 ltleadd 
 |-  ( ( ( B e. RR /\ ( A mod M ) e. RR ) /\ ( M e. RR /\ M e. RR ) ) -> ( ( B < M /\ ( A mod M ) <_ M ) -> ( B + ( A mod M ) ) < ( M + M ) ) )
42 33 40 41 sylc 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> ( B + ( A mod M ) ) < ( M + M ) )
43 nncn 
 |-  ( M e. NN -> M e. CC )
44 43 2timesd 
 |-  ( M e. NN -> ( 2 x. M ) = ( M + M ) )
45 44 adantl 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( 2 x. M ) = ( M + M ) )
46 45 ad2antlr 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> ( 2 x. M ) = ( M + M ) )
47 42 46 breqtrrd 
 |-  ( ( ( B e. ZZ /\ ( A e. ZZ /\ M e. NN ) ) /\ B < M ) -> ( B + ( A mod M ) ) < ( 2 x. M ) )
48 47 exp31 
 |-  ( B e. ZZ -> ( ( A e. ZZ /\ M e. NN ) -> ( B < M -> ( B + ( A mod M ) ) < ( 2 x. M ) ) ) )
49 48 com23 
 |-  ( B e. ZZ -> ( B < M -> ( ( A e. ZZ /\ M e. NN ) -> ( B + ( A mod M ) ) < ( 2 x. M ) ) ) )
50 27 49 syl 
 |-  ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) -> ( B < M -> ( ( A e. ZZ /\ M e. NN ) -> ( B + ( A mod M ) ) < ( 2 x. M ) ) ) )
51 50 imp 
 |-  ( ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) /\ B < M ) -> ( ( A e. ZZ /\ M e. NN ) -> ( B + ( A mod M ) ) < ( 2 x. M ) ) )
52 51 3adant2 
 |-  ( ( B e. ( ZZ>= ` ( M - ( A mod M ) ) ) /\ M e. ZZ /\ B < M ) -> ( ( A e. ZZ /\ M e. NN ) -> ( B + ( A mod M ) ) < ( 2 x. M ) ) )
53 11 52 sylbi 
 |-  ( B e. ( ( M - ( A mod M ) ) ..^ M ) -> ( ( A e. ZZ /\ M e. NN ) -> ( B + ( A mod M ) ) < ( 2 x. M ) ) )
54 53 impcom 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> ( B + ( A mod M ) ) < ( 2 x. M ) )
55 2submod 
 |-  ( ( ( ( B + ( A mod M ) ) e. RR /\ M e. RR+ ) /\ ( M <_ ( B + ( A mod M ) ) /\ ( B + ( A mod M ) ) < ( 2 x. M ) ) ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( B + ( A mod M ) ) - M ) )
56 55 eqcomd 
 |-  ( ( ( ( B + ( A mod M ) ) e. RR /\ M e. RR+ ) /\ ( M <_ ( B + ( A mod M ) ) /\ ( B + ( A mod M ) ) < ( 2 x. M ) ) ) -> ( ( B + ( A mod M ) ) - M ) = ( ( B + ( A mod M ) ) mod M ) )
57 8 10 26 54 56 syl22anc 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> ( ( B + ( A mod M ) ) - M ) = ( ( B + ( A mod M ) ) mod M ) )
58 35 adantr 
 |-  ( ( A e. ZZ /\ M e. NN ) -> A e. RR )
59 58 adantr 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> A e. RR )
60 2 adantl 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> B e. RR )
61 modadd2mod 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( B + A ) mod M ) )
62 59 60 10 61 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( B + A ) mod M ) )
63 57 62 eqtrd 
 |-  ( ( ( A e. ZZ /\ M e. NN ) /\ B e. ( ( M - ( A mod M ) ) ..^ M ) ) -> ( ( B + ( A mod M ) ) - M ) = ( ( B + A ) mod M ) )
64 63 ex 
 |-  ( ( A e. ZZ /\ M e. NN ) -> ( B e. ( ( M - ( A mod M ) ) ..^ M ) -> ( ( B + ( A mod M ) ) - M ) = ( ( B + A ) mod M ) ) )