Metamath Proof Explorer

Theorem fpprel2

Description: An alternate definition for a Fermat pseudoprime to the base 2. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion fpprel2 
|- ( X e. ( FPPr ` 2 ) <-> ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 fpprel 
 |-  ( 2 e. NN -> ( X e. ( FPPr ` 2 ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) )
3 1 2 mp1i 
 |-  ( X e. ( FPPr ` 2 ) -> ( X e. ( FPPr ` 2 ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) )
4 eluz4eluz2 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )
5 4 3ad2ant1 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) -> X e. ( ZZ>= ` 2 ) )
6 5 adantl 
 |-  ( ( X e. ( FPPr ` 2 ) /\ ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) -> X e. ( ZZ>= ` 2 ) )
7 fppr2odd 
 |-  ( X e. ( FPPr ` 2 ) -> X e. Odd )
8 7 adantr 
 |-  ( ( X e. ( FPPr ` 2 ) /\ ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) -> X e. Odd )
9 simpr2 
 |-  ( ( X e. ( FPPr ` 2 ) /\ ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) -> X e/ Prime )
10 6 8 9 3jca 
 |-  ( ( X e. ( FPPr ` 2 ) /\ ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) -> ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) )
11 fpprwppr 
 |-  ( X e. ( FPPr ` 2 ) -> ( ( 2 ^ X ) mod X ) = ( 2 mod X ) )
12 2re 
 |-  2 e. RR
13 12 a1i 
 |-  ( X e. ( ZZ>= ` 4 ) -> 2 e. RR )
14 eluz4nn 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. NN )
15 14 nnrpd 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. RR+ )
16 0le2 
 |-  0 <_ 2
17 16 a1i 
 |-  ( X e. ( ZZ>= ` 4 ) -> 0 <_ 2 )
18 eluz2 
 |-  ( X e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ X e. ZZ /\ 4 <_ X ) )
19 4z 
 |-  4 e. ZZ
20 zlem1lt 
 |-  ( ( 4 e. ZZ /\ X e. ZZ ) -> ( 4 <_ X <-> ( 4 - 1 ) < X ) )
21 19 20 mpan 
 |-  ( X e. ZZ -> ( 4 <_ X <-> ( 4 - 1 ) < X ) )
22 4m1e3 
 |-  ( 4 - 1 ) = 3
23 22 breq1i 
 |-  ( ( 4 - 1 ) < X <-> 3 < X )
24 12 a1i 
 |-  ( ( X e. ZZ /\ 3 < X ) -> 2 e. RR )
25 3re 
 |-  3 e. RR
26 25 a1i 
 |-  ( ( X e. ZZ /\ 3 < X ) -> 3 e. RR )
27 zre 
 |-  ( X e. ZZ -> X e. RR )
28 27 adantr 
 |-  ( ( X e. ZZ /\ 3 < X ) -> X e. RR )
29 2lt3 
 |-  2 < 3
30 29 a1i 
 |-  ( ( X e. ZZ /\ 3 < X ) -> 2 < 3 )
31 simpr 
 |-  ( ( X e. ZZ /\ 3 < X ) -> 3 < X )
32 24 26 28 30 31 lttrd 
 |-  ( ( X e. ZZ /\ 3 < X ) -> 2 < X )
33 32 ex 
 |-  ( X e. ZZ -> ( 3 < X -> 2 < X ) )
34 23 33 biimtrid 
 |-  ( X e. ZZ -> ( ( 4 - 1 ) < X -> 2 < X ) )
35 21 34 sylbid 
 |-  ( X e. ZZ -> ( 4 <_ X -> 2 < X ) )
36 35 a1i 
 |-  ( 4 e. ZZ -> ( X e. ZZ -> ( 4 <_ X -> 2 < X ) ) )
37 36 3imp 
 |-  ( ( 4 e. ZZ /\ X e. ZZ /\ 4 <_ X ) -> 2 < X )
38 18 37 sylbi 
 |-  ( X e. ( ZZ>= ` 4 ) -> 2 < X )
39 modid 
 |-  ( ( ( 2 e. RR /\ X e. RR+ ) /\ ( 0 <_ 2 /\ 2 < X ) ) -> ( 2 mod X ) = 2 )
40 13 15 17 38 39 syl22anc 
 |-  ( X e. ( ZZ>= ` 4 ) -> ( 2 mod X ) = 2 )
41 40 3ad2ant1 
 |-  ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) -> ( 2 mod X ) = 2 )
42 11 41 sylan9eq 
 |-  ( ( X e. ( FPPr ` 2 ) /\ ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) -> ( ( 2 ^ X ) mod X ) = 2 )
43 10 42 jca 
 |-  ( ( X e. ( FPPr ` 2 ) /\ ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) ) -> ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) )
44 43 ex 
 |-  ( X e. ( FPPr ` 2 ) -> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( 2 ^ ( X - 1 ) ) mod X ) = 1 ) -> ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) ) )
45 3 44 sylbid 
 |-  ( X e. ( FPPr ` 2 ) -> ( X e. ( FPPr ` 2 ) -> ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) ) )
46 45 pm2.43i 
 |-  ( X e. ( FPPr ` 2 ) -> ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) )
47 ge2nprmge4 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e/ Prime ) -> X e. ( ZZ>= ` 4 ) )
48 47 3adant2 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> X e. ( ZZ>= ` 4 ) )
49 simp3 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> X e/ Prime )
50 48 49 jca 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) )
51 50 adantr 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) )
52 1 a1i 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> 2 e. NN )
53 12 a1i 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> 2 e. RR )
54 eluz2nn 
 |-  ( X e. ( ZZ>= ` 2 ) -> X e. NN )
55 54 nnrpd 
 |-  ( X e. ( ZZ>= ` 2 ) -> X e. RR+ )
56 55 3ad2ant1 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> X e. RR+ )
57 16 a1i 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> 0 <_ 2 )
58 48 38 syl 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> 2 < X )
59 53 56 57 58 39 syl22anc 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> ( 2 mod X ) = 2 )
60 59 eqcomd 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> 2 = ( 2 mod X ) )
61 60 eqeq2d 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> ( ( ( 2 ^ X ) mod X ) = 2 <-> ( ( 2 ^ X ) mod X ) = ( 2 mod X ) ) )
62 61 biimpa 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> ( ( 2 ^ X ) mod X ) = ( 2 mod X ) )
63 52 62 jca 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> ( 2 e. NN /\ ( ( 2 ^ X ) mod X ) = ( 2 mod X ) ) )
64 gcd2odd1 
 |-  ( X e. Odd -> ( X gcd 2 ) = 1 )
65 64 3ad2ant2 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) -> ( X gcd 2 ) = 1 )
66 65 adantr 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> ( X gcd 2 ) = 1 )
67 fpprwpprb 
 |-  ( ( X gcd 2 ) = 1 -> ( X e. ( FPPr ` 2 ) <-> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( 2 e. NN /\ ( ( 2 ^ X ) mod X ) = ( 2 mod X ) ) ) ) )
68 66 67 syl 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> ( X e. ( FPPr ` 2 ) <-> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime ) /\ ( 2 e. NN /\ ( ( 2 ^ X ) mod X ) = ( 2 mod X ) ) ) ) )
69 51 63 68 mpbir2and 
 |-  ( ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) -> X e. ( FPPr ` 2 ) )
70 46 69 impbii 
 |-  ( X e. ( FPPr ` 2 ) <-> ( ( X e. ( ZZ>= ` 2 ) /\ X e. Odd /\ X e/ Prime ) /\ ( ( 2 ^ X ) mod X ) = 2 ) )