Metamath Proof Explorer

Theorem fmtnoprmfac1lem

Description: Lemma for fmtnoprmfac1 : The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021) (Proof shortened by AV, 18-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
2 prmnn 
 |-  ( P e. Prime -> P e. NN )
3 1 2 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. NN )
4 3 ad2antlr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ P || ( FermatNo ` N ) ) -> P e. NN )
5 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 fmtno 
 |-  ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
7 5 6 syl 
 |-  ( N e. NN -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
8 7 breq2d 
 |-  ( N e. NN -> ( P || ( FermatNo ` N ) <-> P || ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) )
9 8 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P || ( FermatNo ` N ) <-> P || ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) )
10 9 biimpa 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ P || ( FermatNo ` N ) ) -> P || ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
11 dvdsmod0 
 |-  ( ( P e. NN /\ P || ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 )
12 4 10 11 syl2anc 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ P || ( FermatNo ` N ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 )
13 12 ex 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P || ( FermatNo ` N ) -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 ) )
14 2nn 
 |-  2 e. NN
15 14 a1i 
 |-  ( N e. NN -> 2 e. NN )
16 2nn0 
 |-  2 e. NN0
17 16 a1i 
 |-  ( N e. NN -> 2 e. NN0 )
18 17 5 nn0expcld 
 |-  ( N e. NN -> ( 2 ^ N ) e. NN0 )
19 15 18 nnexpcld 
 |-  ( N e. NN -> ( 2 ^ ( 2 ^ N ) ) e. NN )
20 19 nnzd 
 |-  ( N e. NN -> ( 2 ^ ( 2 ^ N ) ) e. ZZ )
21 20 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 ^ ( 2 ^ N ) ) e. ZZ )
22 1zzd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> 1 e. ZZ )
23 3 adantl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> P e. NN )
24 summodnegmod 
 |-  ( ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ 1 e. ZZ /\ P e. NN ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 <-> ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) )
25 21 22 23 24 syl3anc 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 <-> ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) )
26 neg1z 
 |-  -u 1 e. ZZ
27 21 26 jctir 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ -u 1 e. ZZ ) )
28 27 adantr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ -u 1 e. ZZ ) )
29 2 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
30 1 29 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. RR+ )
31 17 30 anim12i 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 e. NN0 /\ P e. RR+ ) )
32 31 adantr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( 2 e. NN0 /\ P e. RR+ ) )
33 simpr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) )
34 modexp 
 |-  ( ( ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ -u 1 e. ZZ ) /\ ( 2 e. NN0 /\ P e. RR+ ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) mod P ) = ( ( -u 1 ^ 2 ) mod P ) )
35 28 32 33 34 syl3anc 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) mod P ) = ( ( -u 1 ^ 2 ) mod P ) )
36 35 ex 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) -> ( ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) mod P ) = ( ( -u 1 ^ 2 ) mod P ) ) )
37 2cnd 
 |-  ( N e. NN -> 2 e. CC )
38 37 18 17 3jca 
 |-  ( N e. NN -> ( 2 e. CC /\ ( 2 ^ N ) e. NN0 /\ 2 e. NN0 ) )
39 38 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 e. CC /\ ( 2 ^ N ) e. NN0 /\ 2 e. NN0 ) )
40 expmul 
 |-  ( ( 2 e. CC /\ ( 2 ^ N ) e. NN0 /\ 2 e. NN0 ) -> ( 2 ^ ( ( 2 ^ N ) x. 2 ) ) = ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) )
