Description: A member in a half-open range of nonnegative integers is less than or equal to the upper bound of the range. (Contributed by Alexander van der Vekens, 23-Sep-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elfzo0le | |- ( A e. ( 0 ..^ B ) -> A <_ B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfzo0 | |- ( A e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. NN /\ A < B ) ) |
|
| 2 | nn0re | |- ( A e. NN0 -> A e. RR ) |
|
| 3 | nnre | |- ( B e. NN -> B e. RR ) |
|
| 4 | ltle | |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) ) |
|
| 5 | 2 3 4 | syl2an | |- ( ( A e. NN0 /\ B e. NN ) -> ( A < B -> A <_ B ) ) |
| 6 | 5 | 3impia | |- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> A <_ B ) |
| 7 | 1 6 | sylbi | |- ( A e. ( 0 ..^ B ) -> A <_ B ) |