xnn0n0n1ge2b

Description: An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021)

		Ref	Expression
	Assertion	xnn0n0n1ge2b	$⊢ N \in ℕ_{0}^{*} \to ((N \neq 0 \land N \neq 1) \leftrightarrow 2 \leq N)$

Step	Hyp	Ref	Expression
1		elxnn0	$⊢ N \in ℕ_{0}^{*} \leftrightarrow (N \in ℕ_{0} \lor N = +∞)$
2		nn0n0n1ge2b	$⊢ N \in ℕ_{0} \to ((N \neq 0 \land N \neq 1) \leftrightarrow 2 \leq N)$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4		nn0nepnf	$⊢ 0 \in ℕ_{0} \to 0 \neq +∞$
5	3 4	ax-mp	$⊢ 0 \neq +∞$
6	5	necomi	$⊢ +∞ \neq 0$
7		neeq1	$⊢ N = +∞ \to (N \neq 0 \leftrightarrow +∞ \neq 0)$
8	6 7	mpbiri	$⊢ N = +∞ \to N \neq 0$
9		1nn0	$⊢ 1 \in ℕ_{0}$
10		nn0nepnf	$⊢ 1 \in ℕ_{0} \to 1 \neq +∞$
11	9 10	ax-mp	$⊢ 1 \neq +∞$
12	11	necomi	$⊢ +∞ \neq 1$
13		neeq1	$⊢ N = +∞ \to (N \neq 1 \leftrightarrow +∞ \neq 1)$
14	12 13	mpbiri	$⊢ N = +∞ \to N \neq 1$
15	8 14	jca	$⊢ N = +∞ \to (N \neq 0 \land N \neq 1)$
16		2re	$⊢ 2 \in ℝ$
17	16	rexri	$⊢ 2 \in ℝ^{*}$
18		pnfge	$⊢ 2 \in ℝ^{*} \to 2 \leq +∞$
19	17 18	ax-mp	$⊢ 2 \leq +∞$
20		breq2	$⊢ N = +∞ \to (2 \leq N \leftrightarrow 2 \leq +∞)$
21	19 20	mpbiri	$⊢ N = +∞ \to 2 \leq N$
22	15 21	2thd	$⊢ N = +∞ \to ((N \neq 0 \land N \neq 1) \leftrightarrow 2 \leq N)$
23	2 22	jaoi	$⊢ (N \in ℕ_{0} \lor N = +∞) \to ((N \neq 0 \land N \neq 1) \leftrightarrow 2 \leq N)$
24	1 23	sylbi	$⊢ N \in ℕ_{0}^{*} \to ((N \neq 0 \land N \neq 1) \leftrightarrow 2 \leq N)$

Metamath Proof Explorer