Metamath Proof Explorer


Theorem fpprel

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

Ref Expression
Assertion fpprel N X FPPr N X 4 X N X 1 mod X = 1

Proof

Step Hyp Ref Expression
1 fpprmod N FPPr N = x 4 | x N x 1 mod x = 1
2 1 eleq2d N X FPPr N X x 4 | x N x 1 mod x = 1
3 neleq1 x = X x X
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 N x 1 mod x = 1 X N X 1 mod X = 1
10 9 elrab X x 4 | x N x 1 mod x = 1 X 4 X N X 1 mod X = 1
11 2 10 bitrdi N X FPPr N X 4 X N X 1 mod X = 1
12 3anass X 4 X N X 1 mod X = 1 X 4 X N X 1 mod X = 1
13 11 12 bitr4di N X FPPr N X 4 X N X 1 mod X = 1