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

Metamath Proof Explorer

Theorem nn01to3

Description: A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 3mix3 
 |-  ( N = 3 -> ( N = 1 \/ N = 2 \/ N = 3 ) )
2 1 a1d 
 |-  ( N = 3 -> ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( N = 1 \/ N = 2 \/ N = 3 ) ) )
3 nn0re 
 |-  ( N e. NN0 -> N e. RR )
4 3 3ad2ant1 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> N e. RR )
5 3re 
 |-  3 e. RR
6 5 a1i 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> 3 e. RR )
7 simp3 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> N <_ 3 )
8 4 6 7 leltned 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( N < 3 <-> 3 =/= N ) )
9 nesym 
 |-  ( 3 =/= N <-> -. N = 3 )
10 8 9 bitr2di 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( -. N = 3 <-> N < 3 ) )
11 elnnnn0c 
 |-  ( N e. NN <-> ( N e. NN0 /\ 1 <_ N ) )
12 orc 
 |-  ( N = 1 -> ( N = 1 \/ N = 2 ) )
13 12 2a1d 
 |-  ( N = 1 -> ( N e. NN -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) ) )
14 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
15 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
16 2a1 
 |-  ( N = 2 -> ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( N < 3 -> N = 2 ) ) )
17 zre 
 |-  ( 2 e. ZZ -> 2 e. RR )
18 zre 
 |-  ( N e. ZZ -> N e. RR )
19 id 
 |-  ( 2 <_ N -> 2 <_ N )
20 leltne 
 |-  ( ( 2 e. RR /\ N e. RR /\ 2 <_ N ) -> ( 2 < N <-> N =/= 2 ) )
21 17 18 19 20 syl3an 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( 2 < N <-> N =/= 2 ) )
22 2z 
 |-  2 e. ZZ
23 simpr 
 |-  ( ( ( N e. ZZ /\ N < 3 ) /\ 2 < N ) -> 2 < N )
24 df-3 
 |-  3 = ( 2 + 1 )
25 24 a1i 
 |-  ( N e. ZZ -> 3 = ( 2 + 1 ) )
26 25 breq2d 
 |-  ( N e. ZZ -> ( N < 3 <-> N < ( 2 + 1 ) ) )
27 26 biimpa 
 |-  ( ( N e. ZZ /\ N < 3 ) -> N < ( 2 + 1 ) )
28 27 adantr 
 |-  ( ( ( N e. ZZ /\ N < 3 ) /\ 2 < N ) -> N < ( 2 + 1 ) )
29 btwnnz 
 |-  ( ( 2 e. ZZ /\ 2 < N /\ N < ( 2 + 1 ) ) -> -. N e. ZZ )
30 22 23 28 29 mp3an2i 
 |-  ( ( ( N e. ZZ /\ N < 3 ) /\ 2 < N ) -> -. N e. ZZ )
31 30 pm2.21d 
 |-  ( ( ( N e. ZZ /\ N < 3 ) /\ 2 < N ) -> ( N e. ZZ -> N = 2 ) )
32 31 exp31 
 |-  ( N e. ZZ -> ( N < 3 -> ( 2 < N -> ( N e. ZZ -> N = 2 ) ) ) )
33 32 com24 
 |-  ( N e. ZZ -> ( N e. ZZ -> ( 2 < N -> ( N < 3 -> N = 2 ) ) ) )
34 33 pm2.43i 
 |-  ( N e. ZZ -> ( 2 < N -> ( N < 3 -> N = 2 ) ) )
35 34 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( 2 < N -> ( N < 3 -> N = 2 ) ) )
36 21 35 sylbird 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( N =/= 2 -> ( N < 3 -> N = 2 ) ) )
37 36 com12 
 |-  ( N =/= 2 -> ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( N < 3 -> N = 2 ) ) )
38 16 37 pm2.61ine 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( N < 3 -> N = 2 ) )
39 15 38 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 3 -> N = 2 ) )
40 39 imp 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N < 3 ) -> N = 2 )
41 40 olcd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N < 3 ) -> ( N = 1 \/ N = 2 ) )
42 41 ex 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) )
43 14 42 sylbir 
 |-  ( ( N e. NN /\ N =/= 1 ) -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) )
44 43 expcom 
 |-  ( N =/= 1 -> ( N e. NN -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) ) )
45 13 44 pm2.61ine 
 |-  ( N e. NN -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) )
46 11 45 sylbir 
 |-  ( ( N e. NN0 /\ 1 <_ N ) -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) )
47 46 3adant3 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( N < 3 -> ( N = 1 \/ N = 2 ) ) )
48 10 47 sylbid 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( -. N = 3 -> ( N = 1 \/ N = 2 ) ) )
49 48 impcom 
 |-  ( ( -. N = 3 /\ ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) ) -> ( N = 1 \/ N = 2 ) )
50 49 orcd 
 |-  ( ( -. N = 3 /\ ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) ) -> ( ( N = 1 \/ N = 2 ) \/ N = 3 ) )
51 df-3or 
 |-  ( ( N = 1 \/ N = 2 \/ N = 3 ) <-> ( ( N = 1 \/ N = 2 ) \/ N = 3 ) )
52 50 51 sylibr 
 |-  ( ( -. N = 3 /\ ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) ) -> ( N = 1 \/ N = 2 \/ N = 3 ) )
53 52 ex 
 |-  ( -. N = 3 -> ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( N = 1 \/ N = 2 \/ N = 3 ) ) )
54 2 53 pm2.61i 
 |-  ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( N = 1 \/ N = 2 \/ N = 3 ) )