Metamath Proof Explorer

Theorem fpprel

Description: A Fermat pseudoprime to the base N . (Contributed by AV, 30-May-2023)

Ref Expression
Assertion fpprel 
|- ( N e. NN -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 fpprmod 
 |-  ( N e. NN -> ( FPPr ` N ) = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) } )
2 1 eleq2d 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) <-> X e. { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) } ) )
3 neleq1 
 |-  ( x = X -> ( x e/ Prime <-> X e/ Prime ) )
4 oveq1 
 |-  ( x = X -> ( x - 1 ) = ( X - 1 ) )
5 4 oveq2d 
 |-  ( x = X -> ( N ^ ( x - 1 ) ) = ( N ^ ( X - 1 ) ) )
6 id 
 |-  ( x = X -> x = X )
7 5 6 oveq12d 
 |-  ( x = X -> ( ( N ^ ( x - 1 ) ) mod x ) = ( ( N ^ ( X - 1 ) ) mod X ) )
8 7 eqeq1d 
 |-  ( x = X -> ( ( ( N ^ ( x - 1 ) ) mod x ) = 1 <-> ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) )
9 3 8 anbi12d 
 |-  ( x = X -> ( ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) <-> ( X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
10 9 elrab 
 |-  ( X e. { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ ( ( N ^ ( x - 1 ) ) mod x ) = 1 ) } <-> ( X e. ( ZZ>= ` 4 ) /\ ( X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
11 2 10 bitrdi 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ ( X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) ) )
12 3anass 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) <-> ( X e. ( ZZ>= ` 4 ) /\ ( X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
13 11 12 bitr4di 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )