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 
|- ( ( X gcd N ) = 1 -> ( X e. ( FPPr ` N ) <-> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fpprbasnn 
 |-  ( X e. ( FPPr ` N ) -> N e. NN )
2 fpprel 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
3 3simpa 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) -> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) )
4 3 a1i 
 |-  ( N e. NN -> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) -> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) ) )
5 2 4 sylbid 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) -> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) ) )
6 1 5 mpcom 
 |-  ( X e. ( FPPr ` N ) -> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) )
7 fpprwppr 
 |-  ( X e. ( FPPr ` N ) -> ( ( N ^ X ) mod X ) = ( N mod X ) )
8 1 7 jca 
 |-  ( X e. ( FPPr ` N ) -> ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) )
9 6 8 jca 
 |-  ( X e. ( FPPr ` N ) -> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) )
10 simprll 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> X e. ( ZZ>= ` 4 ) )
11 simprlr 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> X e/ Prime )
12 eluz4nn 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. NN )
13 12 adantr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> X e. NN )
14 nnz 
 |-  ( N e. NN -> N e. ZZ )
15 12 nnnn0d 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. NN0 )
16 zexpcl 
 |-  ( ( N e. ZZ /\ X e. NN0 ) -> ( N ^ X ) e. ZZ )
17 14 15 16 syl2anr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( N ^ X ) e. ZZ )
18 14 adantl 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> N e. ZZ )
19 moddvds 
 |-  ( ( X e. NN /\ ( N ^ X ) e. ZZ /\ N e. ZZ ) -> ( ( ( N ^ X ) mod X ) = ( N mod X ) <-> X || ( ( N ^ X ) - N ) ) )
20 13 17 18 19 syl3anc 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( ( N ^ X ) mod X ) = ( N mod X ) <-> X || ( ( N ^ X ) - N ) ) )
21 nncn 
 |-  ( N e. NN -> N e. CC )
22 expm1t 
 |-  ( ( N e. CC /\ X e. NN ) -> ( N ^ X ) = ( ( N ^ ( X - 1 ) ) x. N ) )
23 21 12 22 syl2anr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( N ^ X ) = ( ( N ^ ( X - 1 ) ) x. N ) )
24 23 oveq1d 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( N ^ X ) - N ) = ( ( ( N ^ ( X - 1 ) ) x. N ) - N ) )
25 nnm1nn0 
 |-  ( X e. NN -> ( X - 1 ) e. NN0 )
26 12 25 syl 
 |-  ( X e. ( ZZ>= ` 4 ) -> ( X - 1 ) e. NN0 )
27 zexpcl 
 |-  ( ( N e. ZZ /\ ( X - 1 ) e. NN0 ) -> ( N ^ ( X - 1 ) ) e. ZZ )
28 14 26 27 syl2anr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( N ^ ( X - 1 ) ) e. ZZ )
29 28 zcnd 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( N ^ ( X - 1 ) ) e. CC )
30 21 adantl 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> N e. CC )
31 29 30 mulsubfacd 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( ( N ^ ( X - 1 ) ) x. N ) - N ) = ( ( ( N ^ ( X - 1 ) ) - 1 ) x. N ) )
32 24 31 eqtrd 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( N ^ X ) - N ) = ( ( ( N ^ ( X - 1 ) ) - 1 ) x. N ) )
33 32 breq2d 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( X || ( ( N ^ X ) - N ) <-> X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. N ) ) )
34 1zzd 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> 1 e. ZZ )
35 28 34 zsubcld 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( N ^ ( X - 1 ) ) - 1 ) e. ZZ )
36 dvdsmulgcd 
 |-  ( ( ( ( N ^ ( X - 1 ) ) - 1 ) e. ZZ /\ N e. ZZ ) -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. N ) <-> X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) ) )
37 35 18 36 syl2anc 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. N ) <-> X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) ) )
38 eluzelz 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. ZZ )
39 gcdcom 
 |-  ( ( X e. ZZ /\ N e. ZZ ) -> ( X gcd N ) = ( N gcd X ) )
