Theorem 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	⊢ ( 𝑁 ∈ ℕ0* → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elxnn0	⊢ ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
2		nn0n0n1ge2b	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
3		0nn0	⊢ 0 ∈ ℕ0
4		nn0nepnf	⊢ ( 0 ∈ ℕ0 → 0 ≠ +∞ )
5	3 4	ax-mp	⊢ 0 ≠ +∞
6	5	necomi	⊢ +∞ ≠ 0
7		neeq1	⊢ ( 𝑁 = +∞ → ( 𝑁 ≠ 0 ↔ +∞ ≠ 0 ) )
8	6 7	mpbiri	⊢ ( 𝑁 = +∞ → 𝑁 ≠ 0 )
9		1nn0	⊢ 1 ∈ ℕ0
10		nn0nepnf	⊢ ( 1 ∈ ℕ0 → 1 ≠ +∞ )
11	9 10	ax-mp	⊢ 1 ≠ +∞
12	11	necomi	⊢ +∞ ≠ 1
13		neeq1	⊢ ( 𝑁 = +∞ → ( 𝑁 ≠ 1 ↔ +∞ ≠ 1 ) )
14	12 13	mpbiri	⊢ ( 𝑁 = +∞ → 𝑁 ≠ 1 )
15	8 14	jca	⊢ ( 𝑁 = +∞ → ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) )
16		2re	⊢ 2 ∈ ℝ
17	16	rexri	⊢ 2 ∈ ℝ*
18		pnfge	⊢ ( 2 ∈ ℝ* → 2 ≤ +∞ )
19	17 18	ax-mp	⊢ 2 ≤ +∞
20		breq2	⊢ ( 𝑁 = +∞ → ( 2 ≤ 𝑁 ↔ 2 ≤ +∞ ) )
21	19 20	mpbiri	⊢ ( 𝑁 = +∞ → 2 ≤ 𝑁 )
22	15 21	2thd	⊢ ( 𝑁 = +∞ → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
23	2 22	jaoi	⊢ ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
24	1 23	sylbi	⊢ ( 𝑁 ∈ ℕ0* → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )