Metamath Proof Explorer


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