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	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N - 1}{2} \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3		nn0o1gt2	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to (N = 1 \lor 2 < N)$
4	2 3	sylan	$⊢ (N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \to (N = 1 \lor 2 < N)$
5		eqneqall	$⊢ N = 1 \to (N \neq 1 \to \frac{N - 1}{2} \in ℕ)$
6	5	a1d	$⊢ N = 1 \to ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \to (N \neq 1 \to \frac{N - 1}{2} \in ℕ))$
7		nn0z	$⊢ \frac{N + 1}{2} \in ℕ_{0} \to \frac{N + 1}{2} \in ℤ$
8		peano2zm	$⊢ \frac{N + 1}{2} \in ℤ \to (\frac{N + 1}{2}) - 1 \in ℤ$
9	7 8	syl	$⊢ \frac{N + 1}{2} \in ℕ_{0} \to (\frac{N + 1}{2}) - 1 \in ℤ$
10	9	ad2antlr	$⊢ ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \land 2 < N) \to (\frac{N + 1}{2}) - 1 \in ℤ$
11		2cn	$⊢ 2 \in ℂ$
12	11	mullidi	$⊢ 1 \cdot 2 = 2$
13		nnre	$⊢ N \in ℕ \to N \in ℝ$
14	13	ltp1d	$⊢ N \in ℕ \to N < N + 1$
15	14	adantr	$⊢ (N \in ℕ \land 2 < N) \to N < N + 1$
16		2re	$⊢ 2 \in ℝ$
17		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
18	17	nnred	$⊢ N \in ℕ \to N + 1 \in ℝ$
19		lttr	$⊢ (2 \in ℝ \land N \in ℝ \land N + 1 \in ℝ) \to ((2 < N \land N < N + 1) \to 2 < N + 1)$
20	16 13 18 19	mp3an2i	$⊢ N \in ℕ \to ((2 < N \land N < N + 1) \to 2 < N + 1)$
21	20	expdimp	$⊢ (N \in ℕ \land 2 < N) \to (N < N + 1 \to 2 < N + 1)$
22	15 21	mpd	$⊢ (N \in ℕ \land 2 < N) \to 2 < N + 1$
23	12 22	eqbrtrid	$⊢ (N \in ℕ \land 2 < N) \to 1 \cdot 2 < N + 1$
24		1red	$⊢ (N \in ℕ \land 2 < N) \to 1 \in ℝ$
25	18	adantr	$⊢ (N \in ℕ \land 2 < N) \to N + 1 \in ℝ$
26		2rp	$⊢ 2 \in ℝ^{+}$
27	26	a1i	$⊢ (N \in ℕ \land 2 < N) \to 2 \in ℝ^{+}$
28	24 25 27	ltmuldivd	$⊢ (N \in ℕ \land 2 < N) \to (1 \cdot 2 < N + 1 \leftrightarrow 1 < \frac{N + 1}{2})$
29	23 28	mpbid	$⊢ (N \in ℕ \land 2 < N) \to 1 < \frac{N + 1}{2}$
30	18	rehalfcld	$⊢ N \in ℕ \to \frac{N + 1}{2} \in ℝ$
31	30	adantr	$⊢ (N \in ℕ \land 2 < N) \to \frac{N + 1}{2} \in ℝ$
32	24 31	posdifd	$⊢ (N \in ℕ \land 2 < N) \to (1 < \frac{N + 1}{2} \leftrightarrow 0 < (\frac{N + 1}{2}) - 1)$
33	29 32	mpbid	$⊢ (N \in ℕ \land 2 < N) \to 0 < (\frac{N + 1}{2}) - 1$
34	33	adantlr	$⊢ ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \land 2 < N) \to 0 < (\frac{N + 1}{2}) - 1$
35		elnnz	$⊢ (\frac{N + 1}{2}) - 1 \in ℕ \leftrightarrow ((\frac{N + 1}{2}) - 1 \in ℤ \land 0 < (\frac{N + 1}{2}) - 1)$
36	10 34 35	sylanbrc	$⊢ ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \land 2 < N) \to (\frac{N + 1}{2}) - 1 \in ℕ$
37		nncn	$⊢ N \in ℕ \to N \in ℂ$
38		xp1d2m1eqxm1d2	$⊢ N \in ℂ \to (\frac{N + 1}{2}) - 1 = \frac{N - 1}{2}$
39	37 38	syl	$⊢ N \in ℕ \to (\frac{N + 1}{2}) - 1 = \frac{N - 1}{2}$
40	39	eleq1d	$⊢ N \in ℕ \to ((\frac{N + 1}{2}) - 1 \in ℕ \leftrightarrow \frac{N - 1}{2} \in ℕ)$
41	40	adantr	$⊢ (N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \to ((\frac{N + 1}{2}) - 1 \in ℕ \leftrightarrow \frac{N - 1}{2} \in ℕ)$
42	41	adantr	$⊢ ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \land 2 < N) \to ((\frac{N + 1}{2}) - 1 \in ℕ \leftrightarrow \frac{N - 1}{2} \in ℕ)$
43	36 42	mpbid	$⊢ ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \land 2 < N) \to \frac{N - 1}{2} \in ℕ$
44	43	a1d	$⊢ ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \land 2 < N) \to (N \neq 1 \to \frac{N - 1}{2} \in ℕ)$
45	44	expcom	$⊢ 2 < N \to ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \to (N \neq 1 \to \frac{N - 1}{2} \in ℕ))$
46	6 45	jaoi	$⊢ (N = 1 \lor 2 < N) \to ((N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \to (N \neq 1 \to \frac{N - 1}{2} \in ℕ))$
47	4 46	mpcom	$⊢ (N \in ℕ \land \frac{N + 1}{2} \in ℕ_{0}) \to (N \neq 1 \to \frac{N - 1}{2} \in ℕ)$
48	47	impancom	$⊢ (N \in ℕ \land N \neq 1) \to (\frac{N + 1}{2} \in ℕ_{0} \to \frac{N - 1}{2} \in ℕ)$
49	1 48	sylbi	$⊢ N \in ℤ_{\geq 2} \to (\frac{N + 1}{2} \in ℕ_{0} \to \frac{N - 1}{2} \in ℕ)$
50	49	imp	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N - 1}{2} \in ℕ$

Metamath Proof Explorer

Theorem nno

Proof