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	|- ( N e. NN0* -> ( -. N e. { 0 , 1 } <-> 1 < N ) )

Proof

Step	Hyp	Ref	Expression
1		nelpr	|- ( N e. NN0* -> ( -. N e. { 0 , 1 } <-> ( N =/= 0 /\ N =/= 1 ) ) )
2		xnn0n0n1ge2b	|- ( N e. NN0* -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )
3		2nn0	|- 2 e. NN0
4		xnn0lem1lt	|- ( ( 2 e. NN0 /\ N e. NN0* ) -> ( 2 <_ N <-> ( 2 - 1 ) < N ) )
5	3 4	mpan	|- ( N e. NN0* -> ( 2 <_ N <-> ( 2 - 1 ) < N ) )
6		2m1e1	|- ( 2 - 1 ) = 1
7	6	breq1i	|- ( ( 2 - 1 ) < N <-> 1 < N )
8	5 7	bitrdi	|- ( N e. NN0* -> ( 2 <_ N <-> 1 < N ) )
9	1 2 8	3bitrd	|- ( N e. NN0* -> ( -. N e. { 0 , 1 } <-> 1 < N ) )