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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
2		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
3	2	adantl	⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
4		eluz2	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ ∧ 2 ≤ ( ( 2 · 𝑛 ) + 1 ) ) )
5		2re	⊢ 2 ∈ ℝ
6	5	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℝ )
7		1red	⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℝ )
8		2nn0	⊢ 2 ∈ ℕ0
9	8	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 )
10		id	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
11	9 10	nn0mulcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℕ0 )
12	11	nn0red	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℝ )
13	6 7 12	lesubaddd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 − 1 ) ≤ ( 2 · 𝑛 ) ↔ 2 ≤ ( ( 2 · 𝑛 ) + 1 ) ) )
14		2m1e1	⊢ ( 2 − 1 ) = 1
15	14	breq1i	⊢ ( ( 2 − 1 ) ≤ ( 2 · 𝑛 ) ↔ 1 ≤ ( 2 · 𝑛 ) )
16		nn0re	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
17		2rp	⊢ 2 ∈ ℝ+
18	17	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℝ+ )
19	7 16 18	ledivmuld	⊢ ( 𝑛 ∈ ℕ0 → ( ( 1 / 2 ) ≤ 𝑛 ↔ 1 ≤ ( 2 · 𝑛 ) ) )
20		halfgt0	⊢ 0 < ( 1 / 2 )
21		0red	⊢ ( 𝑛 ∈ ℕ0 → 0 ∈ ℝ )
22		halfre	⊢ ( 1 / 2 ) ∈ ℝ
23	22	a1i	⊢ ( 𝑛 ∈ ℕ0 → ( 1 / 2 ) ∈ ℝ )
24		ltletr	⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 0 < ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 𝑛 ) → 0 < 𝑛 ) )
25	21 23 16 24	syl3anc	⊢ ( 𝑛 ∈ ℕ0 → ( ( 0 < ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 𝑛 ) → 0 < 𝑛 ) )
26	20 25	mpani	⊢ ( 𝑛 ∈ ℕ0 → ( ( 1 / 2 ) ≤ 𝑛 → 0 < 𝑛 ) )
27	19 26	sylbird	⊢ ( 𝑛 ∈ ℕ0 → ( 1 ≤ ( 2 · 𝑛 ) → 0 < 𝑛 ) )
28	15 27	biimtrid	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 − 1 ) ≤ ( 2 · 𝑛 ) → 0 < 𝑛 ) )
29	13 28	sylbird	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ≤ ( ( 2 · 𝑛 ) + 1 ) → 0 < 𝑛 ) )
30	29	com12	⊢ ( 2 ≤ ( ( 2 · 𝑛 ) + 1 ) → ( 𝑛 ∈ ℕ0 → 0 < 𝑛 ) )
31	30	3ad2ant3	⊢ ( ( 2 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ ∧ 2 ≤ ( ( 2 · 𝑛 ) + 1 ) ) → ( 𝑛 ∈ ℕ0 → 0 < 𝑛 ) )
32	4 31	sylbi	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ0 → 0 < 𝑛 ) )
33	32	imp	⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 0 < 𝑛 )
34		elnnz	⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℤ ∧ 0 < 𝑛 ) )
35	3 33 34	sylanbrc	⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ )
36	35	ex	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ ) )
37	1 36	biimtrrdi	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ ) ) )
38	37	com13	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → 𝑛 ∈ ℕ ) ) )
39	38	impcom	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → 𝑛 ∈ ℕ ) )
40	39	pm4.71rd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
41	40	bicomd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
42	41	rexbidva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑛 ∈ ℕ0 ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
43		nnssnn0	⊢ ℕ ⊆ ℕ0
44		rexss	⊢ ( ℕ ⊆ ℕ0 → ( ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
45	43 44	mp1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) )
46		eluzge2nn0	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
47		oddnn02np1	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
48	46 47	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
49	42 45 48	3bitr4rd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )