This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )