Theorem ubmelfzo

Description: If an integer in a 1-based finite set of sequential integers is subtracted from the upper bound of this finite set of sequential integers, the result is contained in a half-open range of nonnegative integers with the same upper bound. (Contributed by AV, 18-Mar-2018) (Revised by AV, 30-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> K <_ N )
2		nnnn0	|- ( K e. NN -> K e. NN0 )
3		nnnn0	|- ( N e. NN -> N e. NN0 )
4	2 3	anim12i	|- ( ( K e. NN /\ N e. NN ) -> ( K e. NN0 /\ N e. NN0 ) )
5	4	3adant3	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( K e. NN0 /\ N e. NN0 ) )
6		nn0sub	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( K <_ N <-> ( N - K ) e. NN0 ) )
7	5 6	syl	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( K <_ N <-> ( N - K ) e. NN0 ) )
8	1 7	mpbid	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( N - K ) e. NN0 )
9		simp2	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> N e. NN )
10		nngt0	|- ( K e. NN -> 0 < K )
11	10	3ad2ant1	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> 0 < K )
12		nnre	|- ( K e. NN -> K e. RR )
13		nnre	|- ( N e. NN -> N e. RR )
14	12 13	anim12i	|- ( ( K e. NN /\ N e. NN ) -> ( K e. RR /\ N e. RR ) )
15	14	3adant3	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( K e. RR /\ N e. RR ) )
16		ltsubpos	|- ( ( K e. RR /\ N e. RR ) -> ( 0 < K <-> ( N - K ) < N ) )
17	15 16	syl	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( 0 < K <-> ( N - K ) < N ) )
18	11 17	mpbid	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( N - K ) < N )
19	8 9 18	3jca	|- ( ( K e. NN /\ N e. NN /\ K <_ N ) -> ( ( N - K ) e. NN0 /\ N e. NN /\ ( N - K ) < N ) )
20		elfz1b	|- ( K e. ( 1 ... N ) <-> ( K e. NN /\ N e. NN /\ K <_ N ) )
21		elfzo0	|- ( ( N - K ) e. ( 0 ..^ N ) <-> ( ( N - K ) e. NN0 /\ N e. NN /\ ( N - K ) < N ) )
22	19 20 21	3imtr4i	|- ( K e. ( 1 ... N ) -> ( N - K ) e. ( 0 ..^ N ) )