leibpilem1

		Ref	Expression
	Assertion	leibpilem1	$⊢ (N \in ℕ_{0} \land (\neg N = 0 \land \neg 2 ∥ N)) \to (N \in ℕ \land \frac{N - 1}{2} \in ℕ_{0})$

Step	Hyp	Ref	Expression
1		nn0onn	$⊢ (N \in ℕ_{0} \land \neg 2 ∥ N) \to N \in ℕ$
2		nn0oddm1d2	$⊢ N \in ℕ_{0} \to (\neg 2 ∥ N \leftrightarrow \frac{N - 1}{2} \in ℕ_{0})$
3	2	biimpa	$⊢ (N \in ℕ_{0} \land \neg 2 ∥ N) \to \frac{N - 1}{2} \in ℕ_{0}$
4	1 3	jca	$⊢ (N \in ℕ_{0} \land \neg 2 ∥ N) \to (N \in ℕ \land \frac{N - 1}{2} \in ℕ_{0})$
5	4	adantrl	$⊢ (N \in ℕ_{0} \land (\neg N = 0 \land \neg 2 ∥ N)) \to (N \in ℕ \land \frac{N - 1}{2} \in ℕ_{0})$

Metamath Proof Explorer