Metamath Proof Explorer


Theorem fpprwpprb

Description: An integer X which is coprime with an integer N is a Fermat pseudoprime to the base N iff it is a weak pseudoprime to the base N . (Contributed by AV, 2-Jun-2023)

Ref Expression
Assertion fpprwpprb XgcdN=1XFPPrNX4XNNXmodX=NmodX

Proof

Step Hyp Ref Expression
1 fpprbasnn XFPPrNN
2 fpprel NXFPPrNX4XNX1modX=1
3 3simpa X4XNX1modX=1X4X
4 3 a1i NX4XNX1modX=1X4X
5 2 4 sylbid NXFPPrNX4X
6 1 5 mpcom XFPPrNX4X
7 fpprwppr XFPPrNNXmodX=NmodX
8 1 7 jca XFPPrNNNXmodX=NmodX
9 6 8 jca XFPPrNX4XNNXmodX=NmodX
10 simprll XgcdN=1X4XNNXmodX=NmodXX4
11 simprlr XgcdN=1X4XNNXmodX=NmodXX
12 eluz4nn X4X
13 12 adantr X4NX
14 nnz NN
15 12 nnnn0d X4X0
16 zexpcl NX0NX
17 14 15 16 syl2anr X4NNX
18 14 adantl X4NN
19 moddvds XNXNNXmodX=NmodXXNXN
20 13 17 18 19 syl3anc X4NNXmodX=NmodXXNXN
21 nncn NN
22 expm1t NXNX=NX1 N
23 21 12 22 syl2anr X4NNX=NX1 N
24 23 oveq1d X4NNXN=NX1 NN
25 nnm1nn0 XX10
26 12 25 syl X4X10
27 zexpcl NX10NX1
28 14 26 27 syl2anr X4NNX1
29 28 zcnd X4NNX1
30 21 adantl X4NN
31 29 30 mulsubfacd X4NNX1 NN=NX11 N
32 24 31 eqtrd X4NNXN=NX11 N
33 32 breq2d X4NXNXNXNX11 N
34 1zzd X4N1
35 28 34 zsubcld X4NNX11
36 dvdsmulgcd NX11NXNX11 NXNX11NgcdX
37 35 18 36 syl2anc X4NXNX11 NXNX11NgcdX
38 eluzelz X4X
39 gcdcom XNXgcdN=NgcdX
40 38 14 39 syl2an X4NXgcdN=NgcdX
41 40 eqeq1d X4NXgcdN=1NgcdX=1
42 41 biimpd X4NXgcdN=1NgcdX=1
43 42 imp X4NXgcdN=1NgcdX=1
44 43 oveq2d X4NXgcdN=1NX11NgcdX=NX111
45 35 zcnd X4NNX11
46 45 mulid1d X4NNX111=NX11
47 46 adantr X4NXgcdN=1NX111=NX11
48 44 47 eqtrd X4NXgcdN=1NX11NgcdX=NX11
49 48 breq2d X4NXgcdN=1XNX11NgcdXXNX11
50 49 biimpd X4NXgcdN=1XNX11NgcdXXNX11
51 50 ex X4NXgcdN=1XNX11NgcdXXNX11
52 51 com23 X4NXNX11NgcdXXgcdN=1XNX11
53 37 52 sylbid X4NXNX11 NXgcdN=1XNX11
54 33 53 sylbid X4NXNXNXgcdN=1XNX11
55 20 54 sylbid X4NNXmodX=NmodXXgcdN=1XNX11
56 55 expimpd X4NNXmodX=NmodXXgcdN=1XNX11
57 56 adantr X4XNNXmodX=NmodXXgcdN=1XNX11
58 57 imp X4XNNXmodX=NmodXXgcdN=1XNX11
59 58 impcom XgcdN=1X4XNNXmodX=NmodXXNX11
60 eluz4eluz2 X4X2
61 60 adantr X4XX2
62 61 adantr X4XNNXmodX=NmodXX2
63 14 adantr NNXmodX=NmodXN
64 26 adantr X4XX10
65 63 64 27 syl2anr X4XNNXmodX=NmodXNX1
66 62 65 jca X4XNNXmodX=NmodXX2NX1
67 66 adantl XgcdN=1X4XNNXmodX=NmodXX2NX1
68 modm1div X2NX1NX1modX=1XNX11
69 67 68 syl XgcdN=1X4XNNXmodX=NmodXNX1modX=1XNX11
70 59 69 mpbird XgcdN=1X4XNNXmodX=NmodXNX1modX=1
71 2 adantr NNXmodX=NmodXXFPPrNX4XNX1modX=1
72 71 adantl X4XNNXmodX=NmodXXFPPrNX4XNX1modX=1
73 72 adantl XgcdN=1X4XNNXmodX=NmodXXFPPrNX4XNX1modX=1
74 10 11 70 73 mpbir3and XgcdN=1X4XNNXmodX=NmodXXFPPrN
75 74 ex XgcdN=1X4XNNXmodX=NmodXXFPPrN
76 9 75 impbid2 XgcdN=1XFPPrNX4XNNXmodX=NmodX