Metamath Proof Explorer

Theorem fpprmod

Description: The set of Fermat pseudoprimes to the base N , expressed by a modulo operation instead of the divisibility relation. (Contributed by AV, 30-May-2023)

Ref Expression
Assertion fpprmod 
|- ( N e. NN -> ( FPPr ` N ) = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) } )

Proof

Step Hyp Ref Expression
1 fppr 
 |-  ( N e. NN -> ( FPPr ` N ) = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) } )
2 eluz4eluz2 
 |-  ( x e. ( ZZ>= ` 4 ) -> x e. ( ZZ>= ` 2 ) )
3 nnz 
 |-  ( N e. NN -> N e. ZZ )
4 eluz4nn 
 |-  ( x e. ( ZZ>= ` 4 ) -> x e. NN )
5 nnm1nn0 
 |-  ( x e. NN -> ( x - 1 ) e. NN0 )
6 4 5 syl 
 |-  ( x e. ( ZZ>= ` 4 ) -> ( x - 1 ) e. NN0 )
7 zexpcl 
 |-  ( ( N e. ZZ /\ ( x - 1 ) e. NN0 ) -> ( N ^ ( x - 1 ) ) e. ZZ )
8 3 6 7 syl2an 
 |-  ( ( N e. NN /\ x e. ( ZZ>= ` 4 ) ) -> ( N ^ ( x - 1 ) ) e. ZZ )
9 modm1div 
 |-  ( ( x e. ( ZZ>= ` 2 ) /\ ( N ^ ( x - 1 ) ) e. ZZ ) -> ( ( ( N ^ ( x - 1 ) ) mod x ) = 1 <-> x || ( ( N ^ ( x - 1 ) ) - 1 ) ) )
10 2 8 9 syl2an2 
 |-  ( ( N e. NN /\ x e. ( ZZ>= ` 4 ) ) -> ( ( ( N ^ ( x - 1 ) ) mod x ) = 1 <-> x || ( ( N ^ ( x - 1 ) ) - 1 ) ) )
11 10 bicomd 
 |-  ( ( N e. NN /\ x e. ( ZZ>= ` 4 ) ) -> ( x || ( ( N ^ ( x - 1 ) ) - 1 ) <-> ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) )
12 11 anbi2d 
 |-  ( ( N e. NN /\ x e. ( ZZ>= ` 4 ) ) -> ( ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) <-> ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) ) )
13 12 rabbidva 
 |-  ( N e. NN -> { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) } = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) } )
14 1 13 eqtrd 
 |-  ( N e. NN -> ( FPPr ` N ) = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) } )