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 ∈ ( FPPr ‘ 2 )

Proof

Step Hyp Ref Expression
1 4z ⊢ 4 ∈ ℤ
2 3nn0 ⊢ 3 ∈ ℕ0
3 4nn0 ⊢ 4 ∈ ℕ0
4 2 3 deccl ⊢ 3 4 ∈ ℕ0
5 1nn ⊢ 1 ∈ ℕ
6 4 5 decnncl ⊢ 3 4 1 ∈ ℕ
7 6 nnzi ⊢ 3 4 1 ∈ ℤ
8 4nn ⊢ 4 ∈ ℕ
9 2 8 decnncl ⊢ 3 4 ∈ ℕ
10 1nn0 ⊢ 1 ∈ ℕ0
11 4re ⊢ 4 ∈ ℝ
12 9re ⊢ 9 ∈ ℝ
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 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 3 4 1 ∈ ℤ ∧ 4 ≤ 3 4 1 ) )
17 1 7 15 16 mpbir3an ⊢ 3 4 1 ∈ ( ℤ≥ ‘ 4 )
18 2z ⊢ 2 ∈ ℤ
19 10 5 decnncl ⊢ 1 1 ∈ ℕ
20 19 nnzi ⊢ 1 1 ∈ ℤ
21 2nn0 ⊢ 2 ∈ ℕ0
22 2re ⊢ 2 ∈ ℝ
23 2lt9 ⊢ 2 < 9
24 22 12 23 ltleii ⊢ 2 ≤ 9
25 5 10 21 24 declei ⊢ 2 ≤ 1 1
26 eluz2 ⊢ ( 1 1 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 1 1 ∈ ℤ ∧ 2 ≤ 1 1 ) )
27 18 20 25 26 mpbir3an ⊢ 1 1 ∈ ( ℤ≥ ‘ 2 )
28 2 5 decnncl ⊢ 3 1 ∈ ℕ
29 28 nnzi ⊢ 3 1 ∈ ℤ
30 3nn ⊢ 3 ∈ ℕ
31 30 10 21 24 declei ⊢ 2 ≤ 3 1
32 eluz2 ⊢ ( 3 1 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 3 1 ∈ ℤ ∧ 2 ≤ 3 1 ) )
33 18 29 31 32 mpbir3an ⊢ 3 1 ∈ ( ℤ≥ ‘ 2 )
34 nprm ⊢ ( ( 1 1 ∈ ( ℤ≥ ‘ 2 ) ∧ 3 1 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 1 1 · 3 1 ) ∈ ℙ )
35 27 33 34 mp2an ⊢ ¬ ( 1 1 · 3 1 ) ∈ ℙ
36 df-nel ⊢ ( 3 4 1 ∉ ℙ ↔ ¬ 3 4 1 ∈ ℙ )
37 11t31e341 ⊢ ( 1 1 · 3 1 ) = 3 4 1
38 37 eqcomi ⊢ 3 4 1 = ( 1 1 · 3 1 )
39 38 eleq1i ⊢ ( 3 4 1 ∈ ℙ ↔ ( 1 1 · 3 1 ) ∈ ℙ )
40 36 39 xchbinx ⊢ ( 3 4 1 ∉ ℙ ↔ ¬ ( 1 1 · 3 1 ) ∈ ℙ )
41 35 40 mpbir ⊢ 3 4 1 ∉ ℙ
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 ∈ ℕ
51 fpprel ⊢ ( 2 ∈ ℕ → ( 3 4 1 ∈ ( FPPr ‘ 2 ) ↔ ( 3 4 1 ∈ ( ℤ≥ ‘ 4 ) ∧ 3 4 1 ∉ ℙ ∧ ( ( 2 ↑ ( 3 4 1 − 1 ) ) mod 3 4 1 ) = 1 ) ) )
52 50 51 ax-mp ⊢ ( 3 4 1 ∈ ( FPPr ‘ 2 ) ↔ ( 3 4 1 ∈ ( ℤ≥ ‘ 4 ) ∧ 3 4 1 ∉ ℙ ∧ ( ( 2 ↑ ( 3 4 1 − 1 ) ) mod 3 4 1 ) = 1 ) )
53 17 41 49 52 mpbir3an ⊢ 3 4 1 ∈ ( FPPr ‘ 2 )