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