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	biimtrdi	|- ( 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 )