41 39 40 syl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 ^ ( ( 2 ^ N ) x. 2 ) ) = ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) )
42 2cnd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> 2 e. CC )
43 5 adantr 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> N e. NN0 )
44 42 43 expp1d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
45 44 eqcomd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 ^ N ) x. 2 ) = ( 2 ^ ( N + 1 ) ) )
46 45 oveq2d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 2 ^ ( ( 2 ^ N ) x. 2 ) ) = ( 2 ^ ( 2 ^ ( N + 1 ) ) ) )
47 41 46 eqtr3d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) = ( 2 ^ ( 2 ^ ( N + 1 ) ) ) )
48 47 oveq1d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) mod P ) = ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) )
49 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
50 49 a1i 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( -u 1 ^ 2 ) = 1 )
51 50 oveq1d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( -u 1 ^ 2 ) mod P ) = ( 1 mod P ) )
52 3 nnred 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. RR )
53 prmgt1 
 |-  ( P e. Prime -> 1 < P )
54 1 53 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> 1 < P )
55 1mod 
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
56 52 54 55 syl2anc 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 1 mod P ) = 1 )
57 56 adantl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( 1 mod P ) = 1 )
58 51 57 eqtrd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( -u 1 ^ 2 ) mod P ) = 1 )
59 48 58 eqeq12d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) mod P ) = ( ( -u 1 ^ 2 ) mod P ) <-> ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) )
60 simpll 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 ) -> ( N e. NN /\ P e. ( Prime \ { 2 } ) ) )
61 20 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 ^ ( 2 ^ N ) ) e. ZZ )
62 1zzd 
 |-  ( ( N e. NN /\ P e. Prime ) -> 1 e. ZZ )
63 2 adantl 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. NN )
64 61 62 63 3jca 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ 1 e. ZZ /\ P e. NN ) )
65 1 64 sylan2 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ 1 e. ZZ /\ P e. NN ) )
66 65 adantr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) -> ( ( 2 ^ ( 2 ^ N ) ) e. ZZ /\ 1 e. ZZ /\ P e. NN ) )
67 66 24 syl 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 <-> ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) )
68 m1modnnsub1 
 |-  ( P e. NN -> ( -u 1 mod P ) = ( P - 1 ) )
69 23 68 syl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( -u 1 mod P ) = ( P - 1 ) )
70 eldifsni 
 |-  ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
71 70 adantl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> P =/= 2 )
72 71 necomd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> 2 =/= P )
73 3 nncnd 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. CC )
74 73 adantl 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> P e. CC )
75 1cnd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> 1 e. CC )
76 74 75 75 subadd2d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( P - 1 ) = 1 <-> ( 1 + 1 ) = P ) )
77 1p1e2 
 |-  ( 1 + 1 ) = 2
78 77 eqeq1i 
 |-  ( ( 1 + 1 ) = P <-> 2 = P )
79 76 78 bitrdi 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( P - 1 ) = 1 <-> 2 = P ) )
80 79 necon3bid 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( P - 1 ) =/= 1 <-> 2 =/= P ) )
81 72 80 mpbird 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P - 1 ) =/= 1 )
82 69 81 eqnetrd 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( -u 1 mod P ) =/= 1 )
83 82 adantr 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) -> ( -u 1 mod P ) =/= 1 )
84 83 adantr 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( -u 1 mod P ) =/= 1 )
85 eqeq1 
 |-  ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = 1 <-> ( -u 1 mod P ) = 1 ) )
86 85 adantl 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = 1 <-> ( -u 1 mod P ) = 1 ) )
87 86 necon3bid 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 <-> ( -u 1 mod P ) =/= 1 ) )
88 84 87 mpbird 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 )
89 88 ex 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) -> ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 ) )
90 67 89 sylbid 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 ) )
91 90 imp 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 ) -> ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 )
92 simplr 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 ) -> ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 )
93 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 ) ) )
94 60 91 92 93 syl12anc 
 |-  ( ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )
95 94 ex 
 |-  ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) )
96 95 ex 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
97 59 96 sylbid 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) mod P ) = ( ( -u 1 ^ 2 ) mod P ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
98 36 97 syld 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) = ( -u 1 mod P ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
99 25 98 sylbid 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) ) )
100 99 pm2.43d 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) mod P ) = 0 -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) )
101 13 100 syld 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) -> ( P || ( FermatNo ` N ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) )
102 101 3impia 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )