Metamath Proof Explorer


Theorem modprm1div

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 PAAmodP=1PA1

Proof

Step Hyp Ref Expression
1 prmuz2 PP2
2 modm1div P2AAmodP=1PA1
3 1 2 sylan PAAmodP=1PA1