Theorem gausslemma2dlem0b

Description: Auxiliary lemma 2 for gausslemma2d . (Contributed by AV, 9-Jul-2021)

	Ref	Expression
Hypotheses	gausslemma2dlem0a.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	gausslemma2dlem0b.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
Assertion	gausslemma2dlem0b	⊢ ( 𝜑 → 𝐻 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0a.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		gausslemma2dlem0b.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3		eldifi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
4		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
5	3 4	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
6		nnoddn2prm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
7		nnoddm1d2	⊢ ( 𝑃 ∈ ℕ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ ) )
8	7	biimpa	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ )
9	8	nnnn0d	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ0 )
10	6 9	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ0 )
11	5 10	jca	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ0 ) )
12	1 11	syl	⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ0 ) )
13		nno	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑃 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
14	12 13	syl	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
15	2 14	eqeltrid	⊢ ( 𝜑 → 𝐻 ∈ ℕ )