Metamath Proof Explorer


Theorem modprminv

Description: Show an explicit expression for the modular inverse of A mod P . This is an application of prmdiv . (Contributed by Alexander van der Vekens, 15-May-2018)

Ref Expression
Hypothesis modprminv.1 R=AP2modP
Assertion modprminv PA¬PAR1P1ARmodP=1

Proof

Step Hyp Ref Expression
1 modprminv.1 R=AP2modP
2 1 prmdiv PA¬PAR1P1PAR1
3 elfzelz R1P1R
4 zmulcl ARAR
5 3 4 sylan2 AR1P1AR
6 modprm1div PARARmodP=1PAR1
7 5 6 sylan2 PAR1P1ARmodP=1PAR1
8 7 expr PAR1P1ARmodP=1PAR1
9 8 3adant3 PA¬PAR1P1ARmodP=1PAR1
10 9 pm5.32d PA¬PAR1P1ARmodP=1R1P1PAR1
11 2 10 mpbird PA¬PAR1P1ARmodP=1