Metamath Proof Explorer

Theorem ubmelm1fzo

Description: The result of subtracting 1 and an integer of a half-open range of nonnegative integers from the upper bound of this range is contained in this range. (Contributed by AV, 23-Mar-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion ubmelm1fzo 
|- ( K e. ( 0 ..^ N ) -> ( ( N - K ) - 1 ) e. ( 0 ..^ N ) )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( K e. ( 0 ..^ N ) <-> ( K e. NN0 /\ N e. NN /\ K < N ) )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 2 adantr 
 |-  ( ( N e. NN /\ K e. NN0 ) -> N e. ZZ )
4 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
5 4 adantl 
 |-  ( ( N e. NN /\ K e. NN0 ) -> K e. ZZ )
6 3 5 zsubcld 
 |-  ( ( N e. NN /\ K e. NN0 ) -> ( N - K ) e. ZZ )
7 6 ancoms 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( N - K ) e. ZZ )
8 peano2zm 
 |-  ( ( N - K ) e. ZZ -> ( ( N - K ) - 1 ) e. ZZ )
9 7 8 syl 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( N - K ) - 1 ) e. ZZ )
10 9 3adant3 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( ( N - K ) - 1 ) e. ZZ )
11 simp3 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> K < N )
12 4 2 anim12i 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( K e. ZZ /\ N e. ZZ ) )
13 12 3adant3 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( K e. ZZ /\ N e. ZZ ) )
14 znnsub 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> ( N - K ) e. NN ) )
15 13 14 syl 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( K < N <-> ( N - K ) e. NN ) )
16 11 15 mpbid 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( N - K ) e. NN )
17 nnm1ge0 
 |-  ( ( N - K ) e. NN -> 0 <_ ( ( N - K ) - 1 ) )
18 16 17 syl 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> 0 <_ ( ( N - K ) - 1 ) )
19 elnn0z 
 |-  ( ( ( N - K ) - 1 ) e. NN0 <-> ( ( ( N - K ) - 1 ) e. ZZ /\ 0 <_ ( ( N - K ) - 1 ) ) )
20 10 18 19 sylanbrc 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( ( N - K ) - 1 ) e. NN0 )
21 simp2 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> N e. NN )
22 nncn 
 |-  ( N e. NN -> N e. CC )
23 22 adantl 
 |-  ( ( K e. NN0 /\ N e. NN ) -> N e. CC )
24 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
25 24 adantr 
 |-  ( ( K e. NN0 /\ N e. NN ) -> K e. CC )
26 1cnd 
 |-  ( ( K e. NN0 /\ N e. NN ) -> 1 e. CC )
27 23 25 26 subsub4d 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( N - K ) - 1 ) = ( N - ( K + 1 ) ) )
28 nn0p1gt0 
 |-  ( K e. NN0 -> 0 < ( K + 1 ) )
29 28 adantr 
 |-  ( ( K e. NN0 /\ N e. NN ) -> 0 < ( K + 1 ) )
30 nn0re 
 |-  ( K e. NN0 -> K e. RR )
31 peano2re 
 |-  ( K e. RR -> ( K + 1 ) e. RR )
32 30 31 syl 
 |-  ( K e. NN0 -> ( K + 1 ) e. RR )
33 nnre 
 |-  ( N e. NN -> N e. RR )
34 ltsubpos 
 |-  ( ( ( K + 1 ) e. RR /\ N e. RR ) -> ( 0 < ( K + 1 ) <-> ( N - ( K + 1 ) ) < N ) )
35 32 33 34 syl2an 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( 0 < ( K + 1 ) <-> ( N - ( K + 1 ) ) < N ) )
36 29 35 mpbid 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( N - ( K + 1 ) ) < N )
37 27 36 eqbrtrd 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( N - K ) - 1 ) < N )
38 37 3adant3 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( ( N - K ) - 1 ) < N )
39 elfzo0 
 |-  ( ( ( N - K ) - 1 ) e. ( 0 ..^ N ) <-> ( ( ( N - K ) - 1 ) e. NN0 /\ N e. NN /\ ( ( N - K ) - 1 ) < N ) )
40 20 21 38 39 syl3anbrc 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( ( N - K ) - 1 ) e. ( 0 ..^ N ) )
41 1 40 sylbi 
 |-  ( K e. ( 0 ..^ N ) -> ( ( N - K ) - 1 ) e. ( 0 ..^ N ) )