Metamath Proof Explorer


Theorem fppr

Description: The set of Fermat pseudoprimes to the base N . (Contributed by AV, 29-May-2023)

Ref Expression
Assertion fppr N FPPr N = x 4 | x x N x 1 1

Proof

Step Hyp Ref Expression
1 oveq1 n = N n x 1 = N x 1
2 1 oveq1d n = N n x 1 1 = N x 1 1
3 2 breq2d n = N x n x 1 1 x N x 1 1
4 3 anbi2d n = N x x n x 1 1 x x N x 1 1
5 4 rabbidv n = N x 4 | x x n x 1 1 = x 4 | x x N x 1 1
6 df-fppr FPPr = n x 4 | x x n x 1 1
7 fvex 4 V
8 7 rabex x 4 | x x N x 1 1 V
9 5 6 8 fvmpt N FPPr N = x 4 | x x N x 1 1