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	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(\neg N=0\wedge \neg 2\parallel N\right)\right)\to \left(N\in \mathbb{N}\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0onn	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg 2\parallel N\right)\to N\in \mathbb{N}$$
2		nn0oddm1d2	$$⊢N\in {\mathbb{N}}_0\to \left(\neg 2\parallel N\leftrightarrow \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
3	2	biimpa	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg 2\parallel N\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
4	1 3	jca	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg 2\parallel N\right)\to \left(N\in \mathbb{N}\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
5	4	adantrl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(\neg N=0\wedge \neg 2\parallel N\right)\right)\to \left(N\in \mathbb{N}\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$