Theorem 2lgslem2

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

	Ref	Expression
Hypothesis	2lgslem2.n	⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
Assertion	2lgslem2	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → 𝑁 ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		2lgslem2.n	⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
2		simpl	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℙ )
3		elsng	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ { 2 } ↔ 𝑃 = 2 ) )
4		z2even	⊢ 2 ∥ 2
5		breq2	⊢ ( 𝑃 = 2 → ( 2 ∥ 𝑃 ↔ 2 ∥ 2 ) )
6	4 5	mpbiri	⊢ ( 𝑃 = 2 → 2 ∥ 𝑃 )
7	3 6	biimtrdi	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ { 2 } → 2 ∥ 𝑃 ) )
8	7	con3dimp	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ¬ 𝑃 ∈ { 2 } )
9	2 8	eldifd	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
10		oddprm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
11	10	nnzd	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
12	9 11	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
13		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
14	13	zred	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
15		4re	⊢ 4 ∈ ℝ
16	15	a1i	⊢ ( 𝑃 ∈ ℙ → 4 ∈ ℝ )
17		4ne0	⊢ 4 ≠ 0
18	17	a1i	⊢ ( 𝑃 ∈ ℙ → 4 ≠ 0 )
19	14 16 18	redivcld	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 / 4 ) ∈ ℝ )
20	19	flcld	⊢ ( 𝑃 ∈ ℙ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
21	20	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
22	12 21	zsubcld	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) ∈ ℤ )
23	1 22	eqeltrid	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → 𝑁 ∈ ℤ )