Description: A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018) (Proof shortened by AV, 30-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | modprm1div | |- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 1 <-> P || ( A - 1 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prmuz2 | |- ( P e. Prime -> P e. ( ZZ>= ` 2 ) ) |
|
| 2 | modm1div | |- ( ( P e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A mod P ) = 1 <-> P || ( A - 1 ) ) ) |
|
| 3 | 1 2 | sylan | |- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 1 <-> P || ( A - 1 ) ) ) |