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 e. NN /\ X e. NN ) -> ( ( ( N ^ X ) mod X ) = ( N mod X ) <-> X || ( ( N ^ X ) - N ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( N e. NN /\ X e. NN ) -> X e. NN )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 nnnn0 
 |-  ( X e. NN -> X e. NN0 )
4 zexpcl 
 |-  ( ( N e. ZZ /\ X e. NN0 ) -> ( N ^ X ) e. ZZ )
5 2 3 4 syl2an 
 |-  ( ( N e. NN /\ X e. NN ) -> ( N ^ X ) e. ZZ )
6 2 adantr 
 |-  ( ( N e. NN /\ X e. NN ) -> N e. ZZ )
7 moddvds 
 |-  ( ( X e. NN /\ ( N ^ X ) e. ZZ /\ N e. ZZ ) -> ( ( ( N ^ X ) mod X ) = ( N mod X ) <-> X || ( ( N ^ X ) - N ) ) )
8 1 5 6 7 syl3anc 
 |-  ( ( N e. NN /\ X e. NN ) -> ( ( ( N ^ X ) mod X ) = ( N mod X ) <-> X || ( ( N ^ X ) - N ) ) )