Metamath Proof Explorer

Theorem m1mod0mod1

Description: An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020)

Ref Expression
Assertion m1mod0mod1 
|- ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( ( A - 1 ) mod N ) = 0 <-> ( A mod N ) = 1 ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 npcan1 
 |-  ( A e. CC -> ( ( A - 1 ) + 1 ) = A )
3 2 eqcomd 
 |-  ( A e. CC -> A = ( ( A - 1 ) + 1 ) )
4 1 3 syl 
 |-  ( A e. RR -> A = ( ( A - 1 ) + 1 ) )
5 4 3ad2ant1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> A = ( ( A - 1 ) + 1 ) )
6 5 adantr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> A = ( ( A - 1 ) + 1 ) )
7 6 oveq1d 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( A mod N ) = ( ( ( A - 1 ) + 1 ) mod N ) )
8 simpr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( A - 1 ) mod N ) = 0 )
9 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
10 9 3adant1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
11 10 adantr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( 1 mod N ) = 1 )
12 8 11 oveq12d 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( ( A - 1 ) mod N ) + ( 1 mod N ) ) = ( 0 + 1 ) )
13 12 oveq1d 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( ( ( A - 1 ) mod N ) + ( 1 mod N ) ) mod N ) = ( ( 0 + 1 ) mod N ) )
14 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
15 14 3ad2ant1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( A - 1 ) e. RR )
16 1red 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> 1 e. RR )
17 simpl 
 |-  ( ( N e. RR /\ 1 < N ) -> N e. RR )
18 0lt1 
 |-  0 < 1
19 0re 
 |-  0 e. RR
20 1re 
 |-  1 e. RR
21 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( 0 < 1 /\ 1 < N ) -> 0 < N ) )
22 19 20 21 mp3an12 
 |-  ( N e. RR -> ( ( 0 < 1 /\ 1 < N ) -> 0 < N ) )
23 18 22 mpani 
 |-  ( N e. RR -> ( 1 < N -> 0 < N ) )
24 23 imp 
 |-  ( ( N e. RR /\ 1 < N ) -> 0 < N )
25 17 24 elrpd 
 |-  ( ( N e. RR /\ 1 < N ) -> N e. RR+ )
26 25 3adant1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> N e. RR+ )
27 15 16 26 3jca 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( A - 1 ) e. RR /\ 1 e. RR /\ N e. RR+ ) )
28 27 adantr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( A - 1 ) e. RR /\ 1 e. RR /\ N e. RR+ ) )
29 modaddabs 
 |-  ( ( ( A - 1 ) e. RR /\ 1 e. RR /\ N e. RR+ ) -> ( ( ( ( A - 1 ) mod N ) + ( 1 mod N ) ) mod N ) = ( ( ( A - 1 ) + 1 ) mod N ) )
30 28 29 syl 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( ( ( A - 1 ) mod N ) + ( 1 mod N ) ) mod N ) = ( ( ( A - 1 ) + 1 ) mod N ) )
31 0p1e1 
 |-  ( 0 + 1 ) = 1
32 31 oveq1i 
 |-  ( ( 0 + 1 ) mod N ) = ( 1 mod N )
33 32 9 syl5eq 
 |-  ( ( N e. RR /\ 1 < N ) -> ( ( 0 + 1 ) mod N ) = 1 )
34 33 3adant1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( 0 + 1 ) mod N ) = 1 )
35 34 adantr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( 0 + 1 ) mod N ) = 1 )
36 13 30 35 3eqtr3d 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( ( ( A - 1 ) + 1 ) mod N ) = 1 )
37 7 36 eqtrd 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( ( A - 1 ) mod N ) = 0 ) -> ( A mod N ) = 1 )
38 simpr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( A mod N ) = 1 ) -> ( A mod N ) = 1 )
39 38 eqcomd 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( A mod N ) = 1 ) -> 1 = ( A mod N ) )
40 39 oveq2d 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( A mod N ) = 1 ) -> ( A - 1 ) = ( A - ( A mod N ) ) )
41 40 oveq1d 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( A mod N ) = 1 ) -> ( ( A - 1 ) mod N ) = ( ( A - ( A mod N ) ) mod N ) )
42 simp1 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> A e. RR )
43 42 26 modcld 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( A mod N ) e. RR )
44 43 recnd 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( A mod N ) e. CC )
45 44 subidd 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( A mod N ) - ( A mod N ) ) = 0 )
46 45 oveq1d 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( ( A mod N ) - ( A mod N ) ) mod N ) = ( 0 mod N ) )
47 modsubmod 
 |-  ( ( A e. RR /\ ( A mod N ) e. RR /\ N e. RR+ ) -> ( ( ( A mod N ) - ( A mod N ) ) mod N ) = ( ( A - ( A mod N ) ) mod N ) )
48 42 43 26 47 syl3anc 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( ( A mod N ) - ( A mod N ) ) mod N ) = ( ( A - ( A mod N ) ) mod N ) )
49 0mod 
 |-  ( N e. RR+ -> ( 0 mod N ) = 0 )
50 26 49 syl 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( 0 mod N ) = 0 )
51 46 48 50 3eqtr3d 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( A - ( A mod N ) ) mod N ) = 0 )
52 51 adantr 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( A mod N ) = 1 ) -> ( ( A - ( A mod N ) ) mod N ) = 0 )
53 41 52 eqtrd 
 |-  ( ( ( A e. RR /\ N e. RR /\ 1 < N ) /\ ( A mod N ) = 1 ) -> ( ( A - 1 ) mod N ) = 0 )
54 37 53 impbida 
 |-  ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( ( A - 1 ) mod N ) = 0 <-> ( A mod N ) = 1 ) )