Metamath Proof Explorer


Theorem 2lgslem2

Description: Lemma 2 for 2lgs . (Contributed by AV, 20-Jun-2021)

Ref Expression
Hypothesis 2lgslem2.n
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
Assertion 2lgslem2
|- ( ( P e. Prime /\ -. 2 || P ) -> N e. ZZ )

Proof

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 )