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 syl5bi
 |-  ( 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 ) )