Metamath Proof Explorer

Theorem fzo1fzo0n0

Description: An integer between 1 and an upper bound of a half-open integer range is not 0 and between 0 and the upper bound of the half-open integer range. (Contributed by Alexander van der Vekens, 21-Mar-2018)

Ref Expression
Assertion fzo1fzo0n0 
|- ( K e. ( 1 ..^ N ) <-> ( K e. ( 0 ..^ N ) /\ K =/= 0 ) )

Proof

Step Hyp Ref Expression
1 elfzo2 
 |-  ( K e. ( 1 ..^ N ) <-> ( K e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ K < N ) )
2 elnnuz 
 |-  ( K e. NN <-> K e. ( ZZ>= ` 1 ) )
3 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
4 3 adantr 
 |-  ( ( K e. NN /\ N e. ZZ ) -> K e. NN0 )
5 4 adantr 
 |-  ( ( ( K e. NN /\ N e. ZZ ) /\ K < N ) -> K e. NN0 )
6 nngt0 
 |-  ( K e. NN -> 0 < K )
7 0red 
 |-  ( ( N e. ZZ /\ K e. NN ) -> 0 e. RR )
8 nnre 
 |-  ( K e. NN -> K e. RR )
9 8 adantl 
 |-  ( ( N e. ZZ /\ K e. NN ) -> K e. RR )
10 zre 
 |-  ( N e. ZZ -> N e. RR )
11 10 adantr 
 |-  ( ( N e. ZZ /\ K e. NN ) -> N e. RR )
12 lttr 
 |-  ( ( 0 e. RR /\ K e. RR /\ N e. RR ) -> ( ( 0 < K /\ K < N ) -> 0 < N ) )
13 7 9 11 12 syl3anc 
 |-  ( ( N e. ZZ /\ K e. NN ) -> ( ( 0 < K /\ K < N ) -> 0 < N ) )
14 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
15 14 simplbi2 
 |-  ( N e. ZZ -> ( 0 < N -> N e. NN ) )
16 15 adantr 
 |-  ( ( N e. ZZ /\ K e. NN ) -> ( 0 < N -> N e. NN ) )
17 13 16 syld 
 |-  ( ( N e. ZZ /\ K e. NN ) -> ( ( 0 < K /\ K < N ) -> N e. NN ) )
18 17 exp4b 
 |-  ( N e. ZZ -> ( K e. NN -> ( 0 < K -> ( K < N -> N e. NN ) ) ) )
19 18 com13 
 |-  ( 0 < K -> ( K e. NN -> ( N e. ZZ -> ( K < N -> N e. NN ) ) ) )
20 6 19 mpcom 
 |-  ( K e. NN -> ( N e. ZZ -> ( K < N -> N e. NN ) ) )
21 20 imp31 
 |-  ( ( ( K e. NN /\ N e. ZZ ) /\ K < N ) -> N e. NN )
22 simpr 
 |-  ( ( ( K e. NN /\ N e. ZZ ) /\ K < N ) -> K < N )
23 5 21 22 3jca 
 |-  ( ( ( K e. NN /\ N e. ZZ ) /\ K < N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
24 23 exp31 
 |-  ( K e. NN -> ( N e. ZZ -> ( K < N -> ( K e. NN0 /\ N e. NN /\ K < N ) ) ) )
25 2 24 sylbir 
 |-  ( K e. ( ZZ>= ` 1 ) -> ( N e. ZZ -> ( K < N -> ( K e. NN0 /\ N e. NN /\ K < N ) ) ) )
26 25 3imp 
 |-  ( ( K e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ K < N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
27 elfzo0 
 |-  ( K e. ( 0 ..^ N ) <-> ( K e. NN0 /\ N e. NN /\ K < N ) )
28 26 27 sylibr 
 |-  ( ( K e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ K < N ) -> K e. ( 0 ..^ N ) )
29 nnne0 
 |-  ( K e. NN -> K =/= 0 )
30 2 29 sylbir 
 |-  ( K e. ( ZZ>= ` 1 ) -> K =/= 0 )
31 30 3ad2ant1 
 |-  ( ( K e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ K < N ) -> K =/= 0 )
32 28 31 jca 
 |-  ( ( K e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ K < N ) -> ( K e. ( 0 ..^ N ) /\ K =/= 0 ) )
33 1 32 sylbi 
 |-  ( K e. ( 1 ..^ N ) -> ( K e. ( 0 ..^ N ) /\ K =/= 0 ) )
34 elnnne0 
 |-  ( K e. NN <-> ( K e. NN0 /\ K =/= 0 ) )
35 nnge1 
 |-  ( K e. NN -> 1 <_ K )
36 34 35 sylbir 
 |-  ( ( K e. NN0 /\ K =/= 0 ) -> 1 <_ K )
37 36 3ad2antl1 
 |-  ( ( ( K e. NN0 /\ N e. NN /\ K < N ) /\ K =/= 0 ) -> 1 <_ K )
38 simpl3 
 |-  ( ( ( K e. NN0 /\ N e. NN /\ K < N ) /\ K =/= 0 ) -> K < N )
39 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
40 39 adantr 
 |-  ( ( K e. NN0 /\ N e. NN ) -> K e. ZZ )
41 1zzd 
 |-  ( ( K e. NN0 /\ N e. NN ) -> 1 e. ZZ )
42 nnz 
 |-  ( N e. NN -> N e. ZZ )
43 42 adantl 
 |-  ( ( K e. NN0 /\ N e. NN ) -> N e. ZZ )
44 40 41 43 3jca 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( K e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) )
45 44 3adant3 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( K e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) )
46 45 adantr 
 |-  ( ( ( K e. NN0 /\ N e. NN /\ K < N ) /\ K =/= 0 ) -> ( K e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) )
47 elfzo 
 |-  ( ( K e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( K e. ( 1 ..^ N ) <-> ( 1 <_ K /\ K < N ) ) )
48 46 47 syl 
 |-  ( ( ( K e. NN0 /\ N e. NN /\ K < N ) /\ K =/= 0 ) -> ( K e. ( 1 ..^ N ) <-> ( 1 <_ K /\ K < N ) ) )
49 37 38 48 mpbir2and 
 |-  ( ( ( K e. NN0 /\ N e. NN /\ K < N ) /\ K =/= 0 ) -> K e. ( 1 ..^ N ) )
50 27 49 sylanb 
 |-  ( ( K e. ( 0 ..^ N ) /\ K =/= 0 ) -> K e. ( 1 ..^ N ) )
51 33 50 impbii 
 |-  ( K e. ( 1 ..^ N ) <-> ( K e. ( 0 ..^ N ) /\ K =/= 0 ) )