Metamath Proof Explorer


Theorem dfwppr

Description: Alternate definition of aweak pseudoprime X , which fulfils ( N ^ X ) == N (modulo X ), see Wikipedia "Fermat pseudoprime", https://en.wikipedia.org/wiki/Fermat_pseudoprime , 29-May-2023. (Contributed by AV, 31-May-2023)

Ref Expression
Assertion dfwppr N X N X mod X = N mod X X N X N

Proof

Step Hyp Ref Expression
1 simpr N X X
2 nnz N N
3 nnnn0 X X 0
4 zexpcl N X 0 N X
5 2 3 4 syl2an N X N X
6 2 adantr N X N
7 moddvds X N X N N X mod X = N mod X X N X N
8 1 5 6 7 syl3anc N X N X mod X = N mod X X N X N