Description: An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | uzuzle23 | |- ( A e. ( ZZ>= ` 3 ) -> A e. ( ZZ>= ` 2 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2z | |- 2 e. ZZ |
|
| 2 | 2re | |- 2 e. RR |
|
| 3 | 3re | |- 3 e. RR |
|
| 4 | 2lt3 | |- 2 < 3 |
|
| 5 | 2 3 4 | ltleii | |- 2 <_ 3 |
| 6 | eluzuzle | |- ( ( 2 e. ZZ /\ 2 <_ 3 ) -> ( A e. ( ZZ>= ` 3 ) -> A e. ( ZZ>= ` 2 ) ) ) |
|
| 7 | 1 5 6 | mp2an | |- ( A e. ( ZZ>= ` 3 ) -> A e. ( ZZ>= ` 2 ) ) |