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 e. ( FPPr ` 2 ) -> X e. Odd )

Proof

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