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 N0*¬N011<N

Proof

Step Hyp Ref Expression
1 nelpr N0*¬N01N0N1
2 xnn0n0n1ge2b N0*N0N12N
3 2nn0 20
4 xnn0lem1lt 20N0*2N21<N
5 3 4 mpan N0*2N21<N
6 2m1e1 21=1
7 6 breq1i 21<N1<N
8 5 7 bitrdi N0*2N1<N
9 1 2 8 3bitrd N0*¬N011<N