Theorem oddge22np1

Description: An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021) (Proof shortened by AV, 9-Jul-2022)

	Ref	Expression
Assertion	oddge22np1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\neg 2\parallel N\leftrightarrow \exists n\in \mathbb{N}2n+1=N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢2n+1=N\to \left(2n+1\in {\mathbb{Z}}_{\ge 2}\leftrightarrow N\in {\mathbb{Z}}_{\ge 2}\right)$$
2		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
3	2	adantl	$$⊢\left(2n+1\in {\mathbb{Z}}_{\ge 2}\wedge n\in {\mathbb{N}}_0\right)\to n\in \mathbb{Z}$$
4		eluz2	$$⊢2n+1\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 2n+1\in \mathbb{Z}\wedge 2\le 2n+1\right)$$
5		2re	$$⊢2\in ℝ$$
6	5	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in ℝ$$
7		1red	$$⊢n\in {\mathbb{N}}_0\to 1\in ℝ$$
8		2nn0	$$⊢2\in {\mathbb{N}}_0$$
9	8	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
10		id	$$⊢n\in {\mathbb{N}}_0\to n\in {\mathbb{N}}_0$$
11	9 10	nn0mulcld	$$⊢n\in {\mathbb{N}}_0\to 2n\in {\mathbb{N}}_0$$
12	11	nn0red	$$⊢n\in {\mathbb{N}}_0\to 2n\in ℝ$$
13	6 7 12	lesubaddd	$$⊢n\in {\mathbb{N}}_0\to \left(2-1\le 2n\leftrightarrow 2\le 2n+1\right)$$
14		2m1e1	$$⊢2-1=1$$
15	14	breq1i	$$⊢2-1\le 2n\leftrightarrow 1\le 2n$$
16		nn0re	$$⊢n\in {\mathbb{N}}_0\to n\in ℝ$$
17		2rp	$$⊢2\in {ℝ}^{+}$$
18	17	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in {ℝ}^{+}$$
19	7 16 18	ledivmuld	$$⊢n\in {\mathbb{N}}_0\to \left(\frac{1}{2}\le n\leftrightarrow 1\le 2n\right)$$
20		halfgt0	$$⊢0<\frac{1}{2}$$
21		0red	$$⊢n\in {\mathbb{N}}_0\to 0\in ℝ$$
22		halfre	$$⊢\frac{1}{2}\in ℝ$$
23	22	a1i	$$⊢n\in {\mathbb{N}}_0\to \frac{1}{2}\in ℝ$$
24		ltletr	$$⊢\left(0\in ℝ\wedge \frac{1}{2}\in ℝ\wedge n\in ℝ\right)\to \left(\left(0<\frac{1}{2}\wedge \frac{1}{2}\le n\right)\to 0<n\right)$$
25	21 23 16 24	syl3anc	$$⊢n\in {\mathbb{N}}_0\to \left(\left(0<\frac{1}{2}\wedge \frac{1}{2}\le n\right)\to 0<n\right)$$
26	20 25	mpani	$$⊢n\in {\mathbb{N}}_0\to \left(\frac{1}{2}\le n\to 0<n\right)$$
27	19 26	sylbird	$$⊢n\in {\mathbb{N}}_0\to \left(1\le 2n\to 0<n\right)$$
28	15 27	biimtrid	$$⊢n\in {\mathbb{N}}_0\to \left(2-1\le 2n\to 0<n\right)$$
29	13 28	sylbird	$$⊢n\in {\mathbb{N}}_0\to \left(2\le 2n+1\to 0<n\right)$$
30	29	com12	$$⊢2\le 2n+1\to \left(n\in {\mathbb{N}}_0\to 0<n\right)$$
31	30	3ad2ant3	$$⊢\left(2\in \mathbb{Z}\wedge 2n+1\in \mathbb{Z}\wedge 2\le 2n+1\right)\to \left(n\in {\mathbb{N}}_0\to 0<n\right)$$
32	4 31	sylbi	$$⊢2n+1\in {\mathbb{Z}}_{\ge 2}\to \left(n\in {\mathbb{N}}_0\to 0<n\right)$$
33	32	imp	$$⊢\left(2n+1\in {\mathbb{Z}}_{\ge 2}\wedge n\in {\mathbb{N}}_0\right)\to 0<n$$
34		elnnz	$$⊢n\in \mathbb{N}\leftrightarrow \left(n\in \mathbb{Z}\wedge 0<n\right)$$
35	3 33 34	sylanbrc	$$⊢\left(2n+1\in {\mathbb{Z}}_{\ge 2}\wedge n\in {\mathbb{N}}_0\right)\to n\in \mathbb{N}$$
36	35	ex	$$⊢2n+1\in {\mathbb{Z}}_{\ge 2}\to \left(n\in {\mathbb{N}}_0\to n\in \mathbb{N}\right)$$
37	1 36	biimtrrdi	$$⊢2n+1=N\to \left(N\in {\mathbb{Z}}_{\ge 2}\to \left(n\in {\mathbb{N}}_0\to n\in \mathbb{N}\right)\right)$$
38	37	com13	$$⊢n\in {\mathbb{N}}_0\to \left(N\in {\mathbb{Z}}_{\ge 2}\to \left(2n+1=N\to n\in \mathbb{N}\right)\right)$$
39	38	impcom	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge n\in {\mathbb{N}}_0\right)\to \left(2n+1=N\to n\in \mathbb{N}\right)$$
40	39	pm4.71rd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge n\in {\mathbb{N}}_0\right)\to \left(2n+1=N\leftrightarrow \left(n\in \mathbb{N}\wedge 2n+1=N\right)\right)$$
41	40	bicomd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge n\in {\mathbb{N}}_0\right)\to \left(\left(n\in \mathbb{N}\wedge 2n+1=N\right)\leftrightarrow 2n+1=N\right)$$
42	41	rexbidva	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\exists n\in {\mathbb{N}}_0\left(n\in \mathbb{N}\wedge 2n+1=N\right)\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n+1=N\right)$$
43		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
44		rexss	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left(\exists n\in \mathbb{N}2n+1=N\leftrightarrow \exists n\in {\mathbb{N}}_0\left(n\in \mathbb{N}\wedge 2n+1=N\right)\right)$$
45	43 44	mp1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\exists n\in \mathbb{N}2n+1=N\leftrightarrow \exists n\in {\mathbb{N}}_0\left(n\in \mathbb{N}\wedge 2n+1=N\right)\right)$$
46		eluzge2nn0	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in {\mathbb{N}}_0$$
47		oddnn02np1	$$⊢N\in {\mathbb{N}}_0\to \left(\neg 2\parallel N\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n+1=N\right)$$
48	46 47	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\neg 2\parallel N\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n+1=N\right)$$
49	42 45 48	3bitr4rd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\neg 2\parallel N\leftrightarrow \exists n\in \mathbb{N}2n+1=N\right)$$