Metamath Proof Explorer

Theorem fmtnoprmfac2lem1

Description: Lemma for fmtnoprmfac2 . (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoprmfac2lem1 
|- ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
3 id 
 |-  ( P || ( FermatNo ` N ) -> P || ( FermatNo ` N ) )
4 fmtnoprmfac1 
 |-  ( ( N e. NN /\ P e. Prime /\ P || ( FermatNo ` N ) ) -> E. n e. NN P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) )
5 1 2 3 4 syl3an 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> E. n e. NN P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) )
6 2z 
 |-  2 e. ZZ
7 simp2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> P e. ( Prime \ { 2 } ) )
8 lgsvalmod 
 |-  ( ( 2 e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 /L P ) mod P ) = ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) )
9 8 eqcomd 
 |-  ( ( 2 e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( 2 /L P ) mod P ) )
10 6 7 9 sylancr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( 2 /L P ) mod P ) )
11 10 ad2antrr 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( 2 /L P ) mod P ) )
12 nncn 
 |-  ( n e. NN -> n e. CC )
13 12 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> n e. CC )
14 2nn 
 |-  2 e. NN
15 14 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. NN )
16 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
17 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
18 16 17 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. NN0 )
19 15 18 nnexpcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. NN )
20 19 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. CC )
21 20 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( 2 ^ ( N + 1 ) ) e. CC )
22 13 21 mulcomd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( n x. ( 2 ^ ( N + 1 ) ) ) = ( ( 2 ^ ( N + 1 ) ) x. n ) )
23 8cn 
 |-  8 e. CC
24 23 a1i 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> 8 e. CC )
25 0re 
 |-  0 e. RR
26 8pos 
 |-  0 < 8
27 25 26 gtneii 
 |-  8 =/= 0
28 27 a1i 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> 8 =/= 0 )
29 21 24 28 divcan2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( 8 x. ( ( 2 ^ ( N + 1 ) ) / 8 ) ) = ( 2 ^ ( N + 1 ) ) )
30 29 eqcomd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( 2 ^ ( N + 1 ) ) = ( 8 x. ( ( 2 ^ ( N + 1 ) ) / 8 ) ) )
31 30 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( 2 ^ ( N + 1 ) ) x. n ) = ( ( 8 x. ( ( 2 ^ ( N + 1 ) ) / 8 ) ) x. n ) )
32 23 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 8 e. CC )
33 27 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 8 =/= 0 )
34 20 32 33 divcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( N + 1 ) ) / 8 ) e. CC )
35 34 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( 2 ^ ( N + 1 ) ) / 8 ) e. CC )
36 24 35 13 mulassd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( 8 x. ( ( 2 ^ ( N + 1 ) ) / 8 ) ) x. n ) = ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) )
37 22 31 36 3eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( n x. ( 2 ^ ( N + 1 ) ) ) = ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) )
38 37 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) )
39 38 eqeq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) <-> P = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) ) )
40 oveq1 
 |-  ( P = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) -> ( P mod 8 ) = ( ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) mod 8 ) )
41 40 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) /\ P = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) ) -> ( P mod 8 ) = ( ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) mod 8 ) )
42 3m1e2 
 |-  ( 3 - 1 ) = 2
43 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
44 42 43 eqbrtrid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 3 - 1 ) <_ N )
45 3re 
 |-  3 e. RR
46 45 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 3 e. RR )
47 1red 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. RR )
48 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
49 46 47 48 lesubaddd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 3 - 1 ) <_ N <-> 3 <_ ( N + 1 ) ) )
50 44 49 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> 3 <_ ( N + 1 ) )
51 3nn0 
 |-  3 e. NN0
52 nn0sub 
 |-  ( ( 3 e. NN0 /\ ( N + 1 ) e. NN0 ) -> ( 3 <_ ( N + 1 ) <-> ( ( N + 1 ) - 3 ) e. NN0 ) )
53 51 18 52 sylancr 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 3 <_ ( N + 1 ) <-> ( ( N + 1 ) - 3 ) e. NN0 ) )
54 50 53 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N + 1 ) - 3 ) e. NN0 )
55 15 54 nnexpcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( N + 1 ) - 3 ) ) e. NN )
56 55 nnzd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( N + 1 ) - 3 ) ) e. ZZ )
57 oveq2 
 |-  ( k = ( 2 ^ ( ( N + 1 ) - 3 ) ) -> ( 8 x. k ) = ( 8 x. ( 2 ^ ( ( N + 1 ) - 3 ) ) ) )
58 57 eqeq1d 
 |-  ( k = ( 2 ^ ( ( N + 1 ) - 3 ) ) -> ( ( 8 x. k ) = ( 2 ^ ( N + 1 ) ) <-> ( 8 x. ( 2 ^ ( ( N + 1 ) - 3 ) ) ) = ( 2 ^ ( N + 1 ) ) ) )
59 58 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ k = ( 2 ^ ( ( N + 1 ) - 3 ) ) ) -> ( ( 8 x. k ) = ( 2 ^ ( N + 1 ) ) <-> ( 8 x. ( 2 ^ ( ( N + 1 ) - 3 ) ) ) = ( 2 ^ ( N + 1 ) ) ) )
60 cu2 
 |-  ( 2 ^ 3 ) = 8
61 60 eqcomi 
 |-  8 = ( 2 ^ 3 )
62 61 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 8 = ( 2 ^ 3 ) )
63 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
64 63 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 e. CC /\ 2 =/= 0 ) )
65 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
66 65 peano2zd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. ZZ )
67 3z 
 |-  3 e. ZZ
68 67 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 3 e. ZZ )
69 expsub 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( N + 1 ) e. ZZ /\ 3 e. ZZ ) ) -> ( 2 ^ ( ( N + 1 ) - 3 ) ) = ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 3 ) ) )
70 64 66 68 69 syl12anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( N + 1 ) - 3 ) ) = ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 3 ) ) )
71 62 70 oveq12d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 8 x. ( 2 ^ ( ( N + 1 ) - 3 ) ) ) = ( ( 2 ^ 3 ) x. ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 3 ) ) ) )
72 nnexpcl 
 |-  ( ( 2 e. NN /\ 3 e. NN0 ) -> ( 2 ^ 3 ) e. NN )
73 14 51 72 mp2an 
 |-  ( 2 ^ 3 ) e. NN
74 73 nncni 
 |-  ( 2 ^ 3 ) e. CC
75 74 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ 3 ) e. CC )
76 2cn 
 |-  2 e. CC
77 2ne0 
 |-  2 =/= 0
78 expne0i 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 3 e. ZZ ) -> ( 2 ^ 3 ) =/= 0 )
79 76 77 67 78 mp3an 
 |-  ( 2 ^ 3 ) =/= 0
80 79 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ 3 ) =/= 0 )
81 20 75 80 divcan2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ 3 ) x. ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 3 ) ) ) = ( 2 ^ ( N + 1 ) ) )
82 71 81 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 8 x. ( 2 ^ ( ( N + 1 ) - 3 ) ) ) = ( 2 ^ ( N + 1 ) ) )
83 56 59 82 rspcedvd 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. k e. ZZ ( 8 x. k ) = ( 2 ^ ( N + 1 ) ) )
84 8nn 
 |-  8 e. NN
85 2nn0 
 |-  2 e. NN0
86 85 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. NN0 )
87 86 18 nn0expcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. NN0 )
88 87 nn0zd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. ZZ )
89 zdiv 
 |-  ( ( 8 e. NN /\ ( 2 ^ ( N + 1 ) ) e. ZZ ) -> ( E. k e. ZZ ( 8 x. k ) = ( 2 ^ ( N + 1 ) ) <-> ( ( 2 ^ ( N + 1 ) ) / 8 ) e. ZZ ) )
90 84 88 89 sylancr 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( E. k e. ZZ ( 8 x. k ) = ( 2 ^ ( N + 1 ) ) <-> ( ( 2 ^ ( N + 1 ) ) / 8 ) e. ZZ ) )
91 83 90 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( N + 1 ) ) / 8 ) e. ZZ )
92 91 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( 2 ^ ( N + 1 ) ) / 8 ) e. ZZ )
93 nnz 
 |-  ( n e. NN -> n e. ZZ )
94 93 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> n e. ZZ )
95 92 94 zmulcld 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) e. ZZ )
96 84 nnzi 
 |-  8 e. ZZ
97 2re 
 |-  2 e. RR
98 8re 
 |-  8 e. RR
99 2lt8 
 |-  2 < 8
100 97 98 99 ltleii 
 |-  2 <_ 8
101 eluz2 
 |-  ( 8 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 8 e. ZZ /\ 2 <_ 8 ) )
102 6 96 100 101 mpbir3an 
 |-  8 e. ( ZZ>= ` 2 )
103 mulp1mod1 
 |-  ( ( ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) e. ZZ /\ 8 e. ( ZZ>= ` 2 ) ) -> ( ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) mod 8 ) = 1 )
104 95 102 103 sylancl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) mod 8 ) = 1 )
105 1nn 
 |-  1 e. NN
106 prid1g 
 |-  ( 1 e. NN -> 1 e. { 1 , 7 } )
107 105 106 mp1i 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> 1 e. { 1 , 7 } )
108 104 107 eqeltrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) mod 8 ) e. { 1 , 7 } )
109 108 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) /\ P = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) ) -> ( ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) mod 8 ) e. { 1 , 7 } )
110 41 109 eqeltrd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) /\ P = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) ) -> ( P mod 8 ) e. { 1 , 7 } )
111 110 ex 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( P = ( ( 8 x. ( ( ( 2 ^ ( N + 1 ) ) / 8 ) x. n ) ) + 1 ) -> ( P mod 8 ) e. { 1 , 7 } ) )
112 39 111 sylbid 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN ) -> ( P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) -> ( P mod 8 ) e. { 1 , 7 } ) )
113 112 3ad2antl1 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) -> ( P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) -> ( P mod 8 ) e. { 1 , 7 } ) )
114 113 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( P mod 8 ) e. { 1 , 7 } )
115 2lgs 
 |-  ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
116 2 115 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
117 116 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
118 117 ad2antrr 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
119 114 118 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( 2 /L P ) = 1 )
120 119 oveq1d 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( ( 2 /L P ) mod P ) = ( 1 mod P ) )
121 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
122 eluzelre 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. RR )
123 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
124 122 123 jca 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P e. RR /\ 1 < P ) )
125 121 124 syl 
 |-  ( P e. Prime -> ( P e. RR /\ 1 < P ) )
126 1mod 
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
127 2 125 126 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 1 mod P ) = 1 )
128 127 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( 1 mod P ) = 1 )
129 128 ad2antrr 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( 1 mod P ) = 1 )
130 11 120 129 3eqtrd 
 |-  ( ( ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) /\ n e. NN ) /\ P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 )
131 130 rexlimdva2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( E. n e. NN P = ( ( n x. ( 2 ^ ( N + 1 ) ) ) + 1 ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 ) )
132 5 131 mpd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || ( FermatNo ` N ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 )