Metamath Proof Explorer

Theorem odz2prm2pw

Description: Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021)

Ref Expression
Assertion odz2prm2pw 
|- ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( N e. NN -> 2 e. NN )
4 2nn0 
 |-  2 e. NN0
5 4 a1i 
 |-  ( N e. NN -> 2 e. NN0 )
6 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
7 6 nnnn0d 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
8 5 7 nn0expcld 
 |-  ( N e. NN -> ( 2 ^ ( N + 1 ) ) e. NN0 )
9 3 8 nnexpcld 
 |-  ( N e. NN -> ( 2 ^ ( 2 ^ ( N + 1 ) ) ) e. NN )
10 9 nnzd 
 |-  ( N e. NN -> ( 2 ^ ( 2 ^ ( N + 1 ) ) ) e. ZZ )
11 modprm1div 
 |-  ( ( P e. Prime /\ ( 2 ^ ( 2 ^ ( N + 1 ) ) ) e. ZZ ) -> ( ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 <-> P || ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) - 1 ) ) )
12 1 10 11 syl2anr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 <-> P || ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) - 1 ) ) )
13 prmnn 
 |-  ( P e. Prime -> P e. NN )
14 1 13 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. NN )
15 14 adantl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> P e. NN )
16 2z 
 |-  2 e. ZZ
17 16 a1i 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> 2 e. ZZ )
18 eldifsn 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
19 simpr 
 |-  ( ( P e. Prime /\ P =/= 2 ) -> P =/= 2 )
20 19 necomd 
 |-  ( ( P e. Prime /\ P =/= 2 ) -> 2 =/= P )
21 18 20 sylbi 
 |-  ( P e. ( Prime \ { 2 } ) -> 2 =/= P )
22 2prm 
 |-  2 e. Prime
23 prmrp 
 |-  ( ( 2 e. Prime /\ P e. Prime ) -> ( ( 2 gcd P ) = 1 <-> 2 =/= P ) )
24 22 1 23 sylancr 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( 2 gcd P ) = 1 <-> 2 =/= P ) )
25 21 24 mpbird 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 2 gcd P ) = 1 )
26 25 adantl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 gcd P ) = 1 )
27 15 17 26 3jca 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) )
28 8 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 ^ ( N + 1 ) ) e. NN0 )
29 odzdvds 
 |-  ( ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( 2 ^ ( N + 1 ) ) e. NN0 ) -> ( P || ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) - 1 ) <-> ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) ) )
30 27 28 29 syl2anc 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P || ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) - 1 ) <-> ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) ) )
31 12 30 bitrd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 <-> ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) ) )
32 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
33 5 32 nn0expcld 
 |-  ( N e. NN -> ( 2 ^ N ) e. NN0 )
34 3 33 nnexpcld 
 |-  ( N e. NN -> ( 2 ^ ( 2 ^ N ) ) e. NN )
35 34 nnzd 
 |-  ( N e. NN -> ( 2 ^ ( 2 ^ N ) ) e. ZZ )
36 modprm1div 
 |-  ( ( P e. Prime /\ ( 2 ^ ( 2 ^ N ) ) e. ZZ ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = 1 <-> P || ( ( 2 ^ ( 2 ^ N ) ) - 1 ) ) )
37 1 35 36 syl2anr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = 1 <-> P || ( ( 2 ^ ( 2 ^ N ) ) - 1 ) ) )
38 33 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 ^ N ) e. NN0 )
39 odzdvds 
 |-  ( ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( 2 ^ N ) e. NN0 ) -> ( P || ( ( 2 ^ ( 2 ^ N ) ) - 1 ) <-> ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) ) )
40 27 38 39 syl2anc 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P || ( ( 2 ^ ( 2 ^ N ) ) - 1 ) <-> ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) ) )
41 37 40 bitrd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = 1 <-> ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) ) )
42 41 necon3abid 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 <-> -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) ) )
43 odzcl 
 |-  ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) -> ( ( odZ ` P ) ` 2 ) e. NN )
44 27 43 syl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( odZ ` P ) ` 2 ) e. NN )
45 7 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( N + 1 ) e. NN0 )
46 dvdsprmpweqle 
 |-  ( ( 2 e. Prime /\ ( ( odZ ` P ) ` 2 ) e. NN /\ ( N + 1 ) e. NN0 ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) -> E. n e. NN0 ( n <_ ( N + 1 ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) ) )
47 22 44 45 46 mp3an2i 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) -> E. n e. NN0 ( n <_ ( N + 1 ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) ) )
48 breq1 
 |-  ( ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) <-> ( 2 ^ n ) || ( 2 ^ N ) ) )
