Metamath Proof Explorer

Theorem 341fppr2

Description: 341 is the (smallest)Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023)

Ref Expression
Assertion 341fppr2 
|- ; ; 3 4 1 e. ( FPPr ` 2 )

Proof

Step Hyp Ref Expression
1 4z 
 |-  4 e. ZZ
2 3nn0 
 |-  3 e. NN0
3 4nn0 
 |-  4 e. NN0
4 2 3 deccl 
 |-  ; 3 4 e. NN0
5 1nn 
 |-  1 e. NN
6 4 5 decnncl 
 |-  ; ; 3 4 1 e. NN
7 6 nnzi 
 |-  ; ; 3 4 1 e. ZZ
8 4nn 
 |-  4 e. NN
9 2 8 decnncl 
 |-  ; 3 4 e. NN
10 1nn0 
 |-  1 e. NN0
11 4re 
 |-  4 e. RR
12 9re 
 |-  9 e. RR
13 4lt9 
 |-  4 < 9
14 11 12 13 ltleii 
 |-  4 <_ 9
15 9 10 3 14 declei 
 |-  4 <_ ; ; 3 4 1
16 eluz2 
 |-  ( ; ; 3 4 1 e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ ; ; 3 4 1 e. ZZ /\ 4 <_ ; ; 3 4 1 ) )
17 1 7 15 16 mpbir3an 
 |-  ; ; 3 4 1 e. ( ZZ>= ` 4 )
18 2z 
 |-  2 e. ZZ
19 10 5 decnncl 
 |-  ; 1 1 e. NN
20 19 nnzi 
 |-  ; 1 1 e. ZZ
21 2nn0 
 |-  2 e. NN0
22 2re 
 |-  2 e. RR
23 2lt9 
 |-  2 < 9
24 22 12 23 ltleii 
 |-  2 <_ 9
25 5 10 21 24 declei 
 |-  2 <_ ; 1 1
26 eluz2 
 |-  ( ; 1 1 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ; 1 1 e. ZZ /\ 2 <_ ; 1 1 ) )
27 18 20 25 26 mpbir3an 
 |-  ; 1 1 e. ( ZZ>= ` 2 )
28 2 5 decnncl 
 |-  ; 3 1 e. NN
29 28 nnzi 
 |-  ; 3 1 e. ZZ
30 3nn 
 |-  3 e. NN
31 30 10 21 24 declei 
 |-  2 <_ ; 3 1
32 eluz2 
 |-  ( ; 3 1 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ; 3 1 e. ZZ /\ 2 <_ ; 3 1 ) )
33 18 29 31 32 mpbir3an 
 |-  ; 3 1 e. ( ZZ>= ` 2 )
34 nprm 
 |-  ( ( ; 1 1 e. ( ZZ>= ` 2 ) /\ ; 3 1 e. ( ZZ>= ` 2 ) ) -> -. ( ; 1 1 x. ; 3 1 ) e. Prime )
35 27 33 34 mp2an 
 |-  -. ( ; 1 1 x. ; 3 1 ) e. Prime
36 df-nel 
 |-  ( ; ; 3 4 1 e/ Prime <-> -. ; ; 3 4 1 e. Prime )
37 11t31e341 
 |-  ( ; 1 1 x. ; 3 1 ) = ; ; 3 4 1
38 37 eqcomi 
 |-  ; ; 3 4 1 = ( ; 1 1 x. ; 3 1 )
39 38 eleq1i 
 |-  ( ; ; 3 4 1 e. Prime <-> ( ; 1 1 x. ; 3 1 ) e. Prime )
40 36 39 xchbinx 
 |-  ( ; ; 3 4 1 e/ Prime <-> -. ( ; 1 1 x. ; 3 1 ) e. Prime )
41 35 40 mpbir 
 |-  ; ; 3 4 1 e/ Prime
42 eqid 
 |-  ; ; 3 4 1 = ; ; 3 4 1
43 eqid 
 |-  ( ; 3 4 + 1 ) = ( ; 3 4 + 1 )
44 1m1e0 
 |-  ( 1 - 1 ) = 0
45 4 10 10 42 43 44 decsubi 
 |-  ( ; ; 3 4 1 - 1 ) = ; ; 3 4 0
46 45 oveq2i 
 |-  ( 2 ^ ( ; ; 3 4 1 - 1 ) ) = ( 2 ^ ; ; 3 4 0 )
47 46 oveq1i 
 |-  ( ( 2 ^ ( ; ; 3 4 1 - 1 ) ) mod ; ; 3 4 1 ) = ( ( 2 ^ ; ; 3 4 0 ) mod ; ; 3 4 1 )
48 2exp340mod341 
 |-  ( ( 2 ^ ; ; 3 4 0 ) mod ; ; 3 4 1 ) = 1
49 47 48 eqtri 
 |-  ( ( 2 ^ ( ; ; 3 4 1 - 1 ) ) mod ; ; 3 4 1 ) = 1
50 2nn 
 |-  2 e. NN
51 fpprel 
 |-  ( 2 e. NN -> ( ; ; 3 4 1 e. ( FPPr ` 2 ) <-> ( ; ; 3 4 1 e. ( ZZ>= ` 4 ) /\ ; ; 3 4 1 e/ Prime /\ ( ( 2 ^ ( ; ; 3 4 1 - 1 ) ) mod ; ; 3 4 1 ) = 1 ) ) )
52 50 51 ax-mp 
 |-  ( ; ; 3 4 1 e. ( FPPr ` 2 ) <-> ( ; ; 3 4 1 e. ( ZZ>= ` 4 ) /\ ; ; 3 4 1 e/ Prime /\ ( ( 2 ^ ( ; ; 3 4 1 - 1 ) ) mod ; ; 3 4 1 ) = 1 ) )
53 17 41 49 52 mpbir3an 
 |-  ; ; 3 4 1 e. ( FPPr ` 2 )