40 38 14 39 syl2an 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( X gcd N ) = ( N gcd X ) )
41 40 eqeq1d 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( X gcd N ) = 1 <-> ( N gcd X ) = 1 ) )
42 41 biimpd 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( X gcd N ) = 1 -> ( N gcd X ) = 1 ) )
43 42 imp 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) /\ ( X gcd N ) = 1 ) -> ( N gcd X ) = 1 )
44 43 oveq2d 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) /\ ( X gcd N ) = 1 ) -> ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) = ( ( ( N ^ ( X - 1 ) ) - 1 ) x. 1 ) )
45 35 zcnd 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( N ^ ( X - 1 ) ) - 1 ) e. CC )
46 45 mulid1d 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( ( N ^ ( X - 1 ) ) - 1 ) x. 1 ) = ( ( N ^ ( X - 1 ) ) - 1 ) )
47 46 adantr 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) /\ ( X gcd N ) = 1 ) -> ( ( ( N ^ ( X - 1 ) ) - 1 ) x. 1 ) = ( ( N ^ ( X - 1 ) ) - 1 ) )
48 44 47 eqtrd 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) /\ ( X gcd N ) = 1 ) -> ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) = ( ( N ^ ( X - 1 ) ) - 1 ) )
49 48 breq2d 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) /\ ( X gcd N ) = 1 ) -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) <-> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) )
50 49 biimpd 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) /\ ( X gcd N ) = 1 ) -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) )
51 50 ex 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( X gcd N ) = 1 -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
52 51 com23 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. ( N gcd X ) ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
53 37 52 sylbid 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( X || ( ( ( N ^ ( X - 1 ) ) - 1 ) x. N ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
54 33 53 sylbid 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( X || ( ( N ^ X ) - N ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
55 20 54 sylbid 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ N e. NN ) -> ( ( ( N ^ X ) mod X ) = ( N mod X ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
56 55 expimpd 
 |-  ( X e. ( ZZ>= ` 4 ) -> ( ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
57 56 adantr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) -> ( ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) ) )
58 57 imp 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) -> ( ( X gcd N ) = 1 -> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) )
59 58 impcom 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> X || ( ( N ^ ( X - 1 ) ) - 1 ) )
60 eluz4eluz2 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )
61 60 adantr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) -> X e. ( ZZ>= ` 2 ) )
62 61 adantr 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) -> X e. ( ZZ>= ` 2 ) )
63 14 adantr 
 |-  ( ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) -> N e. ZZ )
64 26 adantr 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) -> ( X - 1 ) e. NN0 )
65 63 64 27 syl2anr 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) -> ( N ^ ( X - 1 ) ) e. ZZ )
66 62 65 jca 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) -> ( X e. ( ZZ>= ` 2 ) /\ ( N ^ ( X - 1 ) ) e. ZZ ) )
67 66 adantl 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> ( X e. ( ZZ>= ` 2 ) /\ ( N ^ ( X - 1 ) ) e. ZZ ) )
68 modm1div 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ ( N ^ ( X - 1 ) ) e. ZZ ) -> ( ( ( N ^ ( X - 1 ) ) mod X ) = 1 <-> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) )
69 67 68 syl 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> ( ( ( N ^ ( X - 1 ) ) mod X ) = 1 <-> X || ( ( N ^ ( X - 1 ) ) - 1 ) ) )
70 59 69 mpbird 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> ( ( N ^ ( X - 1 ) ) mod X ) = 1 )
71 2 adantr 
 |-  ( ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
72 71 adantl 
 |-  ( ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
73 72 adantl 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
74 10 11 70 73 mpbir3and 
 |-  ( ( ( X gcd N ) = 1 /\ ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) -> X e. ( FPPr ` N ) )
75 74 ex 
 |-  ( ( X gcd N ) = 1 -> ( ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) -> X e. ( FPPr ` N ) ) )
76 9 75 impbid2 
 |-  ( ( X gcd N ) = 1 -> ( X e. ( FPPr ` N ) <-> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( N e. NN /\ ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) )