49 48 adantl 
 |-  ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) <-> ( 2 ^ n ) || ( 2 ^ N ) ) )
50 49 notbid 
 |-  ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) <-> -. ( 2 ^ n ) || ( 2 ^ N ) ) )
51 simpr 
 |-  ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) )
52 51 adantr 
 |-  ( ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) /\ -. ( 2 ^ n ) || ( 2 ^ N ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) )
53 nn0re 
 |-  ( n e. NN0 -> n e. RR )
54 6 nnred 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
55 54 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( N + 1 ) e. RR )
56 leloe 
 |-  ( ( n e. RR /\ ( N + 1 ) e. RR ) -> ( n <_ ( N + 1 ) <-> ( n < ( N + 1 ) \/ n = ( N + 1 ) ) ) )
57 53 55 56 syl2anr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( n <_ ( N + 1 ) <-> ( n < ( N + 1 ) \/ n = ( N + 1 ) ) ) )
58 simpr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> n e. NN0 )
59 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
60 59 adantl 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> n e. ZZ )
61 60 adantr 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n < ( N + 1 ) ) -> n e. ZZ )
62 nnz 
 |-  ( N e. NN -> N e. ZZ )
63 62 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> N e. ZZ )
64 63 adantr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> N e. ZZ )
65 64 adantr 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n < ( N + 1 ) ) -> N e. ZZ )
66 zleltp1 
 |-  ( ( n e. ZZ /\ N e. ZZ ) -> ( n <_ N <-> n < ( N + 1 ) ) )
67 59 63 66 syl2anr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( n <_ N <-> n < ( N + 1 ) ) )
68 67 biimpar 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n < ( N + 1 ) ) -> n <_ N )
69 eluz2 
 |-  ( N e. ( ZZ>= ` n ) <-> ( n e. ZZ /\ N e. ZZ /\ n <_ N ) )
70 61 65 68 69 syl3anbrc 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n < ( N + 1 ) ) -> N e. ( ZZ>= ` n ) )
71 dvdsexp 
 |-  ( ( 2 e. ZZ /\ n e. NN0 /\ N e. ( ZZ>= ` n ) ) -> ( 2 ^ n ) || ( 2 ^ N ) )
72 16 58 70 71 mp3an2ani 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n < ( N + 1 ) ) -> ( 2 ^ n ) || ( 2 ^ N ) )
73 72 pm2.24d 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n < ( N + 1 ) ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) )
74 73 expcom 
 |-  ( n < ( N + 1 ) -> ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) ) )
75 oveq2 
 |-  ( n = ( N + 1 ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) )
76 75 2a1d 
 |-  ( n = ( N + 1 ) -> ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) ) )
77 74 76 jaoi 
 |-  ( ( n < ( N + 1 ) \/ n = ( N + 1 ) ) -> ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) ) )
78 77 com12 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( ( n < ( N + 1 ) \/ n = ( N + 1 ) ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) ) )
79 57 78 sylbid 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( n <_ ( N + 1 ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) ) )
80 79 imp 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) )
81 80 adantr 
 |-  ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) ) )
82 81 imp 
 |-  ( ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) /\ -. ( 2 ^ n ) || ( 2 ^ N ) ) -> ( 2 ^ n ) = ( 2 ^ ( N + 1 ) ) )
83 52 82 eqtrd 
 |-  ( ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) /\ -. ( 2 ^ n ) || ( 2 ^ N ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )
84 83 ex 
 |-  ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( -. ( 2 ^ n ) || ( 2 ^ N ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) )
85 50 84 sylbid 
 |-  ( ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) /\ n <_ ( N + 1 ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) )
86 85 expl 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ n e. NN0 ) -> ( ( n <_ ( N + 1 ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
87 86 rexlimdva 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( E. n e. NN0 ( n <_ ( N + 1 ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ n ) ) -> ( -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
88 47 87 syld 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) -> ( -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
89 88 com23 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( -. ( ( odZ ` P ) ` 2 ) || ( 2 ^ N ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
90 42 89 sylbid 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
91 90 com23 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( 2 ^ ( N + 1 ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
92 31 91 sylbid 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
93 92 com23 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 -> ( ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
94 93 imp32 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )