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	|- ( N e. NN0* -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )

Proof

Step	Hyp	Ref	Expression
1		elxnn0	|- ( N e. NN0* <-> ( N e. NN0 \/ N = +oo ) )
2		nn0n0n1ge2b	|- ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )
3		0nn0	|- 0 e. NN0
4		nn0nepnf	|- ( 0 e. NN0 -> 0 =/= +oo )
5	3 4	ax-mp	|- 0 =/= +oo
6	5	necomi	|- +oo =/= 0
7		neeq1	|- ( N = +oo -> ( N =/= 0 <-> +oo =/= 0 ) )
8	6 7	mpbiri	|- ( N = +oo -> N =/= 0 )
9		1nn0	|- 1 e. NN0
10		nn0nepnf	|- ( 1 e. NN0 -> 1 =/= +oo )
11	9 10	ax-mp	|- 1 =/= +oo
12	11	necomi	|- +oo =/= 1
13		neeq1	|- ( N = +oo -> ( N =/= 1 <-> +oo =/= 1 ) )
14	12 13	mpbiri	|- ( N = +oo -> N =/= 1 )
15	8 14	jca	|- ( N = +oo -> ( N =/= 0 /\ N =/= 1 ) )
16		2re	|- 2 e. RR
17	16	rexri	|- 2 e. RR*
18		pnfge	|- ( 2 e. RR* -> 2 <_ +oo )
19	17 18	ax-mp	|- 2 <_ +oo
20		breq2	|- ( N = +oo -> ( 2 <_ N <-> 2 <_ +oo ) )
21	19 20	mpbiri	|- ( N = +oo -> 2 <_ N )
22	15 21	2thd	|- ( N = +oo -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )
23	2 22	jaoi	|- ( ( N e. NN0 \/ N = +oo ) -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )
24	1 23	sylbi	|- ( N e. NN0* -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )