Metamath Proof Explorer


Theorem fpprwppr

Description: A Fermat pseudoprime to the base N is aweak pseudoprime (see Wikipedia "Fermat pseudoprime", 29-May-2023, https://en.wikipedia.org/wiki/Fermat_pseudoprime . (Contributed by AV, 31-May-2023)

Ref Expression
Assertion fpprwppr X FPPr N N X mod X = N mod X

Proof

Step Hyp Ref Expression
1 fpprbasnn X FPPr N N
2 fpprel N X FPPr N X 4 X N X 1 mod X = 1
3 nnz N N
4 eluz4nn X 4 X
5 nnm1nn0 X X 1 0
6 4 5 syl X 4 X 1 0
7 zexpcl N X 1 0 N X 1
8 3 6 7 syl2an N X 4 N X 1
9 8 zred N X 4 N X 1
10 4 nnrpd X 4 X +
11 10 adantl N X 4 X +
12 9 11 modcld N X 4 N X 1 mod X
13 12 recnd N X 4 N X 1 mod X
14 1cnd N X 4 1
15 nncn N N
16 15 adantr N X 4 N
17 nnne0 N N 0
18 17 adantr N X 4 N 0
19 13 14 16 18 mulcand N X 4 N N X 1 mod X = N 1 N X 1 mod X = 1
20 oveq1 N N X 1 mod X = N 1 N N X 1 mod X mod X = N 1 mod X
21 3 adantr N X 4 N
22 modmulmodr N N X 1 X + N N X 1 mod X mod X = N N X 1 mod X
23 21 9 11 22 syl3anc N X 4 N N X 1 mod X mod X = N N X 1 mod X
24 23 eqeq1d N X 4 N N X 1 mod X mod X = N 1 mod X N N X 1 mod X = N 1 mod X
25 8 zcnd N X 4 N X 1
26 16 25 mulcomd N X 4 N N X 1 = N X 1 N
27 expm1t N X N X = N X 1 N
28 27 eqcomd N X N X 1 N = N X
29 15 4 28 syl2an N X 4 N X 1 N = N X
30 26 29 eqtrd N X 4 N N X 1 = N X
31 30 oveq1d N X 4 N N X 1 mod X = N X mod X
32 15 mulid1d N N 1 = N
33 32 adantr N X 4 N 1 = N
34 33 oveq1d N X 4 N 1 mod X = N mod X
35 31 34 eqeq12d N X 4 N N X 1 mod X = N 1 mod X N X mod X = N mod X
36 35 biimpd N X 4 N N X 1 mod X = N 1 mod X N X mod X = N mod X
37 24 36 sylbid N X 4 N N X 1 mod X mod X = N 1 mod X N X mod X = N mod X
38 20 37 syl5 N X 4 N N X 1 mod X = N 1 N X mod X = N mod X
39 19 38 sylbird N X 4 N X 1 mod X = 1 N X mod X = N mod X
40 39 a1d N X 4 X N X 1 mod X = 1 N X mod X = N mod X
41 40 ex N X 4 X N X 1 mod X = 1 N X mod X = N mod X
42 41 3impd N X 4 X N X 1 mod X = 1 N X mod X = N mod X
43 2 42 sylbid N X FPPr N N X mod X = N mod X
44 1 43 mpcom X FPPr N N X mod X = N mod X