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

Metamath Proof Explorer

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