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 | |
|
Assertion | modprminv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | modprminv.1 | |
|
2 | 1 | prmdiv | |
3 | elfzelz | |
|
4 | zmulcl | |
|
5 | 3 4 | sylan2 | |
6 | modprm1div | |
|
7 | 5 6 | sylan2 | |
8 | 7 | expr | |
9 | 8 | 3adant3 | |
10 | 9 | pm5.32d | |
11 | 2 10 | mpbird | |