Step |
Hyp |
Ref |
Expression |
1 |
|
2lgslem2.n |
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) |
2 |
|
simpl |
|- ( ( P e. Prime /\ -. 2 || P ) -> P e. Prime ) |
3 |
|
elsng |
|- ( P e. Prime -> ( P e. { 2 } <-> P = 2 ) ) |
4 |
|
z2even |
|- 2 || 2 |
5 |
|
breq2 |
|- ( P = 2 -> ( 2 || P <-> 2 || 2 ) ) |
6 |
4 5
|
mpbiri |
|- ( P = 2 -> 2 || P ) |
7 |
3 6
|
syl6bi |
|- ( P e. Prime -> ( P e. { 2 } -> 2 || P ) ) |
8 |
7
|
con3dimp |
|- ( ( P e. Prime /\ -. 2 || P ) -> -. P e. { 2 } ) |
9 |
2 8
|
eldifd |
|- ( ( P e. Prime /\ -. 2 || P ) -> P e. ( Prime \ { 2 } ) ) |
10 |
|
oddprm |
|- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN ) |
11 |
10
|
nnzd |
|- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. ZZ ) |
12 |
9 11
|
syl |
|- ( ( P e. Prime /\ -. 2 || P ) -> ( ( P - 1 ) / 2 ) e. ZZ ) |
13 |
|
prmz |
|- ( P e. Prime -> P e. ZZ ) |
14 |
13
|
zred |
|- ( P e. Prime -> P e. RR ) |
15 |
|
4re |
|- 4 e. RR |
16 |
15
|
a1i |
|- ( P e. Prime -> 4 e. RR ) |
17 |
|
4ne0 |
|- 4 =/= 0 |
18 |
17
|
a1i |
|- ( P e. Prime -> 4 =/= 0 ) |
19 |
14 16 18
|
redivcld |
|- ( P e. Prime -> ( P / 4 ) e. RR ) |
20 |
19
|
flcld |
|- ( P e. Prime -> ( |_ ` ( P / 4 ) ) e. ZZ ) |
21 |
20
|
adantr |
|- ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) e. ZZ ) |
22 |
12 21
|
zsubcld |
|- ( ( P e. Prime /\ -. 2 || P ) -> ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) e. ZZ ) |
23 |
1 22
|
eqeltrid |
|- ( ( P e. Prime /\ -. 2 || P ) -> N e. ZZ ) |