Theorem xnn01gt

Description: An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than 1. (Contributed by Thierry Arnoux, 21-Nov-2023)

	Ref	Expression
Assertion	xnn01gt	⊢ ( 𝑁 ∈ ℕ0* → ( ¬ 𝑁 ∈ { 0 , 1 } ↔ 1 < 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nelpr	⊢ ( 𝑁 ∈ ℕ0* → ( ¬ 𝑁 ∈ { 0 , 1 } ↔ ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ) )
2		xnn0n0n1ge2b	⊢ ( 𝑁 ∈ ℕ0* → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
3		2nn0	⊢ 2 ∈ ℕ0
4		xnn0lem1lt	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0* ) → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) < 𝑁 ) )
5	3 4	mpan	⊢ ( 𝑁 ∈ ℕ0* → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) < 𝑁 ) )
6		2m1e1	⊢ ( 2 − 1 ) = 1
7	6	breq1i	⊢ ( ( 2 − 1 ) < 𝑁 ↔ 1 < 𝑁 )
8	5 7	bitrdi	⊢ ( 𝑁 ∈ ℕ0* → ( 2 ≤ 𝑁 ↔ 1 < 𝑁 ) )
9	1 2 8	3bitrd	⊢ ( 𝑁 ∈ ℕ0* → ( ¬ 𝑁 ∈ { 0 , 1 } ↔ 1 < 𝑁 ) )