Theorem nno

Description: An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Assertion	nno	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		eluz2b3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
2		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3		nn0o1gt2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
4	2 3	sylan	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
5		eqneqall	⊢ ( 𝑁 = 1 → ( 𝑁 ≠ 1 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
6	5	a1d	⊢ ( 𝑁 = 1 → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 ≠ 1 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) ) )
7		nn0z	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
8		peano2zm	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ )
9	7 8	syl	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ )
10	9	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ∧ 2 < 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ )
11		2cn	⊢ 2 ∈ ℂ
12	11	mullidi	⊢ ( 1 · 2 ) = 2
13		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
14	13	ltp1d	⊢ ( 𝑁 ∈ ℕ → 𝑁 < ( 𝑁 + 1 ) )
15	14	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 𝑁 < ( 𝑁 + 1 ) )
16		2re	⊢ 2 ∈ ℝ
17		peano2nn	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
18	17	nnred	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
19		lttr	⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ) → ( ( 2 < 𝑁 ∧ 𝑁 < ( 𝑁 + 1 ) ) → 2 < ( 𝑁 + 1 ) ) )
20	16 13 18 19	mp3an2i	⊢ ( 𝑁 ∈ ℕ → ( ( 2 < 𝑁 ∧ 𝑁 < ( 𝑁 + 1 ) ) → 2 < ( 𝑁 + 1 ) ) )
21	20	expdimp	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝑁 < ( 𝑁 + 1 ) → 2 < ( 𝑁 + 1 ) ) )
22	15 21	mpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 2 < ( 𝑁 + 1 ) )
23	12 22	eqbrtrid	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 1 · 2 ) < ( 𝑁 + 1 ) )
24		1red	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 1 ∈ ℝ )
25	18	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 𝑁 + 1 ) ∈ ℝ )
26		2rp	⊢ 2 ∈ ℝ+
27	26	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 2 ∈ ℝ+ )
28	24 25 27	ltmuldivd	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 1 · 2 ) < ( 𝑁 + 1 ) ↔ 1 < ( ( 𝑁 + 1 ) / 2 ) ) )
29	23 28	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 1 < ( ( 𝑁 + 1 ) / 2 ) )
30	18	rehalfcld	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℝ )
31	30	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℝ )
32	24 31	posdifd	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → ( 1 < ( ( 𝑁 + 1 ) / 2 ) ↔ 0 < ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ) )
33	29 32	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) → 0 < ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) )
34	33	adantlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ∧ 2 < 𝑁 ) → 0 < ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) )
35		elnnz	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℕ ↔ ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ ∧ 0 < ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ) )
36	10 34 35	sylanbrc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ∧ 2 < 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℕ )
37		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
38		xp1d2m1eqxm1d2	⊢ ( 𝑁 ∈ ℂ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) = ( ( 𝑁 − 1 ) / 2 ) )
39	37 38	syl	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) = ( ( 𝑁 − 1 ) / 2 ) )
40	39	eleq1d	⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℕ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
41	40	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℕ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
42	41	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ∧ 2 < 𝑁 ) → ( ( ( ( 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℕ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
43	36 42	mpbid	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ∧ 2 < 𝑁 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )
44	43	a1d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ∧ 2 < 𝑁 ) → ( 𝑁 ≠ 1 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
45	44	expcom	⊢ ( 2 < 𝑁 → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 ≠ 1 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) ) )
46	6 45	jaoi	⊢ ( ( 𝑁 = 1 ∨ 2 < 𝑁 ) → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 ≠ 1 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) ) )
47	4 46	mpcom	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 ≠ 1 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
48	47	impancom	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
49	1 48	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
50	49	imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )