Metamath Proof Explorer

Theorem fmtnoprmfac2

Description: Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 ): Let F_n be a Fermat number. Let p be a prime divisor of F_n. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoprmfac2 
|- ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( P = 2 -> ( P || ( FermatNo ` N ) <-> 2 || ( FermatNo ` N ) ) )
2 1 adantr 
 |-  ( ( P = 2 /\ N e. ( ZZ>= ` 2 ) ) -> ( P || ( FermatNo ` N ) <-> 2 || ( FermatNo ` N ) ) )
3 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
4 fmtnoodd 
 |-  ( N e. NN0 -> -. 2 || ( FermatNo ` N ) )
5 3 4 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> -. 2 || ( FermatNo ` N ) )
6 5 adantl 
 |-  ( ( P = 2 /\ N e. ( ZZ>= ` 2 ) ) -> -. 2 || ( FermatNo ` N ) )
7 6 pm2.21d 
 |-  ( ( P = 2 /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 || ( FermatNo ` N ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
8 2 7 sylbid 
 |-  ( ( P = 2 /\ N e. ( ZZ>= ` 2 ) ) -> ( P || ( FermatNo ` N ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
9 8 a1d 
 |-  ( ( P = 2 /\ N e. ( ZZ>= ` 2 ) ) -> ( P e. Prime -> ( P || ( FermatNo ` N ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
10 9 ex 
 |-  ( P = 2 -> ( N e. ( ZZ>= ` 2 ) -> ( P e. Prime -> ( P || ( FermatNo ` N ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) ) )
11 10 3impd 
 |-  ( P = 2 -> ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
12 simpr1 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> N e. ( ZZ>= ` 2 ) )
13 neqne 
 |-  ( -. P = 2 -> P =/= 2 )
14 13 anim2i 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( P e. Prime /\ P =/= 2 ) )
15 eldifsn 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
16 14 15 sylibr 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> P e. ( Prime \ { 2 } ) )
17 16 ex 
 |-  ( P e. Prime -> ( -. P = 2 -> P e. ( Prime \ { 2 } ) ) )
18 17 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> ( -. P = 2 -> P e. ( Prime \ { 2 } ) ) )
19 18 impcom 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> P e. ( Prime \ { 2 } ) )
20 simpr3 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> P || ( FermatNo ` N ) )
21 fmtnoprmfac2lem1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 )
22 12 19 20 21 syl3anc 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 )
23 simpl 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> P e. Prime )
24 2nn 
 |-  2 e. NN
25 24 a1i 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> 2 e. NN )
26 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
27 16 26 syl 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( ( P - 1 ) / 2 ) e. NN )
28 27 nnnn0d 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( ( P - 1 ) / 2 ) e. NN0 )
29 25 28 nnexpcld 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( 2 ^ ( ( P - 1 ) / 2 ) ) e. NN )
30 29 nnzd 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( 2 ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
31 23 30 jca 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( P e. Prime /\ ( 2 ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) )
32 31 ex 
 |-  ( P e. Prime -> ( -. P = 2 -> ( P e. Prime /\ ( 2 ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) ) )
33 32 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> ( -. P = 2 -> ( P e. Prime /\ ( 2 ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) ) )
34 33 impcom 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( P e. Prime /\ ( 2 ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) )
35 modprm1div 
 |-  ( ( P e. Prime /\ ( 2 ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) -> ( ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 <-> P || ( ( 2 ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
36 34 35 syl 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 <-> P || ( ( 2 ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
37 prmnn 
 |-  ( P e. Prime -> P e. NN )
38 37 adantr 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> P e. NN )
39 2z 
 |-  2 e. ZZ
40 39 a1i 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> 2 e. ZZ )
41 13 necomd 
 |-  ( -. P = 2 -> 2 =/= P )
42 41 adantl 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> 2 =/= P )
43 2prm 
 |-  2 e. Prime
44 43 a1i 
 |-  ( -. P = 2 -> 2 e. Prime )
45 44 anim2i 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( P e. Prime /\ 2 e. Prime ) )
46 45 ancomd 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( 2 e. Prime /\ P e. Prime ) )
47 prmrp 
 |-  ( ( 2 e. Prime /\ P e. Prime ) -> ( ( 2 gcd P ) = 1 <-> 2 =/= P ) )
48 46 47 syl 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( ( 2 gcd P ) = 1 <-> 2 =/= P ) )
49 42 48 mpbird 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( 2 gcd P ) = 1 )
50 38 40 49 3jca 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) )
51 50 28 jca 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( ( P - 1 ) / 2 ) e. NN0 ) )
52 51 ex 
 |-  ( P e. Prime -> ( -. P = 2 -> ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( ( P - 1 ) / 2 ) e. NN0 ) ) )
