Metamath Proof Explorer

Theorem p1modz1

Description: If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022)

Ref Expression
Assertion p1modz1 
|- ( ( M || A /\ 1 < M ) -> ( ( A + 1 ) mod M ) = 1 )

Proof

Step Hyp Ref Expression
1 dvdszrcl 
 |-  ( M || A -> ( M e. ZZ /\ A e. ZZ ) )
2 0red 
 |-  ( ( M e. ZZ /\ 1 < M ) -> 0 e. RR )
3 1red 
 |-  ( ( M e. ZZ /\ 1 < M ) -> 1 e. RR )
4 zre 
 |-  ( M e. ZZ -> M e. RR )
5 4 adantr 
 |-  ( ( M e. ZZ /\ 1 < M ) -> M e. RR )
6 2 3 5 3jca 
 |-  ( ( M e. ZZ /\ 1 < M ) -> ( 0 e. RR /\ 1 e. RR /\ M e. RR ) )
7 0lt1 
 |-  0 < 1
8 7 a1i 
 |-  ( M e. ZZ -> 0 < 1 )
9 8 anim1i 
 |-  ( ( M e. ZZ /\ 1 < M ) -> ( 0 < 1 /\ 1 < M ) )
10 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ M e. RR ) -> ( ( 0 < 1 /\ 1 < M ) -> 0 < M ) )
11 6 9 10 sylc 
 |-  ( ( M e. ZZ /\ 1 < M ) -> 0 < M )
12 11 ex 
 |-  ( M e. ZZ -> ( 1 < M -> 0 < M ) )
13 elnnz 
 |-  ( M e. NN <-> ( M e. ZZ /\ 0 < M ) )
14 13 simplbi2 
 |-  ( M e. ZZ -> ( 0 < M -> M e. NN ) )
15 12 14 syld 
 |-  ( M e. ZZ -> ( 1 < M -> M e. NN ) )
16 15 adantr 
 |-  ( ( M e. ZZ /\ A e. ZZ ) -> ( 1 < M -> M e. NN ) )
17 16 imp 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> M e. NN )
18 dvdsmod0 
 |-  ( ( M e. NN /\ M || A ) -> ( A mod M ) = 0 )
19 17 18 sylan 
 |-  ( ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) /\ M || A ) -> ( A mod M ) = 0 )
20 19 ex 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> ( M || A -> ( A mod M ) = 0 ) )
21 oveq1 
 |-  ( ( A mod M ) = 0 -> ( ( A mod M ) + 1 ) = ( 0 + 1 ) )
22 0p1e1 
 |-  ( 0 + 1 ) = 1
23 21 22 eqtrdi 
 |-  ( ( A mod M ) = 0 -> ( ( A mod M ) + 1 ) = 1 )
24 23 oveq1d 
 |-  ( ( A mod M ) = 0 -> ( ( ( A mod M ) + 1 ) mod M ) = ( 1 mod M ) )
25 24 adantl 
 |-  ( ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) /\ ( A mod M ) = 0 ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( 1 mod M ) )
26 zre 
 |-  ( A e. ZZ -> A e. RR )
27 26 adantl 
 |-  ( ( M e. ZZ /\ A e. ZZ ) -> A e. RR )
28 27 adantr 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> A e. RR )
29 1red 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> 1 e. RR )
30 17 nnrpd 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> M e. RR+ )
31 28 29 30 3jca 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> ( A e. RR /\ 1 e. RR /\ M e. RR+ ) )
32 31 adantr 
 |-  ( ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) /\ ( A mod M ) = 0 ) -> ( A e. RR /\ 1 e. RR /\ M e. RR+ ) )
33 modaddmod 
 |-  ( ( A e. RR /\ 1 e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( ( A + 1 ) mod M ) )
34 32 33 syl 
 |-  ( ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) /\ ( A mod M ) = 0 ) -> ( ( ( A mod M ) + 1 ) mod M ) = ( ( A + 1 ) mod M ) )
35 4 adantr 
 |-  ( ( M e. ZZ /\ A e. ZZ ) -> M e. RR )
36 1mod 
 |-  ( ( M e. RR /\ 1 < M ) -> ( 1 mod M ) = 1 )
37 35 36 sylan 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> ( 1 mod M ) = 1 )
38 37 adantr 
 |-  ( ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) /\ ( A mod M ) = 0 ) -> ( 1 mod M ) = 1 )
39 25 34 38 3eqtr3d 
 |-  ( ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) /\ ( A mod M ) = 0 ) -> ( ( A + 1 ) mod M ) = 1 )
40 39 ex 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> ( ( A mod M ) = 0 -> ( ( A + 1 ) mod M ) = 1 ) )
41 20 40 syld 
 |-  ( ( ( M e. ZZ /\ A e. ZZ ) /\ 1 < M ) -> ( M || A -> ( ( A + 1 ) mod M ) = 1 ) )
42 41 ex 
 |-  ( ( M e. ZZ /\ A e. ZZ ) -> ( 1 < M -> ( M || A -> ( ( A + 1 ) mod M ) = 1 ) ) )
43 42 com23 
 |-  ( ( M e. ZZ /\ A e. ZZ ) -> ( M || A -> ( 1 < M -> ( ( A + 1 ) mod M ) = 1 ) ) )
44 1 43 mpcom 
 |-  ( M || A -> ( 1 < M -> ( ( A + 1 ) mod M ) = 1 ) )
45 44 imp 
 |-  ( ( M || A /\ 1 < M ) -> ( ( A + 1 ) mod M ) = 1 )