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 syl5bi ( 𝑋 ∈ ℤ → ( ( 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 ) )