Metamath Proof Explorer


Theorem fppr2odd

Description: A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion fppr2odd X FPPr 2 X Odd

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 ax-mp X FPPr 2 X 4 X 2 X 1 mod X = 1
4 eluz4nn X 4 X
5 4 adantr X 4 2 X 1 mod X = 1 X
6 eluzelz X 4 X
7 zeo2ALTV X X Even ¬ X Odd
8 6 7 syl X 4 X Even ¬ X Odd
9 8 adantr X 4 2 X 1 mod X = 1 X Even ¬ X Odd
10 9 biimprd X 4 2 X 1 mod X = 1 ¬ X Odd X Even
11 nnennexALTV X X Even y X = 2 y
12 5 10 11 syl6an X 4 2 X 1 mod X = 1 ¬ X Odd y X = 2 y
13 oveq1 X = 2 y X 1 = 2 y 1
14 13 oveq2d X = 2 y 2 X 1 = 2 2 y 1
15 id X = 2 y X = 2 y
16 14 15 oveq12d X = 2 y 2 X 1 mod X = 2 2 y 1 mod 2 y
17 16 eqeq1d X = 2 y 2 X 1 mod X = 1 2 2 y 1 mod 2 y = 1
18 17 adantl X 4 y X = 2 y 2 X 1 mod X = 1 2 2 y 1 mod 2 y = 1
19 2z 2
20 1 a1i y 2
21 id y y
22 20 21 nnmulcld y 2 y
23 nnm1nn0 2 y 2 y 1 0
24 22 23 syl y 2 y 1 0
25 zexpcl 2 2 y 1 0 2 2 y 1
26 19 24 25 sylancr y 2 2 y 1
27 22 nnrpd y 2 y +
28 modmuladdim 2 2 y 1 2 y + 2 2 y 1 mod 2 y = 1 m 2 2 y 1 = m 2 y + 1
29 26 27 28 syl2anc y 2 2 y 1 mod 2 y = 1 m 2 2 y 1 = m 2 y + 1
30 24 adantr y m 2 y 1 0
31 19 30 25 sylancr y m 2 2 y 1
32 31 zcnd y m 2 2 y 1
33 zcn m m
34 33 adantl y m m
35 2cnd y m 2
36 nncn y y
37 36 adantr y m y
38 35 37 mulcld y m 2 y
39 34 38 mulcld y m m 2 y
40 1cnd y m 1
41 subadd 2 2 y 1 m 2 y 1 2 2 y 1 m 2 y = 1 m 2 y + 1 = 2 2 y 1
42 eqcom m 2 y + 1 = 2 2 y 1 2 2 y 1 = m 2 y + 1
43 41 42 bitrdi 2 2 y 1 m 2 y 1 2 2 y 1 m 2 y = 1 2 2 y 1 = m 2 y + 1
44 32 39 40 43 syl3anc y m 2 2 y 1 m 2 y = 1 2 2 y 1 = m 2 y + 1
45 2cnd y 2
46 45 36 mulcld y 2 y
47 1cnd y 1
48 46 47 subcld y 2 y 1
49 48 adantr y m 2 y 1
50 npcan1 2 y 1 2 y 1 - 1 + 1 = 2 y 1
51 49 50 syl y m 2 y 1 - 1 + 1 = 2 y 1
52 51 eqcomd y m 2 y 1 = 2 y 1 - 1 + 1
53 52 oveq2d y m 2 2 y 1 = 2 2 y 1 - 1 + 1
54 2t1e2 2 1 = 2
55 54 eqcomi 2 = 2 1
56 55 oveq2i 2 y 2 = 2 y 2 1
57 sub1m1 2 y 2 y - 1 - 1 = 2 y 2
58 38 57 syl y m 2 y - 1 - 1 = 2 y 2
59 35 37 40 subdid y m 2 y 1 = 2 y 2 1
60 56 58 59 3eqtr4a y m 2 y - 1 - 1 = 2 y 1
61 2nn0 2 0
62 61 a1i y m 2 0
63 nnm1nn0 y y 1 0
64 63 adantr y m y 1 0
65 62 64 nn0mulcld y m 2 y 1 0
66 60 65 eqeltrd y m 2 y - 1 - 1 0
67 35 66 expp1d y m 2 2 y 1 - 1 + 1 = 2 2 y - 1 - 1 2
68 35 66 expcld y m 2 2 y - 1 - 1
69 68 35 mulcomd y m 2 2 y - 1 - 1 2 = 2 2 2 y - 1 - 1
70 67 69 eqtrd y m 2 2 y 1 - 1 + 1 = 2 2 2 y - 1 - 1
71 53 70 eqtrd y m 2 2 y 1 = 2 2 2 y - 1 - 1
72 34 35 37 mul12d y m m 2 y = 2 m y
73 71 72 oveq12d y m 2 2 y 1 m 2 y = 2 2 2 y - 1 - 1 2 m y
74 34 37 mulcld y m m y
75 35 68 74 subdid y m 2 2 2 y - 1 - 1 m y = 2 2 2 y - 1 - 1 2 m y
76 75 eqcomd y m 2 2 2 y - 1 - 1 2 m y = 2 2 2 y - 1 - 1 m y
77 73 76 eqtrd y m 2 2 y 1 m 2 y = 2 2 2 y - 1 - 1 m y
78 77 eqeq1d y m 2 2 y 1 m 2 y = 1 2 2 2 y - 1 - 1 m y = 1
79 zexpcl 2 2 y - 1 - 1 0 2 2 y - 1 - 1
80 19 66 79 sylancr y m 2 2 y - 1 - 1
81 simpr y m m
82 nnz y y
83 82 adantr y m y
84 81 83 zmulcld y m m y
85 80 84 zsubcld y m 2 2 y - 1 - 1 m y
86 m2even 2 2 y - 1 - 1 m y 2 2 2 y - 1 - 1 m y Even
87 85 86 syl y m 2 2 2 y - 1 - 1 m y Even
88 1oddALTV 1 Odd
89 zneoALTV 2 2 2 y - 1 - 1 m y Even 1 Odd 2 2 2 y - 1 - 1 m y 1
90 87 88 89 sylancl y m 2 2 2 y - 1 - 1 m y 1
91 eqneqall 2 2 2 y - 1 - 1 m y = 1 2 2 2 y - 1 - 1 m y 1 X Odd
92 90 91 syl5com y m 2 2 2 y - 1 - 1 m y = 1 X Odd
93 78 92 sylbid y m 2 2 y 1 m 2 y = 1 X Odd
94 44 93 sylbird y m 2 2 y 1 = m 2 y + 1 X Odd
95 94 rexlimdva y m 2 2 y 1 = m 2 y + 1 X Odd
96 29 95 syld y 2 2 y 1 mod 2 y = 1 X Odd
97 96 adantl X 4 y 2 2 y 1 mod 2 y = 1 X Odd
98 97 adantr X 4 y X = 2 y 2 2 y 1 mod 2 y = 1 X Odd
99 18 98 sylbid X 4 y X = 2 y 2 X 1 mod X = 1 X Odd
100 99 ex X 4 y X = 2 y 2 X 1 mod X = 1 X Odd
101 100 rexlimdva X 4 y X = 2 y 2 X 1 mod X = 1 X Odd
102 101 com23 X 4 2 X 1 mod X = 1 y X = 2 y X Odd
103 102 imp X 4 2 X 1 mod X = 1 y X = 2 y X Odd
104 12 103 syld X 4 2 X 1 mod X = 1 ¬ X Odd X Odd
105 104 3adant2 X 4 X 2 X 1 mod X = 1 ¬ X Odd X Odd
106 3 105 sylbi X FPPr 2 ¬ X Odd X Odd
107 106 pm2.18d X FPPr 2 X Odd