Theorem leibpilem1

Description: Lemma for leibpi . (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by Steven Nguyen, 23-Mar-2023)

	Ref	Expression
Assertion	leibpilem1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0onn	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
2		nn0oddm1d2	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
3	2	biimpa	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
4	1 3	jca	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
5	4	adantrl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )