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 ( 𝑋 ∈ ( FPPr ‘ 2 ) ↔ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ Odd ∧ 𝑋 ∉ ℙ ) ∧ ( ( 2 ↑ 𝑋 ) mod 𝑋 ) = 2 ) )

Proof

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