Metamath Proof Explorer

Theorem modltm1p1mod

Description: If a real number modulo a positive real number is less than the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals the real number modulo the positive real number increased by 1. (Contributed by AV, 2-Nov-2018)

Ref Expression
Assertion modltm1p1mod 
|- ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( ( A + 1 ) mod M ) = ( ( A mod M ) + 1 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> A e. RR )
2 1red 
 |-  ( ( A e. RR /\ M e. RR+ ) -> 1 e. RR )
3 simpr 
 |-  ( ( A e. RR /\ M e. RR+ ) -> M e. RR+ )
4 1 2 3 3jca 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A e. RR /\ 1 e. RR /\ M e. RR+ ) )
5 4 3adant3 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( A e. RR /\ 1 e. RR /\ M e. RR+ ) )
6 modaddmod 
 |-  ( ( A e. RR /\ 1 e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( ( A + 1 ) mod M ) )
7 5 6 syl 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( ( A + 1 ) mod M ) )
8 modcl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )
9 peano2re 
 |-  ( ( A mod M ) e. RR -> ( ( A mod M ) + 1 ) e. RR )
10 8 9 syl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) + 1 ) e. RR )
11 10 3 jca 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) + 1 ) e. RR /\ M e. RR+ ) )
12 11 3adant3 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( ( ( A mod M ) + 1 ) e. RR /\ M e. RR+ ) )
13 0red 
 |-  ( ( A e. RR /\ M e. RR+ ) -> 0 e. RR )
14 modge0 
 |-  ( ( A e. RR /\ M e. RR+ ) -> 0 <_ ( A mod M ) )
15 8 lep1d 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) <_ ( ( A mod M ) + 1 ) )
16 13 8 10 14 15 letrd 
 |-  ( ( A e. RR /\ M e. RR+ ) -> 0 <_ ( ( A mod M ) + 1 ) )
17 16 3adant3 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> 0 <_ ( ( A mod M ) + 1 ) )
18 rpre 
 |-  ( M e. RR+ -> M e. RR )
19 18 adantl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> M e. RR )
20 8 2 19 ltaddsubd 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) + 1 ) < M <-> ( A mod M ) < ( M - 1 ) ) )
21 20 biimp3ar 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( ( A mod M ) + 1 ) < M )
22 modid 
 |-  ( ( ( ( ( A mod M ) + 1 ) e. RR /\ M e. RR+ ) /\ ( 0 <_ ( ( A mod M ) + 1 ) /\ ( ( A mod M ) + 1 ) < M ) ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( ( A mod M ) + 1 ) )
23 12 17 21 22 syl12anc 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( ( A mod M ) + 1 ) )
24 7 23 eqtr3d 
 |-  ( ( A e. RR /\ M e. RR+ /\ ( A mod M ) < ( M - 1 ) ) -> ( ( A + 1 ) mod M ) = ( ( A mod M ) + 1 ) )