Metamath Proof Explorer

Theorem fzonn0p1p1

Description: If a nonnegative integer is element of a half-open range of nonnegative integers, increasing this integer by one results in an element of a half- open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018)

Ref Expression
Assertion fzonn0p1p1 
|- ( I e. ( 0 ..^ N ) -> ( I + 1 ) e. ( 0 ..^ ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( I e. ( 0 ..^ N ) <-> ( I e. NN0 /\ N e. NN /\ I < N ) )
2 peano2nn0 
 |-  ( I e. NN0 -> ( I + 1 ) e. NN0 )
3 2 3ad2ant1 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( I + 1 ) e. NN0 )
4 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
5 4 3ad2ant2 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( N + 1 ) e. NN )
6 simp3 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> I < N )
7 nn0re 
 |-  ( I e. NN0 -> I e. RR )
8 nnre 
 |-  ( N e. NN -> N e. RR )
9 1red 
 |-  ( I < N -> 1 e. RR )
10 ltadd1 
 |-  ( ( I e. RR /\ N e. RR /\ 1 e. RR ) -> ( I < N <-> ( I + 1 ) < ( N + 1 ) ) )
11 7 8 9 10 syl3an 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( I < N <-> ( I + 1 ) < ( N + 1 ) ) )
12 6 11 mpbid 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( I + 1 ) < ( N + 1 ) )
13 elfzo0 
 |-  ( ( I + 1 ) e. ( 0 ..^ ( N + 1 ) ) <-> ( ( I + 1 ) e. NN0 /\ ( N + 1 ) e. NN /\ ( I + 1 ) < ( N + 1 ) ) )
14 3 5 12 13 syl3anbrc 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( I + 1 ) e. ( 0 ..^ ( N + 1 ) ) )
15 1 14 sylbi 
 |-  ( I e. ( 0 ..^ N ) -> ( I + 1 ) e. ( 0 ..^ ( N + 1 ) ) )