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

Metamath Proof Explorer

Theorem nn0n0n1ge2b

Description: A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018)

Ref Expression
Assertion nn0n0n1ge2b 
|- ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )

Proof

Step Hyp Ref Expression
1 nn0n0n1ge2 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> 2 <_ N )
2 1 3expib 
 |-  ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) -> 2 <_ N ) )
3 ianor 
 |-  ( -. ( N =/= 0 /\ N =/= 1 ) <-> ( -. N =/= 0 \/ -. N =/= 1 ) )
4 nne 
 |-  ( -. N =/= 0 <-> N = 0 )
5 nne 
 |-  ( -. N =/= 1 <-> N = 1 )
6 4 5 orbi12i 
 |-  ( ( -. N =/= 0 \/ -. N =/= 1 ) <-> ( N = 0 \/ N = 1 ) )
7 3 6 bitri 
 |-  ( -. ( N =/= 0 /\ N =/= 1 ) <-> ( N = 0 \/ N = 1 ) )
8 2pos 
 |-  0 < 2
9 breq1 
 |-  ( N = 0 -> ( N < 2 <-> 0 < 2 ) )
10 8 9 mpbiri 
 |-  ( N = 0 -> N < 2 )
11 10 a1d 
 |-  ( N = 0 -> ( N e. NN0 -> N < 2 ) )
12 1lt2 
 |-  1 < 2
13 breq1 
 |-  ( N = 1 -> ( N < 2 <-> 1 < 2 ) )
14 12 13 mpbiri 
 |-  ( N = 1 -> N < 2 )
15 14 a1d 
 |-  ( N = 1 -> ( N e. NN0 -> N < 2 ) )
16 11 15 jaoi 
 |-  ( ( N = 0 \/ N = 1 ) -> ( N e. NN0 -> N < 2 ) )
17 16 impcom 
 |-  ( ( N e. NN0 /\ ( N = 0 \/ N = 1 ) ) -> N < 2 )
18 nn0re 
 |-  ( N e. NN0 -> N e. RR )
19 2re 
 |-  2 e. RR
20 18 19 jctir 
 |-  ( N e. NN0 -> ( N e. RR /\ 2 e. RR ) )
21 20 adantr 
 |-  ( ( N e. NN0 /\ ( N = 0 \/ N = 1 ) ) -> ( N e. RR /\ 2 e. RR ) )
22 ltnle 
 |-  ( ( N e. RR /\ 2 e. RR ) -> ( N < 2 <-> -. 2 <_ N ) )
23 21 22 syl 
 |-  ( ( N e. NN0 /\ ( N = 0 \/ N = 1 ) ) -> ( N < 2 <-> -. 2 <_ N ) )
24 17 23 mpbid 
 |-  ( ( N e. NN0 /\ ( N = 0 \/ N = 1 ) ) -> -. 2 <_ N )
25 24 ex 
 |-  ( N e. NN0 -> ( ( N = 0 \/ N = 1 ) -> -. 2 <_ N ) )
26 7 25 biimtrid 
 |-  ( N e. NN0 -> ( -. ( N =/= 0 /\ N =/= 1 ) -> -. 2 <_ N ) )
27 2 26 impcon4bid 
 |-  ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )