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 FPPr 2 X 2 X Odd X 2 X mod X = 2

Proof

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