53 52 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> ( -. P = 2 -> ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( ( P - 1 ) / 2 ) e. NN0 ) ) )
54 53 impcom 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( ( P - 1 ) / 2 ) e. NN0 ) )
55 odzdvds 
 |-  ( ( ( P e. NN /\ 2 e. ZZ /\ ( 2 gcd P ) = 1 ) /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( P || ( ( 2 ^ ( ( P - 1 ) / 2 ) ) - 1 ) <-> ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) ) )
56 54 55 syl 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( P || ( ( 2 ^ ( ( P - 1 ) / 2 ) ) - 1 ) <-> ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) ) )
57 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
58 57 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> N e. NN )
59 58 adantl 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> N e. NN )
60 fmtnoprmfac1lem 
 |-  ( ( N e. NN /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )
61 59 19 20 60 syl3anc 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )
62 breq1 
 |-  ( ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) <-> ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) ) )
63 62 adantl 
 |-  ( ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) <-> ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) ) )
64 24 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. NN )
65 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
66 57 65 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. NN )
67 66 nnnn0d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. NN0 )
68 64 67 nnexpcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. NN )
69 nndivides 
 |-  ( ( ( 2 ^ ( N + 1 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN ) -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) <-> E. k e. NN ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) ) )
70 68 27 69 syl2an 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( P e. Prime /\ -. P = 2 ) ) -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) <-> E. k e. NN ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) ) )
71 eqcom 
 |-  ( ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) <-> ( ( P - 1 ) / 2 ) = ( k x. ( 2 ^ ( N + 1 ) ) ) )
72 71 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) <-> ( ( P - 1 ) / 2 ) = ( k x. ( 2 ^ ( N + 1 ) ) ) ) )
73 37 nncnd 
 |-  ( P e. Prime -> P e. CC )
74 peano2cnm 
 |-  ( P e. CC -> ( P - 1 ) e. CC )
75 73 74 syl 
 |-  ( P e. Prime -> ( P - 1 ) e. CC )
76 75 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( P - 1 ) e. CC )
77 76 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( P - 1 ) e. CC )
78 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> k e. NN )
79 68 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( 2 ^ ( N + 1 ) ) e. NN )
80 78 79 nnmulcld 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( k x. ( 2 ^ ( N + 1 ) ) ) e. NN )
81 80 nncnd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( k x. ( 2 ^ ( N + 1 ) ) ) e. CC )
82 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
83 82 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( 2 e. CC /\ 2 =/= 0 ) )
84 divmul3 
 |-  ( ( ( P - 1 ) e. CC /\ ( k x. ( 2 ^ ( N + 1 ) ) ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( P - 1 ) / 2 ) = ( k x. ( 2 ^ ( N + 1 ) ) ) <-> ( P - 1 ) = ( ( k x. ( 2 ^ ( N + 1 ) ) ) x. 2 ) ) )
85 77 81 83 84 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( ( P - 1 ) / 2 ) = ( k x. ( 2 ^ ( N + 1 ) ) ) <-> ( P - 1 ) = ( ( k x. ( 2 ^ ( N + 1 ) ) ) x. 2 ) ) )
86 nncn 
 |-  ( k e. NN -> k e. CC )
87 86 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> k e. CC )
88 68 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. CC )
89 88 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( 2 ^ ( N + 1 ) ) e. CC )
90 2cnd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> 2 e. CC )
91 87 89 90 mulassd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( k x. ( 2 ^ ( N + 1 ) ) ) x. 2 ) = ( k x. ( ( 2 ^ ( N + 1 ) ) x. 2 ) ) )
92 2cnd 
 |-  ( N e. NN -> 2 e. CC )
93 65 nnnn0d 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
94 92 93 expp1d 
 |-  ( N e. NN -> ( 2 ^ ( ( N + 1 ) + 1 ) ) = ( ( 2 ^ ( N + 1 ) ) x. 2 ) )
95 nncn 
 |-  ( N e. NN -> N e. CC )
96 add1p1 
 |-  ( N e. CC -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
97 95 96 syl 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
98 97 oveq2d 
 |-  ( N e. NN -> ( 2 ^ ( ( N + 1 ) + 1 ) ) = ( 2 ^ ( N + 2 ) ) )
99 94 98 eqtr3d 
 |-  ( N e. NN -> ( ( 2 ^ ( N + 1 ) ) x. 2 ) = ( 2 ^ ( N + 2 ) ) )
100 57 99 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( N + 1 ) ) x. 2 ) = ( 2 ^ ( N + 2 ) ) )
101 100 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( 2 ^ ( N + 1 ) ) x. 2 ) = ( 2 ^ ( N + 2 ) ) )
102 101 oveq2d 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( k x. ( ( 2 ^ ( N + 1 ) ) x. 2 ) ) = ( k x. ( 2 ^ ( N + 2 ) ) ) )
103 91 102 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( k x. ( 2 ^ ( N + 1 ) ) ) x. 2 ) = ( k x. ( 2 ^ ( N + 2 ) ) ) )
104 103 eqeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( P - 1 ) = ( ( k x. ( 2 ^ ( N + 1 ) ) ) x. 2 ) <-> ( P - 1 ) = ( k x. ( 2 ^ ( N + 2 ) ) ) ) )
105 73 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> P e. CC )
106 105 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> P e. CC )
107 1cnd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> 1 e. CC )
108 id 
 |-  ( N e. NN -> N e. NN )
109 24 a1i 
 |-  ( N e. NN -> 2 e. NN )
110 108 109 nnaddcld 
 |-  ( N e. NN -> ( N + 2 ) e. NN )
111 110 nnnn0d 
 |-  ( N e. NN -> ( N + 2 ) e. NN0 )
112 57 111 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 2 ) e. NN0 )
113 64 112 nnexpcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 2 ) ) e. NN )
114 113 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 2 ) ) e. CC )
115 114 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( 2 ^ ( N + 2 ) ) e. CC )
116 87 115 mulcld 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( k x. ( 2 ^ ( N + 2 ) ) ) e. CC )
117 106 107 116 subadd2d 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( P - 1 ) = ( k x. ( 2 ^ ( N + 2 ) ) ) <-> ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = P ) )
118 eqcom 
 |-  ( ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = P <-> P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
119 118 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = P <-> P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
120 104 117 119 3bitrd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( P - 1 ) = ( ( k x. ( 2 ^ ( N + 1 ) ) ) x. 2 ) <-> P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
121 72 85 120 3bitrd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) /\ k e. NN ) -> ( ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) <-> P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
122 121 rexbidva 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( E. k e. NN ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) <-> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
123 122 biimpd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( E. k e. NN ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
124 123 adantrr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( P e. Prime /\ -. P = 2 ) ) -> ( E. k e. NN ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
125 70 124 sylbid 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( P e. Prime /\ -. P = 2 ) ) -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
126 125 expr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( -. P = 2 -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
127 126 3adant3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> ( -. P = 2 -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
128 127 impcom 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
129 128 adantr 
 |-  ( ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) -> ( ( 2 ^ ( N + 1 ) ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
130 63 129 sylbid 
 |-  ( ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) /\ ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
131 130 ex 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
132 61 131 mpd 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( ( odZ ` P ) ` 2 ) || ( ( P - 1 ) / 2 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
133 56 132 sylbid 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( P || ( ( 2 ^ ( ( P - 1 ) / 2 ) ) - 1 ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
134 36 133 sylbid 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> ( ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
135 22 134 mpd 
 |-  ( ( -. P = 2 /\ ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
136 135 ex 
 |-  ( -. P = 2 -> ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
137 11 136 pm2.61i 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )